research-article

A verified prover based on ordered resolution

Authors:

Anders Schlichtkrull,

Jasmin Christian Blanchette,

Dmitriy TraytelAuthors Info & Claims

CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 152 - 165

https://doi.org/10.1145/3293880.3294100

Published: 14 January 2019 Publication History

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.

References

[1]

Leo Bachmair, Nachum Dershowitz, and David A. Plaisted. 1989. Completion without Failure. In Rewriting Techniques--resolution of Equations in Algebraic Structures, Hassan Aït-Kaci and Maurice Nivat (Eds.). Vol. 2. Academic Press, 1-30.

[2]

Leo Bachmair and Harald Ganzinger. 2001. Resolution Theorem Proving. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). Vol. I. Elsevier and MIT Press, 19-99.

[3]

Jasmin Christian Blanchette. 2019. Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Paper). In CPP 2019, Assia Mahboubi and Magnus O. Myreen (Eds.). ACM.

Digital Library

[4]

Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier. 2016. Semi-intelligible Isar Proofs from Machine-Generated Proofs. J. Autom. Reasoning 56, 2 (2016), 155-200.

Digital Library

[5]

Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel. 2017. Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants. In ESOP 2017, Hongseok Yang (Ed.). LNCS, Vol. 10201. Springer, 111-140.

Digital Library

[6]

Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, and Christoph Weidenbach. 2018. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. Autom. Reasoning 61, 1-4 (2018), 333-365.

Digital Library

[7]

François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011, K. Rustan M. Leino and Michal Moskal (Eds.). 53-64.

[8]

Koen Claessen and Nicholas Smallbone. 2018. Efficient Encodings of First-Order Horn Formulas in Equational Logic. In IJCAR 2018, Didier Galmiche, Stephan Schulz, and Roberto Sebastiani (Eds.). LNCS, Vol. 10900. Springer, 388-404.

[9]

Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, and Peter Schneider-Kamp. 2017. Efficient Certified RAT Verification. In CADE-26, Leonardo de Moura (Ed.). LNCS, Vol. 10395. Springer, 220-236.

[10]

Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich. 2018. A Verified SAT Solver with Watched Literals using Imperative HOL. In CPP 2018, June Andronick and Amy P. Felty (Eds.). ACM, 158-171.

Digital Library

[11]

Florian Haftmann and Tobias Nipkow. 2010. Code Generation via Higher-Order Rewrite Systems. In FLOPS 2010, Matthias Blume, Naoki Kobayashi, and Germán Vidal (Eds.). LNCS, Vol. 6009. Springer, 103-117.

Digital Library

[12]

Thomas Hillenbrand, Arnim Buch, Roland Vogt, and Bernd Löchner. 1997. WALDMEISTER--High-Performance Equational Deduction. J. Autom. Reasoning 18, 2 (1997), 265-270.

Digital Library

[13]

Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler. 2017. Infinite Runs in Abstract Completion. In FSCD 2017, Dale Miller (Ed.). LIPIcs, Vol. 84. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 19:1-19:16.

[14]

Lars Hupel and Tobias Nipkow. 2018. A Verified Compiler from Isabelle/HOL to CakeML. In ESOP 2018, Amal Ahmed (Ed.). LNCS, Vol. 10801. Springer, 999-1026.

[15]

Joe Hurd. 2003. First-Order Proof Tactics in Higher-Order Logic Theorem Provers. In Design and Application of Strategies/Tactics in Higher Order Logics (STRATA), Myla Archer, Ben Di Vito, and César Muñoz (Eds.). 56-68.

[16]

Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull, and Jørgen Villadsen. 2018. Programming and Verifying a Declarative First-Order Prover in Isabelle/HOL. AICommun.31, 3 (2018), 281-299.

[17]

Cezary Kaliszyk and Josef Urban. 2013. PRocH: Proof Reconstruction for HOL Light. In CADE-24, Maria Paola Bonacina (Ed.). LNCS, Vol. 7898. Springer, 267-273.

Digital Library

[18]

Deepak Kapur and Paliath Narendran. 1986. NP-Completeness of the Set Unification and Matching Problems. In CADE-8, Jörg H. Siekmann (Ed.). LNCS, Vol. 230. Springer, 489-495.

Digital Library

[19]

Donald E. Knuth and Peter B. Bendix. 1970. Simple Word Problems in Universal Algebras. In Computational Problems in Abstract Algebra, John Leech (Ed.). Pergamon Press, 263-297.

[20]

Laura Kovács and Andrei Voronkov. 2009. Finding Loop Invariants for Programs over Arrays using a Theorem Prover. In SYNASC 2009, Stephen M. Watt, Viorel Negru, Tetsuo Ida, Tudor Jebelean, Dana Petcu, and Daniela Zaharie (Eds.). IEEE Computer Society, 10.

Digital Library

Cited By

Lund SVilladsen J(2024)On Verified Automated Reasoning in Propositional Logic: Teaching Sequent Calculus to Computer Science StudentsVietnam Journal of Computer Science10.1142/S2196888824500064(1-24)Online publication date: 2-May-2024
https://doi.org/10.1142/S2196888824500064
From AJacobsen F(2024)Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOLJournal of Automated Reasoning10.1007/s10817-024-09697-368:3Online publication date: 27-Jun-2024
https://dl.acm.org/doi/10.1007/s10817-024-09697-3
Ebner GBlanchette JTourret S(2023)Unifying SplittingJournal of Automated Reasoning10.1007/s10817-023-09660-867:2Online publication date: 28-Apr-2023
https://dl.acm.org/doi/10.1007/s10817-023-09660-8
Show More Cited By

Index Terms

A verified prover based on ordered resolution
1. Theory of computation
  1. Logic
    1. Automated reasoning
    2. Logic and verification

Recommendations

A modular Isabelle framework for verifying saturation provers
CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs

We present a formalization in Isabelle/HOL of a comprehensive framework for proving the completeness of automatic theorem provers based on resolution, superposition, or other saturation calculi. The framework helps calculus designers and prover ...
Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover
Abstract
We present an Isabelle/HOL formalization of the first half of Bachmair and Ganzinger’s chapter on resolution theorem proving, culminating with a refutationally complete first-order prover based on ordered resolution with literal selection. We ...
Soundness and Completeness Proofs by Coinductive Methods

We show how codatatypes can be employed to produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. For the classical completeness result, we first establish an ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2019

261 pages

ISBN:9781450362221

DOI:10.1145/3293880

Program Chairs:
Assia Mahboubi
INRIA, France
,
Magnus O. Myreen
Chalmers University of Technology, Sweden

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGLOG: ACM Special Interest Group on Logic and Computation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

European Research Council

Conference

CPP '19

Sponsor:

SIGPLAN

CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 14 - 15, 2019

Cascais, Portugal

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
127
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)0

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lund SVilladsen J(2024)On Verified Automated Reasoning in Propositional Logic: Teaching Sequent Calculus to Computer Science StudentsVietnam Journal of Computer Science10.1142/S2196888824500064(1-24)Online publication date: 2-May-2024
https://doi.org/10.1142/S2196888824500064
From AJacobsen F(2024)Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOLJournal of Automated Reasoning10.1007/s10817-024-09697-368:3Online publication date: 27-Jun-2024
https://dl.acm.org/doi/10.1007/s10817-024-09697-3
Ebner GBlanchette JTourret S(2023)Unifying SplittingJournal of Automated Reasoning10.1007/s10817-023-09660-867:2Online publication date: 28-Apr-2023
https://dl.acm.org/doi/10.1007/s10817-023-09660-8
From AVilladsen J(2023)A Naive Prover for First-Order Logic: A Minimal Example of Analytic CompletenessAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-031-43513-3_25(468-480)Online publication date: 14-Sep-2023
https://doi.org/10.1007/978-3-031-43513-3_25
Waldmann UTourret SRobillard SBlanchette J(2022)A Comprehensive Framework for Saturation Theorem ProvingJournal of Automated Reasoning10.1007/s10817-022-09621-766:4(499-539)Online publication date: 1-Nov-2022
https://dl.acm.org/doi/10.1007/s10817-022-09621-7
Lund SVilladsen J(2022)On Verified Automated Reasoning in Propositional LogicIntelligent Information and Database Systems10.1007/978-3-031-21743-2_31(390-402)Online publication date: 28-Nov-2022
https://dl.acm.org/doi/10.1007/978-3-031-21743-2_31
Sutcliffe GDesharnais M(2021)The CADE-28 Automated Theorem Proving System Competition – CASC-28AI Communications10.3233/AIC-21023534:4(259-276)Online publication date: 1-Jan-2021
https://dl.acm.org/doi/10.3233/AIC-210235
Tourret SBlanchette JHriţcu CPopescu A(2021)A modular Isabelle framework for verifying saturation proversProceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3437992.3439912(224-237)Online publication date: 17-Jan-2021
https://dl.acm.org/doi/10.1145/3437992.3439912
Abuin Ade Cerio UHermo MLucio P(2021)Verified Model Checking for Conjunctive Positive LogicSN Computer Science10.1007/s42979-020-00417-32:5Online publication date: 19-Jun-2021
https://doi.org/10.1007/s42979-020-00417-3
Villadsen JFrom AJensen ASchlichtkrull A(2021)Interactive Theorem Proving for Logic and InformationNatural Language Processing in Artificial Intelligence — NLPinAI 202110.1007/978-3-030-90138-7_2(25-48)Online publication date: 2-Nov-2021
https://doi.org/10.1007/978-3-030-90138-7_2
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents