Code Generation for a Simple First-Order Prover

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

179 Downloads (Pure)

Abstract

We present Standard ML code generation in Isabelle/HOL of a sound and complete prover for first-order logic, taking formalizations by Tom Ridge and others as the starting point. We also define a set of so-called unfolding rules and show how to use these as a simple prover, with the aim of using the approach for teaching logic and verification to computer science students at the bachelor level.
Original languageEnglish
Title of host publicationProceedings of the Isabelle Workshop 2016
Number of pages15
Publication date2016
Publication statusPublished - 2016
EventIsabelle Workshop 2016 - Nancy, France
Duration: 25 Aug 201626 Aug 2016
http://www21.in.tum.de/~nipkow/Isabelle2016/

Workshop

WorkshopIsabelle Workshop 2016
CountryFrance
CityNancy
Period25/08/201626/08/2016
OtherAssociated with ITP 2016: Interactive Theorem Proving
Internet address

Keywords

  • Isabelle/HOL
  • First-order logic
  • Soundness
  • Completeness
  • Code generation
  • Unfolding rules
  • Standard ML
  • Isabelle/ML

Fingerprint Dive into the research topics of 'Code Generation for a Simple First-Order Prover'. Together they form a unique fingerprint.

Cite this