Boolean reasoning in a higher-order superposition prover

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

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 languageEnglish
Title of host publicationPAAR+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)
EditorsPascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, Sophie Tourret
PublisherCEUR-WS
Pages148-166
Number of pages19
Publication statusPublished - 26 Nov 2020
EventJoint 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

NameCEUR Workshop Proceedings
PublisherCEUR Workshop Proceedings
Volume2752
ISSN (Print)1613-0073

Conference

ConferenceJoint of the 7th Workshop on Practical Aspects of Automated Reasoning and the 5th Satisfiability Checking and Symbolic Computation Workshop, PAAR+SC-Square 2020
CountryFrance
CityVirtual, Paris
Period5/07/20 → …

Keywords

  • Higher-order logic
  • Superposition
  • Theorem proving

Cite this