Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

Anders Schlichtkrull*, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review

212 Downloads (Pure)


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 developed general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition. Our work clarifies fine points in the chapter, emphasizing the value of formal proofs in the field of automated reasoning.

Original languageEnglish
Pages (from-to)1169-1195
Number of pages27
JournalJournal of Automated Reasoning
Issue number7
Early online date17 Jun 2020
Publication statusPublished - Oct 2020

Bibliographical note

Special Issue: Selected Extended Papers from IJCAR 2018.


Schlichtkrull was supported by a Ph.D. scholarship in the Algorithms, Logic and Graphs section of DTU Compute and by the LIGHT est \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathrm {LIGHT}^{ est }$$\end{document} project, which is partially funded by the European Commission as an Innovation Act as part of the Horizon 2020 research and innovation program (Grant Agreement No. 700321, LIGHTest). Blanchette was partly supported by the Deutsche Forschungsgemeinschaft (DFG) project Hardening the Hammer (Grant NI 491/14-1). He also received funding from the ERC under the European Union’s Horizon 2020 program (Grant Agreement No. 713999, Matryoshka) and from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (Project No. 016.Vidi.189.037, Lean Forward). Traytel was partly supported by the DFG program Program and Model Analysis (PUMA, doctorate Program 1480).

FundersFunder number
Horizon 2020 Framework Programme
European Commission
European Research Council
Deutsche ForschungsgemeinschaftNI 491/14-1
Nederlandse Organisatie voor Wetenschappelijk Onderzoek016
Horizon 2020713999, 700321


    • Automatic theorem provers
    • Proof assistants
    • Resolution calculus


    Dive into the research topics of 'Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover'. Together they form a unique fingerprint.

    Cite this