A Micro Prover for Teaching Automated Reasoning

Research output: Contribution to conferencePaperResearchpeer-review

37 Downloads (Pure)

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 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
http://paar2020.gforge.inria.fr/

Workshop

Workshop7th Workshop on Practical Aspects of Automated Reasoning
LocationVirtual event
Country/TerritoryFrance
CityParis
Period29/06/202030/06/2020
Internet address

Fingerprint

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

Cite this