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

Fingerprint

Specifications

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 (Ed.), CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019 (pp. 152-165). Association for Computing Machinery, Inc. https://doi.org/10.1145/3293880.3294100
Schlichtkrull, Anders ; Blanchette, Jasmin Christian ; Traytel, Dmitriy. / A verified prover based on ordered resolution. CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. editor / Assia Mahboubi. Association for Computing Machinery, Inc, 2019. pp. 152-165
@inproceedings{234da92dfaaf4e3aa2d9a1793346eec9,
title = "A verified prover based on ordered resolution",
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.",
keywords = "automatic theorem provers, first-order logic, proof assistants, stepwise refinement",
author = "Anders Schlichtkrull and Blanchette, {Jasmin Christian} and Dmitriy Traytel",
year = "2019",
month = "1",
day = "14",
doi = "10.1145/3293880.3294100",
language = "English",
pages = "152--165",
editor = "Assia Mahboubi",
booktitle = "CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019",
publisher = "Association for Computing Machinery, Inc",

}

Schlichtkrull, A, Blanchette, JC & Traytel, D 2019, A verified prover based on ordered resolution. in A Mahboubi (ed.), CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. Association for Computing Machinery, Inc, pp. 152-165, 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, 14/01/19. https://doi.org/10.1145/3293880.3294100

A verified prover based on ordered resolution. / Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy.

CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. ed. / Assia Mahboubi. Association for Computing Machinery, Inc, 2019. p. 152-165.

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

TY - GEN

T1 - A verified prover based on ordered resolution

AU - Schlichtkrull, Anders

AU - Blanchette, Jasmin Christian

AU - Traytel, Dmitriy

PY - 2019/1/14

Y1 - 2019/1/14

N2 - 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.

AB - 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.

KW - automatic theorem provers

KW - first-order logic

KW - proof assistants

KW - stepwise refinement

UR - http://www.scopus.com/inward/record.url?scp=85061211892&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85061211892&partnerID=8YFLogxK

U2 - 10.1145/3293880.3294100

DO - 10.1145/3293880.3294100

M3 - Conference contribution

SP - 152

EP - 165

BT - CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019

A2 - Mahboubi, Assia

PB - Association for Computing Machinery, Inc

ER -

Schlichtkrull A, Blanchette JC, Traytel D. A verified prover based on ordered resolution. In Mahboubi A, editor, CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. Association for Computing Machinery, Inc. 2019. p. 152-165 https://doi.org/10.1145/3293880.3294100