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

scholarly journals Dialogues for proof search

10.29007/5t86 ◽  
2018 ◽  
Author(s):  
Jesse Alama
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Order Logic ◽  
Theorem Prover ◽  
First Order Logic ◽  
Dialogue Games ◽  
First Order ◽  
Proof Search ◽  
Automated Theorem Prover

Dialogue games are a two-player semantics for a variety of logics, including intuitionistic and classical logic. Dialogues can be viewed as a kind of analytic calculus not unlike tableaux. Can dialogue games be an effective foundation for proof search in intuitionistic logic (both first-order and propositional)? We announce Kuno, an automated theorem prover for intuitionistic first-order logic based on dialogue games.

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

scholarly journals nanoCoP: Natural Non-clausal Theorem Proving

2017 ◽  
Author(s):  
Jens Otten
Keyword(s):  
Conjunctive Normal Form ◽  
Order Logic ◽  
Theorem Prover ◽  
Original Structure ◽  
First Order ◽  
Proof Search ◽  
Automated Theorem Prover ◽  
Speed Up ◽  
Input Formula ◽  
Original Formula

Most efficient fully automated theorem provers implement proof search calculi that require the input formula to be in a clausal form, i.e. disjunctive or conjunctive normal form. The translation into clausal form introduces a significant overhead to the proof search and modifies the structure of the original formula. Translating a proof in clausal form back into a more readable non-clausal proof of the original formula is not straightforward. This paper presents a non-clausal automated theorem prover for classical first-order logic. It is based on a non-clausal connection calculus and implemented with a few lines of Prolog code. Working entirely on the original structure of the input formula yields not only a speed up of the proof search, but the resulting non-clausal proofs are also shorter.

scholarly journals EPR-based k-induction with Counterexample Guided Abstraction Refinement

10.29007/scv7 ◽  
2018 ◽  
Author(s):  
Zurab Khasidashvili ◽  
Konstantin Korovin ◽  
Dmitry Tsarkov
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Order Logic ◽  
Experimental Results ◽  
Theorem Prover ◽  
First Order Logic ◽  
Safety Properties ◽  
Abstraction Refinement ◽  
First Order ◽  
Automated Theorem Prover

In recent years it was proposed to encode bounded model checking (BMC) into the effectively propositional fragment of first-order logic (EPR). The EPR fragment can provide for a succinct representation of the problem and facilitate reasoning at a higher level.In this paper we present an extension of the EPR-based bounded model checkingwith k-induction which can be used to prove safety properties of systems overunbounded runs. We present a novel abstraction-refinement approach based onunsatisfiable cores and models (UCM) for BMC and k-induction in the EPR setting.We have implemented UCM refinements for EPR-based BMC and k-induction in a first-order automated theorem prover iProver. We also extended iProver with the AIGER format and evaluated it over the HWMCC'14 competition benchmarks. The experimental results are encouraging. We show that a number of AIG problems can be verified until deeper bounds with the EPR-based model checking.

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.

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 Checkable Proofs for First-Order Theorem Proving

10.29007/s6d1 ◽  
2018 ◽  
Author(s):  
Giles Reger ◽  
Martin Suda
Keyword(s):  
Theorem Proving ◽  
Critical Mass ◽  
Current Situation ◽  
Boolean Satisfiability ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Theorem Provers ◽  
Interactive Theorem Provers ◽  
Theory Reasoning

Inspired by the success of the DRAT proof format for certification of boolean satisfiability (SAT),we argue that a similar goal of having unified automatically checkable proofs should be soughtby the developers of automated first-order theorem provers (ATPs). This would not onlyhelp to further increase assurance about the correctness of prover results,but would also be indispensable for tools which rely on ATPs,such as ``hammers'' employed within interactive theorem provers.The current situation, represented by the TSTP format is unsatisfactory,because this format does not have a standardised semantics and thus cannot be checked automatically.Providing such semantics, however, is a challenging endeavour. One would ideallylike to have a proof format which covers only-satisfiability-preserving operations such as Skolemisationand is versatile enough to encompass various proving methods (i.e. not just superposition)or is perhaps even open ended towards yet to be conceived methods or at least easily extendable in principle.Going beyond pure first-order logic to theory reasoning in the style of SMT orbeyond proofs to certification of satisfiability are further interesting challenges.Although several projects have already provided partial solutions in this direction,we would like to use the opportunity of ARCADE to further promote the idea andgather critical mass needed for its satisfactory realisation.

Sign in / Sign up

Export Citation Format

Share Document