Automated Generation of Consistent Graph Models with First-Order Logic Theorem Provers

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.

Download Full-text

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.

Download Full-text

SGGS Theorem Proving: an Exposition

10.29007/m2vf ◽

2018 ◽

Author(s):

Maria Paola Bonacina ◽

David Plaisted

Keyword(s):

Theorem Proving ◽

Order Logic ◽

First Order Logic ◽

Candidate Model ◽

Narrative Style ◽

First Order ◽

The Core ◽

Theorem Provers ◽

Instance Generation ◽

Main Ideas

We present in expository style the main ideas in SGGS, which stands for Semantically-Guided Goal-Sensitive theorem proving. SGGS uses sequences of constrained clauses to represent models, instance generation to go from a candidate model to the next, and resolution as well as other inferences to repair the model. SGGS is refutationally complete for first-order logic, DPLL-style model based, semantically guided, goal sensitive, and proof confluent, which appears to be a rare combination of features. In this paper we describe the core of SGGS in a narrative style, emphasizing ideas and trying to keep technicalities to a minimum, in order to advertise it to builders and users of theorem provers.

Download Full-text

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.

Download Full-text

Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics

10.29007/cpbz ◽

2018 ◽

Author(s):

Damien Doligez ◽

Jael Kriener ◽

Leslie Lamport ◽

Tomer Libal ◽

Stephan Merz

Keyword(s):

Modal Logic ◽

Modal Logics ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Propositional Modal Logic ◽

Theorem Provers ◽

Syntactic Abstraction

We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic.

Download Full-text

Superposition for Full Higher-order Logic

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

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

2021 ◽

pp. 396-412

Author(s):

Alexander Bentkamp ◽

Jasmin Blanchette ◽

Sophie Tourret ◽

Petar Vukmirović

Keyword(s):

Higher Order ◽

Order Logic ◽

First Order Logic ◽

Stepping Stones ◽

Higher Order Logic ◽

First Order ◽

Theorem Provers ◽

New Challenges

AbstractWe recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free $$\lambda $$ λ -superposition and superposition for first-order logic with interpreted Booleans. Stepping on these stones, we finally reach a sound and refutationally complete calculus for higher-order logic with polymorphism, extensionality, Hilbert choice, and Henkin semantics. In addition to the complexity of combining the calculus’s two predecessors, new challenges arise from the interplay between $$\lambda $$ λ -terms and Booleans. Our implementation in Zipperposition outperforms all other higher-order theorem provers and is on a par with an earlier, pragmatic prototype of Booleans in Zipperposition.

Download Full-text

Evaluating Automated Theorem Provers Using Adimen-SUMO

10.29007/hplh ◽

2018 ◽

Author(s):

Javier Álvez ◽

Paqui Lucio ◽

German Rigau

Keyword(s):

Order Logic ◽

Experimental Results ◽

First Order Logic ◽

First Order ◽

Theorem Provers ◽

Small Set

We report on the results of evaluating the performance automated theorem provers using \ADIMENSUMO{}. The evaluation follows the adaptation of the methodology based on competency questions \cite{GrF95} to the framework of first-order logic, which is presented in \cite{ALR15}, and is applied to \ADIMENSUMO{} \cite{ALR12}. The set of competency questions used for this evaluation has been semi-automatically generated from a small set of semantic patterns and the mapping of \WORDNET{} to \SUMO{}, also introduced in \cite{ALR15}. Our experimental results demonstrate that improved versions of the proposed set of competency questions could be really valuable for the development of automated theorem provers.

Download Full-text

Automatic white-box testing of first-order logic ontologies

Journal of Logic and Computation ◽

10.1093/logcom/exz001 ◽

2019 ◽

Vol 29 (5) ◽

pp. 723-751

Author(s):

Javier Álvez ◽

Montserrat Hermo ◽

Paqui Lucio ◽

German Rigau

Keyword(s):

Automated Reasoning ◽

Computational Cost ◽

Order Logic ◽

First Order Logic ◽

Automated Generation ◽

First Order ◽

Formal Ontologies ◽

Expected Information ◽

Fully Automatic ◽

White Box Testing

AbstractFormal ontologies are axiomatizations in a logic-based formalism. The development of formal ontologies is generating considerable research on the use of automated reasoning techniques and tools that help in ontology engineering. One of the main aims is to refine and to improve axiomatizations for enabling automated reasoning tools to efficiently infer reliable information. Defects in the axiomatization cannot only cause wrong inferences, but can also hinder the inference of expected information, either by increasing the computational cost of or even preventing the inference. In this paper, we introduce a novel, fully automatic white-box testing framework for first-order logic (FOL) ontologies. Our methodology is based on the detection of inference-based redundancies in the given axiomatization. The application of the proposed testing method is fully automatic since (i) the automated generation of tests is guided only by the syntax of axioms and (ii) the evaluation of tests is performed by automated theorem provers (ATPs). Our proposal enables the detection of defects and serves to certify the grade of suitability—for reasoning purposes—of every axiom. We formally define the set of tests that are (automatically) generated from any axiom and prove that every test is logically related to redundancies in the axiom from which the test has been generated. We have implemented our method and used this implementation to automatically detect several non-trivial defects that were hidden in various FOL ontologies. Throughout the paper we provide illustrative examples of these defects, explain how they were found and how each proof—given by an ATP—provides useful hints on the nature of each defect. Additionally, by correcting all the detected defects, we have obtained an improved version of one of the tested ontologies: Adimen-SUMO.

Download Full-text