scholarly journals Global Subsumption Revisited (Briefly)

10.29007/qcd7 ◽  
2018 ◽  
Author(s):  
Giles Reger ◽  
Martin Suda
Keyword(s):  
Initial Problem ◽  
Theorem Prover ◽  
General Idea ◽  
Practical Implementation ◽  
Global Approach ◽  
Smt Solver ◽  
First Order ◽  
Theorem Provers ◽  
Sat Solver

Global subsumption is an existing simplification technique for saturation-based first-order theorem provers. The general idea is that we can replace a clause C by its subclause D if D follows from the initial problem as D will subsume C. The effectiveness of the technique comes from a cheap, global approach for (incompletely) checking whether D is a consequence of the initial problem. The idea is to produce and maintain a set S of ground clauses that follow from the input (e.g. grounded versions of all derived clauses) and to check whether a grounding of D follows from this set. As this is now a propositional problem this check can be performed by a SAT solver, making it efficient. In this paper we review the global subsumption technique and pose a number of questions related to the practical implementation of global subsumption and possible variations of the approach. We consider, for example, which groundings to place in S, how to select the subclause(s) D to check, how to integrate this technique with the AVATAR approach and whether it makes sense to replace the SAT solver with an SMT solver. This discussion takes place within the context of the Vampire theorem prover.

scholarly journals AVATAR Modulo Theories

10.29007/k6tp ◽  
2018 ◽  
Author(s):  
Giles Reger ◽  
Nikolaj Bjorner ◽  
Martin Suda ◽  
Andrei Voronkov
Keyword(s):  
Theorem Proving ◽  
Satisfiability Modulo Theories ◽  
Theorem Prover ◽  
Ground Theory ◽  
Smt Solver ◽  
First Order ◽  
Proof Search ◽  
Smt Solvers ◽  
Sat Solver ◽  
A New Technique

This paper introduces a new technique for reasoning with quantifiers and theories. Traditionally, first-order theorem provers (ATPs) are well suited to reasoning with first-order problems containing many quantifiers and satisfiability modulo theories (SMT) solvers are well suited to reasoning with first-order problems in ground theories such as arithmetic. A recent development in first-order theorem proving has been the AVATAR architecture which uses a SAT solver to guide proof search based on a propositional abstraction of the first-order clause space. The approach turns a single proof search into a sequence of proof searches on (much) smaller sub-problems. This work extends the AVATAR approach to use a SMT solver in place of the SAT solver, with the effect that the first-order solver only needs to consider ground-theory-consistent sub-problems. The new architecture has been implemented using the Vampire theorem prover and Z3 SMT solver. Our experimental results, and the results of recent competitions, show that such a combination can be highly effective.

scholarly journals SAT solving experiments in Vampire

10.29007/5l47 ◽  
2018 ◽  
Author(s):  
Armin Biere ◽  
Ioan Dragan ◽  
Laura Kovács ◽  
Andrei Voronkov
Keyword(s):  
State Of The Art ◽  
Theorem Prover ◽  
Sat Solving ◽  
First Order ◽  
Automated Theorem Prover ◽  
Sat Solver ◽  
Overall Performance

In order to better understand how well a state of the art SAT solver would behave in the framework of a first-order automated theorem prover we have decided to integrate Lingeling, best performing SAT solver, inside Vampire’s AVATAR framework. In this paper we propose two ways of integrating a SAT solver inside of Vampire and evaluate overall performance of this combination. Our experiments show that by using a state of the art SAT solver in Vampire we manage to solve more problems. Surprisingly though, there are cases where combination of the two solvers does not always prove to generate best results.

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 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 Aiming for the Goal with SInE

10.29007/q4pt ◽  
2020 ◽  
Author(s):  
Martin Suda
Keyword(s):  
Experimental Evaluation ◽  
Main Idea ◽  
Inference Engine ◽  
Theorem Prover ◽  
Selection Algorithm ◽  
First Order ◽  
Theorem Provers ◽  
The Individual ◽  
Goal Distance ◽  
Automatic Theorem

The Sumo INference Engine (SInE) is a well-established premise selection algorithm for first-order theorem provers, routinely used, especially on large theory problems. The main idea of SInE is to start from the goal formula and to iteratively add other formulas to those already added that are related by sharing signature symbols. This implicitly defines a certain heuristical distance of the individual formulas and symbols from the goal.In this paper, we show how this distance can be successfully used for other purposes than just premise selection. In particular, biasing clause selection to postpone introduction of input clauses further from the goal helps to solve more problems. Moreover, a precedence which respects such goal distance of symbols gives rise to a goal sensitive simplification ordering. We implemented both ideas in the automatic theorem prover Vampire and present their experimental evaluation on the TPTP benchmark.

scholarly journals GridTPT: a distributed platform for Theorem Prover Testing

10.29007/hk8w ◽  
2018 ◽  
Author(s):  
Thomas Bouton ◽  
Diego Caminha ◽  
David Déharbe ◽  
Pascal Fontaine
Keyword(s):  
Open Source ◽  
Future Development ◽  
Theorem Prover ◽  
Complex Task ◽  
Smt Solver ◽  
Requirement Specification ◽  
Open Source Tool ◽  
Theorem Provers ◽  
Distributed Platform ◽  
Implementation Resources

Programming provers is a complex task; completeness or even soundness may often be broken by apparently harmless bugs. A good testing platform can contribute in detecting problems early and helping development. This paper presents GridTPT, the distributed platform for testing the verit SMT solver. Its features are fairly standard, but it allows to easily distribute the task in a cluster.We plan to make this platform available as an open source tool for the community of developers of automated theorem provers. This presentation to PAAR'2010 will provide the opportunity to discuss the need for such a tool and the necessary features in a broader context. We would like to extract a requirement specification from this discussion, that would be useful to get dedicated implementation resources for distribution, maintenance and future development of GridTPT.

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 An Inference Rule for the Acyclicity Property of Term Algebras

10.29007/tlw4 ◽  
2018 ◽  
Author(s):  
Simon Robillard
Keyword(s):  
Computer Science ◽  
Inference Rule ◽  
Theorem Prover ◽  
Science Reasoning ◽  
First Order ◽  
Theorem Provers ◽  
Smt Solvers ◽  
Indexing Technique ◽  
Superposition Calculus

Term algebras are important structures in many areas of mathematics and computer science. Reasoning about their theories in superposition-based first-order theorem provers is made difficult by the acyclicity property of terms, which is not finitely axiomatizable. We present an inference rule that extends the superposition calculus and allows reasoning about term algebras without axioms to describe the acyclicity property. We detail an indexing technique to efficiently apply this rule in problems containing a large number of clauses. Finally we experimentally evaluate an implementation of this extended calculus in the first-order theorem prover Vampire. The results show that this technique is able to find proofs for difficult problems that existing SMT solvers and first-order theorem provers are unable to solve.

scholarly journals Local proofs and AVATAR

10.29007/qgdk ◽  
2018 ◽  
Author(s):  
Giles Reger ◽  
Martin Suda
Keyword(s):  
Experimental Results ◽  
Theorem Prover ◽  
First Order ◽  
Theorem Provers

With first-order interpolation as the application in mind, we study the problem of gen- erating local proofs in theorem provers employing the AVATAR architecture. The theory is complemented by experimental results based on our implementation of the techniques in theorem prover Vampire.

scholarly journals The Challenges of Evaluating a New Feature in Vampire

10.29007/1ffk ◽  
2018 ◽  
Author(s):  
Giles Reger ◽  
Martin Suda ◽  
Andrei Voronkov
Keyword(s):  
Experimental Results ◽  
New Method ◽  
Smt Solver ◽  
First Order ◽  
Theorem Provers ◽  
New Feature ◽  
Superposition Theorem

This paper presents and explores experimental results examining the usage of AVATAR (Advanced Vampire Architecture for Theories and Resolution). This architecture introduces a new method for splitting in first-order resolution and superposition theorem provers that makes use of a SAT (or SMT) solver to make splitting decisions. The architecture (as implemented in Vampire) has many options and components that can be varied and this paper explores the effects of these variations on the performance of the prover.

Sign in / Sign up

Export Citation Format

Share Document