4 citations · 11 across the 4 of their papers we have counts for
4 papers
Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
Lukas Stevens
Using Isabelle/HOL, we verify the state-of-the-art decision procedure for multi-level syllogistic with singleton (MLSS for short), which is a quantifier-free fragment of set theory…
Engaging, Large-Scale Functional Programming Education in Physical and Virtual Space
Kevin Kappelmann, Jonas Rädle, Lukas Stevens
Worldwide, computer science departments have experienced a dramatic increase in the number of student enrolments. Moreover, the ongoing COVID-19 pandemic requires institutions to r…
A Linter for Isabelle: Implementation and Evaluation
Yecine Megdiche, Fabian Huch, Lukas Stevens
In interactive theorem proving, formalization quality is a key factor for maintainability and re-usability of developments and can also impact proof-checking performance. Commonly,…
A Verified Decision Procedure for Orders in Isabelle/HOL
Lukas Stevens, Tobias Nipkow
We present the first verified implementation of a decision procedure for the quantifier-free theory of partial and linear orders. We formalise the procedure in Isabelle/HOL and pro…