A Verified Simple Prover for First-Order Logic

Research output: Research - peer-reviewArticle in proceedings – Annual report year: 2018

Documents

Links

View graph of relations

We present a simple prover for first-order logic with certified soundness and completeness in Isabelle/HOL, taking formalizations by Tom Ridge and others as the starting point, but with the aim of using the approach for teaching logic and verification to computer science students at the bachelor level. The prover is simple in the following sense: It is purely functional and can be executed with rewriting rules or as code generation to a number of functional programming languages. The prover uses no higher-order functions, that is, no function takes a function as argument or returns a function as its result. This is advantageous when students perform rewriting steps by hand. The prover uses the logic of first-order logic on negation normal form with a term language consisting of only variables. This subset of the full syntax of first-order logic allows for a simple proof system without resorting to the much weaker propositional logic.
Original languageEnglish
Title of host publicationProceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR)
EditorsBoris Konev, Josef Urban, Philipp Rümmer
PublisherCEUR-WS
Publication date2018
Pages88—104
StatePublished - 2018
Event6th Workshop on Practical Aspects of Automated Reasoning (PAAR) - Oxford, United Kingdom
Duration: 19 Jul 201819 Jul 2018

Workshop

Workshop6th Workshop on Practical Aspects of Automated Reasoning (PAAR)
CountryUnited Kingdom
CityOxford
Period19/07/201819/07/2018
SeriesCEUR Workshop Proceedings
Volume2162
ISSN1613-0073
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

Download statistics

No data available

ID: 152182881