A Micro Prover for Teaching Automated Reasoning

Research output: Contribution to conferencePaperResearchpeer-review

95 Downloads (Pure)


We present a simple prover for classical propositional logic. The prover is based on the sequent calculus and is formally verified in the Isabelle/HOL proof assistant. We use the prover for teaching automated reasoning to computer science students. The micro prover is available online and is simple enough to be the first example in a course. It shows how to use Isabelle/HOL and it also shows a prover program with termination, soundness and completeness proofs.
Original languageEnglish
Publication date2020
Number of pages12
Publication statusPublished - 2020
Event7th Workshop on Practical Aspects of Automated Reasoning - Virtual event, Paris, France
Duration: 29 Jun 202030 Jun 2020


Workshop7th Workshop on Practical Aspects of Automated Reasoning
LocationVirtual event
Internet address


Dive into the research topics of 'A Micro Prover for Teaching Automated Reasoning'. Together they form a unique fingerprint.

Cite this