scholarly journals Reasoning About Loops Using Vampire

10.29007/tcvj ◽  
2018 ◽  
Author(s):  
Laura Kovács ◽  
Simon Robillard
Keyword(s):  
Order Logic ◽  
Theorem Prover ◽  
Program Correctness ◽  
Command Language ◽  
Rule Based ◽  
Invariant Generation ◽  
Partial Correctness ◽  
First Order ◽  
Deductive Systems ◽  
Fully Automatic

In 2009, the symbol elimination method for loop invariant generationwas introduced, which used saturationtheorem proving in first-order logic to generate quantified invariantsof programs with arrays. Symbol elimination is fully automatic,requires no user guidance, and it is the first ever approach able togenerate invariants with alternations of quantifiers. In this paperwe describe a number of improvements and extensions to symbolelimination and invariant generation using first-order theoremproving, in particular the Vampire theorem prover. Rather than beinglimited to a specific programming language, our approach to reasoningabout loops in Vampire relies on a simple guarded command language forits input, which can be used as an interface for more complex andrealistic imperative languages. We propose new ways for extendingquantified loop properties describing valid loop properties, bysimplifying the properties over array updates and next staterelations. We also extend symbol elimination with pre- andpost-conditions of loops. We use the loop specification to generateonly invariants that are relevant, that is, invariants that are neededfor proving partial correctness of loops. Further, we turn symbolelimination into an automatic approach proving program correctness,providing an alternative method to Hoare-rule based loop verificationor other deductive systems. We present our newly redesignedimplementation of loop reasoning in Vampire and also report onexperimental 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 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.

Topos-theoretic background

2018 ◽  
Author(s):  
Olivia Caramello
Keyword(s):  
Category Theory ◽  
Order Theory ◽  
Order Logic ◽  
Basic Theory ◽  
First Order Logic ◽  
Syntactic Category ◽  
First Order ◽  
Deductive Systems ◽  
First Order Theory ◽  
Categorical Semantics

This chapter provides the topos-theoretic background necessary for understanding the contents of the book; the presentation is self-contained and only assumes a basic familiarity with the language of category theory. The chapter begins by reviewing the basic theory of Grothendieck toposes, including the fundamental equivalence between geometric morphisms and flat functors. Then it presents the notion of first-order theory and the various deductive systems for fragments of first-order logic that will be considered in the course of the book, notably including that of geometric logic. Further, it discusses categorical semantics, i.e. the interpretation of first-order theories in categories possessing ‘enough’ structure. Lastly, the key concept of syntactic category of a first-order theory is reviewed; this notion will be used in Chapter 2 for constructing classifying toposes of geometric theories.

Principles and practice in verifying rule-based systems

1992 ◽  
Vol 7 (2) ◽  
pp. 115-141 ◽  
Author(s):  
Alun D. Preece ◽  
Rajjan Shinghal ◽  
Aïda Batarekh
Keyword(s):  
Expert System ◽  
Knowledge Base ◽  
State Of The Art ◽  
Knowledge Bases ◽  
Order Logic ◽  
First Order Logic ◽  
Rule Based ◽  
First Order ◽  
Rule Bases ◽  
System Knowledge

AbstractThis paper surveys the verification of expert system knowledge bases by detecting anomalies. Such anomalies are highly indicative of errors in the knowledge base. The paper is in two parts. The first part describes four types of anomaly: redundancy, ambivalence, circularity, and deficiency. We consider rule bases which are based on first-order logic, and explain the anomalies in terms of the syntax and semantics of logic. The second part presents a review of five programs which have been built to detect various subsets of the anomalies. The four anomalies provide a framework for comparing the capabilities of the five tools, and we highlight the strengths and weaknesses of each approach. This paper therefore provides not only a set of underlying principles for performing knowledge base verification through anomaly detection, but also a survey of the state-of-the-art in building practical tools for carrying out such verification. The reader of this paper is expected to be familiar with first-order logic.

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.

Sign in / Sign up

Export Citation Format

Share Document