scholarly journals 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.

scholarly journals Superposition with First-class Booleans and Inprocessing Clausification

2021 ◽  
pp. 378-395
Author(s):  
Visa Nummelin ◽  
Alexander Bentkamp ◽  
Sophie Tourret ◽  
Petar Vukmirović
Keyword(s):  
State Of The Art ◽  
Higher Order ◽  
The State ◽  
Order Logic ◽  
Theorem Prover ◽  
First Order Logic ◽  
Higher Order Logic ◽  
First Order ◽  
Superposition Calculus

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.

scholarly journals Integer Induction in Saturation

2021 ◽  
pp. 361-377
Author(s):  
Petra Hozzová ◽  
Laura Kovács ◽  
Andrei Voronkov
Keyword(s):  
Theorem Proving ◽  
Program Analysis ◽  
State Of The Art ◽  
Inductive Reasoning ◽  
Theorem Prover ◽  
Inference Rules ◽  
First Order ◽  
Theorem Provers ◽  
Mathematical Properties

AbstractIntegers are ubiquitous in programming and therefore also in applications of program analysis and verification. Such applications often require some sort of inductive reasoning. In this paper we analyze the challenge of automating inductive reasoning with integers. We introduce inference rules for integer induction within the saturation framework of first-order theorem proving. We implemented these rules in the theorem prover Vampire and evaluated our work against other state-of-the-art theorem provers. Our results demonstrate the strength of our approach by solving new problems coming from program analysis and mathematical properties of integers.

scholarly journals Implementing Polymorphism in Zenon

10.29007/87vl ◽  
2018 ◽  
Author(s):  
Guillaume Bury ◽  
Raphaël Cauderlier ◽  
Pierre Halmagrand
Keyword(s):  
Search Algorithm ◽  
Order Logic ◽  
Theorem Prover ◽  
First Order Logic ◽  
First Order ◽  
Proof Search ◽  
Theorem Provers ◽  
Automated Theorem Prover

Extending first-order logic with ML-style polymorphism allows to definegeneric axioms dealing with several sorts. Until recently, mostautomated theorem provers relied on preprocess encodings intomono/many-sorted logic to reason within such theories. In this paper, wediscuss the implementation of polymorphism into thefirst-order tableau-based automated theorem prover Zenon. Thisimplementation leads to slightly modify some basic parts of the code,from the representation of expressions to the proof-search algorithm.

scholarly journals 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.

scholarly journals Extensions in graph normal form

2020 ◽  
Author(s):  
Michał Walicki
Keyword(s):  
Normal Form ◽  
Fixed Points ◽  
Propositional Logic ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Special Cases

Abstract Graph normal form, introduced earlier for propositional logic, is shown to be a normal form also for first-order logic. It allows to view syntax of theories as digraphs, while their semantics as kernels of these digraphs. Graphs are particularly well suited for studying circularity, and we provide some general means for verifying that circular or apparently circular extensions are conservative. Traditional syntactic means of ensuring conservativity, like definitional extensions or positive occurrences guaranteeing exsitence of fixed points, emerge as special cases.

scholarly journals CSE_E 1.0: An Integrated Automated Theorem Prover for First-Order Logic

Symmetry ◽  
2019 ◽  
Vol 11 (9) ◽  
pp. 1142
Author(s):  
Feng Cao ◽  
Yang Xu ◽  
Jun Liu ◽  
Shuwei Chen ◽  
Xinran Ning
Keyword(s):  
Order Logic ◽  
Theorem Prover ◽  
First Order Logic ◽  
Inference Mechanism ◽  
First Order ◽  
Proof Search ◽  
Interdisciplinary Field ◽  
Heuristic Strategies ◽  
Automated Theorem Prover ◽  
Hard Problems

First-order logic is an important part of mathematical logic, and automated theorem proving is an interdisciplinary field of mathematics and computer science. The paper presents an automated theorem prover for first-order logic, called C S E _ E 1.0, which is a combination of two provers contradiction separation extension (CSE) and E, where CSE is based on the recently-introduced multi-clause standard contradiction separation (S-CS) calculus for first-order logic and E is the well-known equational theorem prover for first-order logic based on superposition and rewriting. The motivation of the combined prover C S E _ E 1.0 is to (1) evaluate the capability, applicability and generality of C S E _ E , and (2) take advantage of novel multi-clause S-CS dynamic deduction of CSE and mature equality handling of E to solve more and harder problems. In contrast to other improvements of E, C S E _ E 1.0 optimizes E mainly from the inference mechanism aspect. The focus of the present work is given to the description of C S E _ E including its S-CS rule, heuristic strategies, and the S-CS dynamic deduction algorithm for implementation. In terms of combination, in order not to lose the capability of E and use C S E _ E to solve some hard problems which are unsolved by E, C S E _ E 1.0 schedules the running of the two provers in time. It runs plain E first, and if E does not find a proof, it runs plain CSE, then if it does not find a proof, some clauses inferred in the CSE run as lemmas are added to the original clause set and the combined clause set handed back to E for further proof search. C S E _ E 1.0 is evaluated through benchmarks, e.g., CASC-26 (2017) and CASC-J9 (2018) competition problems (FOFdivision). Experimental results show that C S E _ E 1.0 indeed enhances the performance of E to a certain extent.

Lifting propositional proof compression algorithms to first-order logic

2020 ◽  
Author(s):  
Jan Gorzny ◽  
Ezequiel Postan ◽  
Bruno Woltzenlogel Paleo
Keyword(s):  
Propositional Logic ◽  
Empirical Evaluation ◽  
Order Logic ◽  
Automated Deduction ◽  
First Order Logic ◽  
Compression Algorithms ◽  
International Conference ◽  
First Order ◽  
Theorem Provers ◽  
Resolution Proofs

Abstract Proofs are a key feature of modern propositional and first-order theorem provers. Proofs generated by such tools serve as explanations for unsatisfiability of statements. However, these explanations are complicated by proofs which are not necessarily as concise as possible. There are a wide variety of compression techniques for propositional resolution proofs but fewer compression techniques for first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. The first approach lifted from propositional logic delays resolution with unit clauses, which are clauses that have a single literal. The second approach is partial regularization, which removes an inference $\eta $ when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from $\eta $ to the root of the proof. This paper describes the generalization of the algorithms LowerUnits and RecyclePivotsWithIntersection (Fontaine et al.. Compression of propositional resolution proofs via partial regularization. In Automated Deduction—CADE-23—23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31–August 5, 2011, p. 237--251. Springer, 2011) from propositional logic to first-order logic. The generalized algorithms compresses resolution proofs containing resolution and factoring inferences with unification. An empirical evaluation of these approaches is included.

scholarly journals Towards closed world reasoning in dynamic open worlds

2010 ◽  
Vol 10 (4-6) ◽  
pp. 547-563 ◽  
Author(s):  
MARTIN SLOTA ◽  
JOÃO LEITE
Keyword(s):  
Semantic Web ◽  
State Of The Art ◽  
Knowledge Bases ◽  
Order Logic ◽  
First Order Logic ◽  
Static Case ◽  
First Order ◽  
Closed World ◽  
Hybrid Knowledge ◽  
First Time

AbstractThe need for integration of ontologies with nonmonotonic rules has been gaining importance in a number of areas, such as the Semantic Web. A number of researchers addressed this problem by proposing a unified semantics forhybrid knowledge basescomposed of both an ontology (expressed in a fragment of first-order logic) and nonmonotonic rules. These semantics have matured over the years, but only provide solutions for the static case when knowledge does not need to evolve.In this paper we take a first step towards addressing the dynamics of hybrid knowledge bases. We focus on knowledge updates and, considering the state of the art of belief update, ontology update and rule update, we show that current solutions are only partial and difficult to combine. Then we extend the existing work on ABox updates with rules, provide a semantics for such evolving hybrid knowledge bases and study its basic properties.To the best of our knowledge, this is the first time that an update operator is proposed for hybrid knowledge bases.

Sign in / Sign up

Export Citation Format

Share Document