A verified prover based on ordered resolution

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedings – Annual report year: 2019Researchpeer-review

Documents

DOI

View graph of relations

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
CitationsWeb of Science® Times Cited: No match on DOI

    Research areas

  • Automatic theorem provers, First-order logic, Proof assistants, Stepwise refinement
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: 172637140