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

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.

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

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 Consistent Inference for Dialogue Relation Extraction

2021 ◽  
Author(s):  
Xinwei Long ◽  
Shuzi Niu ◽  
Yucheng Li
Keyword(s):  
Performance Improvement ◽  
Relation Extraction ◽  
Attention Mechanism ◽  
Order Logic ◽  
Experimental Results ◽  
First Order Logic ◽  
Specific Topic ◽  
Inference Method ◽  
First Order ◽  
Benchmark Datasets

Relation Extraction is key to many downstream tasks. Dialogue relation extraction aims at discovering entity relations from multi-turn dialogue scenario. There exist utterance, topic and relation discrepancy mainly due to multi-speakers, utterances, and relations. In this paper, we propose a consistent learning and inference method to minimize possible contradictions from those distinctions. First, we design mask mechanisms to refine utterance-aware and speaker-aware representations respectively from the global dialogue representation for the utterance distinction. Then a gate mechanism is proposed to aggregate such bi-grained representations. Next, mutual attention mechanism is introduced to obtain the entity representation for various relation specific topic structures. Finally, the relational inference is performed through first order logic constraints over the labeled data to decrease logically contradictory predicted relations. Experimental results on two benchmark datasets show that the F1 performance improvement of the proposed method is at least 3.3% compared with SOTA.

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

scholarly journals Superposition for Full Higher-order Logic

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.

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.

Sign in / Sign up

Export Citation Format

Share Document