Abstract
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 language | English |
|---|---|
| Publication date | 2020 |
| Number of pages | 12 |
| Publication status | Published - 2020 |
| Event | 7th Workshop on Practical Aspects of Automated Reasoning - Virtual event, Paris, France Duration: 29 Jun 2020 → 30 Jun 2020 http://paar2020.gforge.inria.fr/ |
Workshop
| Workshop | 7th Workshop on Practical Aspects of Automated Reasoning |
|---|---|
| Location | Virtual event |
| Country/Territory | France |
| City | Paris |
| Period | 29/06/2020 → 30/06/2020 |
| Internet address |