Conference paper
A Micro Prover for Teaching Automated Reasoning
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.
Language: | English |
---|---|
Year: | 2020 |
Proceedings: | 7<sup>th </sup>Workshop on Practical Aspects of Automated Reasoning |
Types: | Conference paper |
ORCIDs: | Villadsen, Jørgen |