scholarly journals SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment

2020 ◽  
Vol 64 (3) ◽  
pp. 611-640
Author(s):  
Andreas Teucke ◽  
Christoph Weidenbach
Keyword(s):  
Theorem Prover ◽  
First Order ◽  
Linear Fragment

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 Deep Network Guided Proof Search

10.29007/8mwc ◽  
2018 ◽  
Author(s):  
Sarah Loos ◽  
Geoffrey Irving ◽  
Christian Szegedy ◽  
Cezary Kaliszyk
Keyword(s):  
Deep Learning ◽  
Program Analysis ◽  
Network Models ◽  
Theorem Prover ◽  
Neural Network Models ◽  
Two Phase ◽  
First Order ◽  
Proof Search ◽  
System Verification ◽  
Theory Reasoning

Deep learning techniques lie at the heart of several significant AI advances in recent years including object recognition and detection, image captioning, machine translation, speech recognition and synthesis, and playing the game of Go.Automated first-order theorem provers can aid in the formalization and verification of mathematical theorems and play a crucial role in program analysis, theory reasoning, security, interpolation, and system verification.Here we suggest deep learning based guidance in the proof search of the theorem prover E. We train and compare several deep neural network models on the traces of existing ATP proofs of Mizar statements and use them to select processed clauses during proof search. We give experimental evidence that with a hybrid, two-phase approach, deep learning based guidance can significantly reduce the average number of proof search steps while increasing the number of theorems proved.Using a few proof guidance strategies that leverage deep neural networks, we have found first-order proofs of 7.36% of the first-order logic translations of the Mizar Mathematical Library theorems that did not previously have ATP generated proofs. This increases the ratio of statements in the corpus with ATP generated proofs from 56% to 59%.

scholarly journals Topical Neural Theorem Prover that Induces Rules

10.29007/wscr ◽  
2020 ◽  
Author(s):  
Shuang Xia ◽  
Krysia Broda ◽  
Alessandra Russo
Keyword(s):  
Knowledge Base ◽  
Predictive Accuracy ◽  
Theorem Prover ◽  
Computational Time ◽  
Backward Chaining ◽  
First Order ◽  
Computation Tree ◽  
Computation Trees ◽  
Reasoning Mechanism ◽  
The Given

Various sub-symbolic approaches for reasoning and learning have been proposed in the literature. Among these approaches, the neural theorem prover (NTP) approach uses a backward chaining reasoning mechanism to guide a machine learning architecture to learn vector embedding representations of predicates and to induce first-order clauses from a given knowledge base. NTP is however known for being not scalable, as the computation trees generated by the backward chaining process can grow exponentially with the size of the given knowledge base. In this paper we address this limitation by extending the NTP approach with a topic-based method for controlling the induction of first-order clauses. Our proposed approach, called TNTP for Topical NTP, identifies topic-based clusters over a large knowledge-base and uses these clusters to control the soft unification of predicates during the learning process with the effect of reducing the size of the computation tree needed to induce first-order clauses. Our TNTP framework is capable of learning a diverse set of induced rules that have improved predictive accuracy, whilst reducing the computational time by several orders of magnitude. We demonstrated this by evaluating our approach on three different datasets (UMLS, Kinship and Nations) and comparing our results with that of the NTP method, chosen here as our baseline.

scholarly journals Understanding LEO-II’s proofs

10.29007/x9c9 ◽  
2018 ◽  
Author(s):  
Nik Sultana ◽  
Christoph Benzmüller
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Higher Order ◽  
Target Audience ◽  
Theorem Prover ◽  
First Order

The LEO and LEO-II provers have pioneered the integration of higher-order and first-order automated theorem proving. To date, the LEO-II system is, to our knowledge, the only automated higher-order theorem prover which is capable of generating joint higher-order–first-order proof objects in TPTP format. This paper discusses LEO-II’s proof objects. The target audience are practitioners with an interest in using LEO-II proofs within other systems.

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

Sign in / Sign up

Export Citation Format

Share Document