A verified prover based on ordered resolution

Anders Schlichtkrull; Jasmin Christian Blanchette; Dmitriy Traytel

doi:10.1145/3293880.3294100

A verified prover based on ordered resolution

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

55 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 language	English
Title of host publication	CPP 2019
Subtitle of host publication	Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs
Editors	Assia Mahboubi
Publisher	Association for Computing Machinery, Inc
Pages	152-165
Number of pages	14
ISBN (Electronic)	9781450362221
DOIs	https://doi.org/10.1145/3293880.3294100
Publication status	Published - Jan 2019
Event	8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 - Cascais, Portugal Duration: 14 Jan 2019 → 15 Jan 2019

Conference

Conference	8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019
Country/Territory	Portugal
City	Cascais
Period	14/01/19 → 15/01/19

Funding

Funders	Funder number
Horizon 2020 Framework Programme	713999, 700321

Keywords

automatic theorem provers
first-order logic
proof assistants
stepwise refinement

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1145/3293880.3294100

A verified prover based on ordered resolutionFinal published version, 695 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Persistent link

Cite this

@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 = jan,

doi = "10.1145/3293880.3294100",

language = "English",

pages = "152--165",

editor = "Assia Mahboubi",

booktitle = "CPP 2019",

publisher = "Association for Computing Machinery, Inc",

note = "8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 ; Conference date: 14-01-2019 Through 15-01-2019",

}

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. 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. ed. / Assia Mahboubi. Association for Computing Machinery, Inc, 2019. p. 152-165.

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A verified prover based on ordered resolution

AU - Schlichtkrull, Anders

AU - Blanchette, Jasmin Christian

AU - Traytel, Dmitriy

PY - 2019/1

Y1 - 2019/1

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 - https://www.scopus.com/pages/publications/85061211892

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

U2 - 10.1145/3293880.3294100

DO - 10.1145/3293880.3294100

M3 - Conference contribution

AN - SCOPUS:85061211892

SP - 152

EP - 165

BT - CPP 2019

A2 - Mahboubi, Assia

PB - Association for Computing Machinery, Inc

T2 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019

Y2 - 14 January 2019 through 15 January 2019

ER -

A verified prover based on ordered resolution

Abstract

Conference

Funding

Keywords

UN SDGs

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this