A verified prover based on ordered resolution

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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 publicationCPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019
EditorsAssia Mahboubi
PublisherAssociation for Computing Machinery, Inc
Pages152-165
Number of pages14
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/1915/01/19

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