Abstract
We present a pragmatic approach to extending a Boolean-free higher-order superposition calculus to support Boolean reasoning. Our approach extends inference rules that have been used only in a firstorder setting, uses some well-known rules previously implemented in higher-order provers, as well as new rules. We have implemented the approach in the Zipperposition theorem prover. The evaluation shows highly competitive performance of our approach and clear improvement over previous techniques.
| Original language | English |
|---|---|
| Title of host publication | PAAR+SC-Square 2020 Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2020 |
| Subtitle of host publication | Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020) Paris, France, June-July, 2020 (Virtual) |
| Editors | Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, Sophie Tourret |
| Publisher | CEUR-WS |
| Pages | 148-166 |
| Number of pages | 19 |
| Publication status | Published - 26 Nov 2020 |
| Event | Joint of the 7th Workshop on Practical Aspects of Automated Reasoning and the 5th Satisfiability Checking and Symbolic Computation Workshop, PAAR+SC-Square 2020 - Virtual, Paris, France Duration: 5 Jul 2020 → … |
Publication series
| Name | CEUR Workshop Proceedings |
|---|---|
| Publisher | CEUR Workshop Proceedings |
| Volume | 2752 |
| ISSN (Print) | 1613-0073 |
Conference
| Conference | Joint of the 7th Workshop on Practical Aspects of Automated Reasoning and the 5th Satisfiability Checking and Symbolic Computation Workshop, PAAR+SC-Square 2020 |
|---|---|
| Country/Territory | France |
| City | Virtual, Paris |
| Period | 5/07/20 → … |
Funding
Acknowledgment We are grateful to the maintainers of StarExec for letting us use their service. We thank Alexander Bentkamp, Jasmin Blanchette and Simon Cruanes for many stimulating discussions and all the useful advice. Alexander Bentkamp suggested the rule BoolER. We are also thankful to Ahmed Bhayat, Predrag Janičić and the anonymous reviewers for suggesting many improvements to this paper. We thank Evgeny Kotelnikov for patiently explaining the details of FOOL, Alexander Steen for clarifying Leo-III’s treatment of Booleans, and Giles Reger and Martin Suda for explaining the renaming mechanism implemented in VCNF. 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). Nummelin has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).
Keywords
- Higher-order logic
- Superposition
- Theorem proving