Superposition with First-class Booleans and Inprocessing Clausification

AbstractWe 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.

Download Full-text

Making Higher-Order Superposition Work

Automated Deduction – CADE 28 - Lecture Notes in Computer Science ◽

10.1007/978-3-030-79876-5_24 ◽

2021 ◽

pp. 415-432

Author(s):

Petar Vukmirović ◽

Alexander Bentkamp ◽

Jasmin Blanchette ◽

Simon Cruanes ◽

Visa Nummelin ◽

...

Keyword(s):

Higher Order ◽

Order Logic ◽

Theorem Prover ◽

First Order Logic ◽

Inference Rules ◽

Higher Order Logic ◽

First Order ◽

New Challenges

AbstractSuperposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about formulas, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.

Download Full-text

Satisfiability Checking and Query Answering for Large Ontologies

10.29007/n1sv ◽

2018 ◽

Author(s):

Christoph Weidenbach ◽

Patrick Wischnewski

Keyword(s):

State Of The Art ◽

The State ◽

Order Logic ◽

Query Answering ◽

First Order Logic ◽

First Order ◽

Satisfiability Checking ◽

Superposition Calculus

In this paper we develop a sound, complete and terminating superposition calculusplus a query answering calculus for the BSH-Y2 fragment of theBernays-Schoenfinkel Horn class of first-order logic.BSH-Y2 can be used to represent expressive ontologies.In addition to checking consistency, our calculus supports query answeringfor queries with arbitrary quantifier alternations.Experiments on BSH-Y2 (fragments) of several large ontologies show that ourapproach advances the state of the art.

Download Full-text

Extending a brainiac prover to lambda-free higher-order logic

International Journal on Software Tools for Technology Transfer ◽

10.1007/s10009-021-00639-7 ◽

2021 ◽

Author(s):

Petar Vukmirović ◽

Jasmin Blanchette ◽

Simon Cruanes ◽

Stephan Schulz

Keyword(s):

Data Structures ◽

Theorem Proving ◽

State Of The Art ◽

Higher Order ◽

The State ◽

Order Logic ◽

Automatic Theorem Proving ◽

Higher Order Logic ◽

First Order ◽

Automatic Theorem

AbstractDecades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to $$\lambda $$ λ -free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone toward full higher-order logic.

Download Full-text

A Clausal Normal Form Translation for FOOL

10.29007/ltkk ◽

2018 ◽

Author(s):

Evgenii Kotelnikov ◽

Laura Kovács ◽

Martin Suda ◽

Andrei Voronkov

Keyword(s):

Normal Form ◽

Programming Languages ◽

Program Analysis ◽

State Of The Art ◽

Order Logic ◽

Theorem Prover ◽

First Order Logic ◽

First Order ◽

Theorem Provers ◽

Superposition Calculus

Automated theorem provers for first-order logic usually operate on sets of first-order clauses. It is well-known that the translation of a formula in full first-order logic to a clausal normal form (CNF) can crucially affect performance of a theorem prover. In our recent work we introduced a modification of first-order logic extended by the first class boolean sort and syntactical constructs that mirror features of programming languages. We called this logic FOOL. Formulas in FOOL can be translated to ordinary first-order formulas and checked by first-order theorem provers. While this translation is straightforward, it does not result in a CNF that can be efficiently handled by state-of-the-art theorem provers which use superposition calculus. In this paper we present a new CNF translation algorithm for FOOL that is friendly and efficient for superposition-based first-order provers. We implemented the algorithm in the Vampire theorem prover and evaluated it on a large number of problems coming from formalisation of mathematics and program analysis. Our experimental results show an increase of performance of the prover with our CNF translation compared to the naive translation.

Download Full-text

Resolution in type theory

Journal of Symbolic Logic ◽

10.2307/2269949 ◽

1971 ◽

Vol 36 (3) ◽

pp. 414-432 ◽

Cited By ~ 107

Author(s):

Peter B. Andrews

Keyword(s):

Set Theory ◽

Type Theory ◽

Higher Order ◽

Order Logic ◽

First Order Logic ◽

Higher Order Logic ◽

First Order ◽

Different Types ◽

Axiomatic Set Theory ◽

Order Predicate Calculus

In [8] J. A. Robinson introduced a complete refutation procedure called resolution for first order predicate calculus. Resolution is based on ideas in Herbrand's Theorem, and provides a very convenient framework in which to search for a proof of a wff believed to be a theorem. Moreover, it has proved possible to formulate many refinements of resolution which are still complete but are more efficient, at least in many contexts. However, when efficiency is a prime consideration, the restriction to first order logic is unfortunate, since many statements of mathematics (and other disciplines) can be expressed more simply and naturally in higher order logic than in first order logic. Also, the fact that in higher order logic (as in many-sorted first order logic) there is an explicit syntactic distinction between expressions which denote different types of intuitive objects is of great value where matching is involved, since one is automatically prevented from trying to make certain inappropriate matches. (One may contrast this with the situation in which mathematical statements are expressed in the symbolism of axiomatic set theory.).

Download Full-text

Formalization of Linear Space Theory in the Higher-Order Logic Proving System

Journal of Applied Mathematics ◽

10.1155/2013/218492 ◽

2013 ◽

Vol 2013 ◽

pp. 1-6 ◽

Cited By ~ 1

Author(s):

Jie Zhang ◽

Danwen Mao ◽

Yong Guan

Keyword(s):

Linear Space ◽

Theorem Proving ◽

Predicate Logic ◽

Higher Order ◽

Order Logic ◽

First Order Logic ◽

Space Theory ◽

Higher Order Logic ◽

First Order ◽

Important Approach

Theorem proving is an important approach in formal verification. Higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and stronger semantics. Higher-order logic is more expressive. This paper presents the formalization of the linear space theory in HOL4. A set of properties is characterized in HOL4. This result is used to build the underpinnings for the application of higher-order logic in a wider spectrum of engineering applications.

Download Full-text

Antirealism/realism of Hintikka’s game-theoretical semantics

Papers on Philosophy Psychology Sociology and Pedagogy ◽

10.15291/radovifpsp.2405 ◽

2018 ◽

Vol 26 (3) ◽

Author(s):

Heda Festini

Keyword(s):

Higher Order ◽

Order Logic ◽

First Order Logic ◽

Higher Order Logic ◽

First Order ◽

Theory Of Meaning ◽

Truth Conditional ◽

Context Dependent ◽

Extended Notion

Hintikka’s game-theoretical semantics (GTS) is presented as an anti-Tarskian semantical approach to the context-dependent fragments of Englisch, which overcomes the usual notion of semantical realism. Analysing Hintikka’s critique of Tarski’s interpretation of the truth-conditional theory of meaning, its recursive fashion and the narrow notion of realism, Hintikka’s basic conception is presented in the following manner:1. the Context-Principle vs. the Frege Principle,2.First-order logic together with higher-order logic vs. the primacy of first-order logic,3.verificationist/falsificationist theory vs. Taraski’s narrow truth- conditional theory.Comparing some reviews of Hintikka’s GTS (M. Dummett, E. Itkonen, E. Saarinen, M. Hand) with a short examination of the antirealistic/realistic controversis by C. Wright and M. Dummett, the following was reached:Hintikka’s GTS introduces a new, more extended notion of realism, which embraces Taraski-type realistic semantics, Hintikka’s GTS and with this the question of the possibility to also include Dummett’s neoverificationism or other orientations, remains open.

Download Full-text

Leo-III Version 1.1 (System description)

10.29007/grmx ◽

2018 ◽

Author(s):

Christoph Benzmüller ◽

Alexander Steen ◽

Max Wisniewski

Keyword(s):

Higher Order ◽

Order Logic ◽

Theorem Prover ◽

Higher Order Logic ◽

System Description ◽

Agent Based ◽

First Order ◽

Theorem Provers ◽

Automated Theorem Prover ◽

Ordering Constraints

Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based on a paramodulation calculus with ordering constraints and, in tradition of its predecessor LEO-II, heavily relies on cooperation with external first-order theorem provers.Unlike LEO-II, asynchronous cooperation with typed first-order provers and an agent-based internal cooperation scheme is supported. In this paper, we sketch Leo-III's underlying calculus, survey implementation details and give examples of use.

Download Full-text

Using the TPTP Language for Representing Derivations in Tableau and Connection Calculi

10.29007/jcqn ◽

2018 ◽

Author(s):

Jens Otten ◽

Geoff Sutcliffe

Keyword(s):

Higher Order ◽

Order Logic ◽

First Order Logic ◽

Higher Order Logic ◽

First Order ◽

Standard Tableau ◽

Representation Of Solutions ◽

Problems And Solutions

The TPTP language, developed within the framework of the TPTP library, allows the representation of problems and solutions in first-order and higher-order logic. Whereas the writing of solutions in resolution calculi is well documented and used, an appropriate representation of solutions in tableau or connection calculi using the TPTP syntax has not yet been specified. This paper describes how the TPTP language can be used to represent derivations and solutions in standard tableau, sequent and connection calculi for classical first-order logic.

Download Full-text

Fraïssé–Hintikka theorem in institutions

Journal of Logic and Computation ◽

10.1093/logcom/exaa042 ◽

2020 ◽

Vol 30 (7) ◽

pp. 1377-1399

Author(s):

Daniel Găină ◽

Tomasz Kowalski

Keyword(s):

Classical Case ◽

Higher Order ◽

Order Logic ◽

First Order Logic ◽

Specification Languages ◽

Higher Order Logic ◽

Elementary Equivalence ◽

First Order

Abstract We generalize the characterization of elementary equivalence by Ehrenfeucht–Fraïssé games to arbitrary institutions whose sentences are finitary. These include many-sorted first-order logic, higher-order logic with types, as well as a number of other logics arising in connection to specification languages. The gain for the classical case is that the characterization is proved directly for all signatures, including infinite ones.

Download Full-text