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

192 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, CPP 2019 - Cascais, Portugal
Duration: 14 Jan 201915 Jan 2019

Conference

Conference8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019
CountryPortugal
CityCascais
Period14/01/201915/01/2019
SponsorAssociation for Computing Machinery

Keywords

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

Cite this

Schlichtkrull, A., Blanchette, J. C., & Traytel, D. (2019). A verified prover based on ordered resolution. In A. Mahboubi, & M. O. Myreen (Eds.), Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 152-165). Association for Computing Machinery. https://doi.org/10.1145/3293880.3294100