Superposition with First-Class Booleans and Inprocessing Clausification

V. Nummelin, A. Bentkamp, S. Tourret, P. Vukmirović

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

Abstract

© 2021, The Author(s).We present a complete superposition calculus for first-order logic with an interpreted Boolean type. Our motivation is to lay the foundation for refutationally complete calculi in more expressive logics with Booleans, such as higher-order logic, and to make superposition work efficiently on problems that would be obfuscated when using clausification as preprocessing. Working directly on formulas, our calculus avoids the costly axiomatic encoding of the theory of Booleans into first-order logic and offers various ways to interleave clausification with other derivation steps. We evaluate our calculus using the Zipperposition theorem prover, and observe that, with no tuning of parameters, our approach is on a par with the state-of-the-art approach.
Original languageEnglish
Title of host publicationAutomated Deduction – CADE 2021
Subtitle of host publication28th International Conference on Automated Deduction, Proceedings
EditorsA. Platzer, G. Sutcliffe
PublisherSpringer Science and Business Media Deutschland GmbH
Pages378-395
ISBN (Print)9783030798758
DOIs
Publication statusPublished - 2021
Event28th International Conference on Automated Deduction, CADE 28 2021 - Virtual, Online
Duration: 12 Jul 202115 Jul 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference28th International Conference on Automated Deduction, CADE 28 2021
CityVirtual, Online
Period12/07/2115/07/21

Funding

Acknowledgment Martin Desharnais and Jasmin Blanchette generated the Sledgehammer benchmarks. Simon Cruanes helped us with the implementation. The anonymous reviewers, Ahmed Bhayat, Jasmin Blanchette, and Uwe Wald-mann suggested textual improvements. The maintainers of StarExec Iowa let us use their service. We thank them all. Nummelin’s research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Bentkamp and Vukmirović’s research has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka).

FundersFunder number
Horizon 2020 Framework Programme713999
European Research Council
Nederlandse Organisatie voor Wetenschappelijk Onderzoek016

    Fingerprint

    Dive into the research topics of 'Superposition with First-Class Booleans and Inprocessing Clausification'. Together they form a unique fingerprint.

    Cite this