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 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 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 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 Making Higher-Order Superposition Work

2021 ◽  
pp. 415-432
Author(s):  
Petar Vukmirović ◽  
Alexander Bentkamp ◽  
Jasmin Blanchette ◽  
Simon Cruanes ◽  
Visa Nummelin ◽  
...  
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
First Order Logic ◽  
Inference Rules ◽  
Higher Order Logic ◽  
First Order ◽  
New Challenges

AbstractSuperposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about formulas, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.

scholarly journals “Most of” leads to undecidability: Failure of adding frequencies to LTL

2021 ◽  
pp. 82-101
Author(s):  
Bartosz Bednarczyk ◽  
Jakub Michaliszyn
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Temporal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Statistical Reasoning ◽  
First Order ◽  
High Interest ◽  
The Past ◽  
Influence Networks

AbstractLinear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However, despite the high interest in the logic in recent years, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition, or that $$\sigma $$ σ is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately, as we prove in the paper, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation, and discuss how the undecidability results transfer to first-order logic on words.

AUTOMATED TERMINATION IN MODEL-CHECKING MODULO THEORIES

2013 ◽  
Vol 24 (02) ◽  
pp. 211-232 ◽  
Author(s):  
ALESSANDRO CARIONI ◽  
SILVIO GHILARDI ◽  
SILVIO RANISE
Keyword(s):  
Model Checking ◽  
Sufficient Conditions ◽  
Order Logic ◽  
Satisfiability Modulo Theories ◽  
First Order Logic ◽  
Reachability Problem ◽  
First Order ◽  
Recent Advances ◽  
Infinite State Systems ◽  
Infinite State

We identify sufficient conditions to automatically establish the termination of a backward reachability procedure for infinite state systems by using well-quasi-orderings. Besides showing that backward reachability succeeds on many instances of problems covered by general termination results, we argue that it could predict termination also on interesting instances of the reachability problem that are outside the scope of applicability of such general results. We work in the declarative framework of Model Checking Modulo Theories that permits us to exploit recent advances in Satisfiability Modulo Theories solving and model-theoretic notions of first-order logic.

Sign in / Sign up

Export Citation Format

Share Document