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 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 Dolius: A Distributed Parallel SAT Solving Framework

10.29007/hvqt ◽  
2018 ◽  
Author(s):  
Gilles Audemard ◽  
Benoît Hoessen ◽  
Saïd Jabbour ◽  
Cédric Piette
Keyword(s):  
Shared Memory ◽  
State Of The Art ◽  
Divide And Conquer ◽  
Sat Solving ◽  
Sat Solvers ◽  
Sat Solver

Over the years, parallel SAT solving becomes more and more important. However, most of state-of-the-art parallel SAT solvers are portfolio-based ones. They aim at running several times the same solver with different parameters. In this paper, we propose a tool called Dolius, mainly based on the divide and conquer paradigm. In contrast to most current parallel efficient engines, Dolius does not need shared memory, can be distributed, and scales well when a large number of computing units is available. Furthermore, our tool contains an API allowing to plug any SAT solver in a simple way.

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 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 Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic

10.29007/dzc2 ◽  
2018 ◽  
Author(s):  
Max Wisniewski ◽  
Alexander Steen
Keyword(s):  
Modal Logic ◽  
Higher Order ◽  
Order Logic ◽  
Tense Logic ◽  
Theorem Prover ◽  
Higher Order Logic ◽  
First Order ◽  
Automated Theorem Prover ◽  
Nominal Logic ◽  
The Moment

In this paper, we present an embedding of higher-order nominal modal logicinto classical higher-order logic, and study its automation. There exists no automated theorem prover for first-order or higher-order nominal logic at the moment, hence, this is the first automation for this kind of logic.In our work, we focus on nominal tense logic and have successfully proven some first theorems.

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 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 Light-Weight Integration of SAT Solving into First-Order Reasoners – First Experiments

10.29007/89kc ◽  
2018 ◽  
Author(s):  
Stephan Schulz
Keyword(s):  
Search Space ◽  
Light Weight ◽  
Sat Solving ◽  
First Order ◽  
Proof Search ◽  
Sat Solver

We describe a light-weight integration of the propositional SAT solver PicoSAT and the saturation-based superposition prover E. The proof search is driven by the saturation prover. Periodically, the saturation is interrupted, and all first-order clauses are grounded. The resulting ground problem is converted to a propositional format and handed to the SAT solver. If the SAT solver reports unsatisfiability, the proof is extracted and reported on the first-order level. First experiments demonstrate the viability of the approach and suggest future extensions. They also yield interesting information about the structure of the search space.

Sign in / Sign up

Export Citation Format

Share Document