A verified prover based on ordered resolution

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel

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

508 Downloads (Pure)

Abstract

The superposition calculus, which underlies first-order theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional first-order ordered resolution prover and establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract nondeterministic specification, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for first-order logic.

Original languageEnglish
Title of host publicationProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs
EditorsAssia Mahboubi, Magnus O. Myreen
PublisherAssociation for Computing Machinery
Publication date14 Jan 2019
Pages152-165
ISBN (Electronic)9781450362221
DOIs
Publication statusPublished - 14 Jan 2019
Event8th ACM SIGPLAN International Conference on Certified Programs and Proofs - Cascais, Portugal
Duration: 14 Jan 201915 Jan 2019
Conference number: 8

Conference

Conference8th ACM SIGPLAN International Conference on Certified Programs and Proofs
Number8
Country/TerritoryPortugal
CityCascais
Period14/01/201915/01/2019
SponsorAssociation for Computing Machinery

Keywords

  • Automatic theorem provers
  • First-order logic
  • Proof assistants
  • Stepwise refinement

Fingerprint

Dive into the research topics of 'A verified prover based on ordered resolution'. Together they form a unique fingerprint.

Cite this