scholarly journals The Uses of SAT Solvers in Vampire

10.29007/4w68 ◽  
2018 ◽  
Author(s):  
Giles Reger ◽  
Martin Suda
Keyword(s):  
Data Structures ◽  
Theorem Prover ◽  
Worst Case ◽  
Running Time ◽  
First Order ◽  
Sat Solvers ◽  
Memory Overhead ◽  
Complex Term

Reasoning in a saturation-based first-order theorem prover is generally expensive involving complex term-indexing data structures and inferences such as subsumption resolution whose (worst case) running time is exponential in the length of the clause. In contrast, SAT solvers are very cheap, being able to solve large problems quickly and with relatively little memory overhead.Consequently, utilising this cheap power within Vampire to carry out certain tasks has proven highly successful. We give an overview of the different ways that SAT solvers are utilisedwithin Vampire and discuss further ways in which this usage could be extended

PAL – Propositional Algorithmic Logic

1981 ◽  
Vol 4 (3) ◽  
pp. 675-760
Author(s):  
Grażyna Mirkowska
Keyword(s):  
Data Structures ◽  
Completeness Theorem ◽  
Natural Numbers ◽  
First Order ◽  
Algorithmic Logic ◽  
Axiomatic Systems ◽  
Nondeterministic Program ◽  
Basic Sets

The aim of propositional algorithmic logic is to investigate the properties of program connectives. Complete axiomatic systems for deterministic as well as for nondeterministic interpretations of program variables are presented. They constitute basic sets of tools useful in the practice of proving the properties of program schemes. Propositional theories of data structures, e.g. the arithmetic of natural numbers and stacks, are constructed. This shows that in many aspects PAL is close to first-order algorithmic logic. Tautologies of PAL become tautologies of algorithmic logic after replacing program variables by programs and propositional variables by formulas. Another corollary to the completeness theorem asserts that it is possible to eliminate nondeterministic program variables and replace them by schemes with deterministic atoms.

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 Optimal Purely Functional Priority Queues

1996 ◽  
Vol 3 (37) ◽  
Author(s):  
Gerth Stølting Brodal ◽  
Chris Okasaki
Keyword(s):  
Data Structure ◽  
Higher Order ◽  
Priority Queues ◽  
Worst Case ◽  
Minimum Element ◽  
Asymptotically Optimal ◽  
Running Time ◽  
Recursive Structures ◽  
Functional Setting

Brodal recently introduced the first implementation of imperative priority queues to support findMin, insert, and meld in O(1) worst-case time, and deleteMin in O(log n) worst-case time. These bounds are asymptotically optimal among all comparison-based priority queues. In this paper, we adapt<br />Brodal's data structure to a purely functional setting. In doing so, we both simplify the data structure and clarify its relationship to the binomial queues of Vuillemin, which support all four operations in O(log n) time. Specifically, we derive our implementation from binomial queues in three steps: first, we reduce the running time of insert to O(1) by eliminating the possibility of cascading links; second, we reduce the running time of findMin to O(1) by adding a global root to hold the minimum element; and finally, we reduce the running time of meld to O(1) by allowing priority queues to contain other<br />priority queues. Each of these steps is expressed using ML-style functors. The last transformation, known as data-structural bootstrapping, is an interesting<br />application of higher-order functors and recursive structures.

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

Water Sport Tow Ropes

2009 ◽  
Author(s):  
Ralph L. Barnett ◽  
Adam A. E. Ziemba
Keyword(s):  
Mechanical Properties ◽  
Grip Strength ◽  
Case Scenario ◽  
Worst Case ◽  
Impact Speed ◽  
First Order ◽  
Water Sport ◽  
Water Sports ◽  
System Geometry ◽  
Stiffness Criterion

With the exception of tubing, towed water sports are afflicted by “wipeouts” that cause the athlete to release the handle of the tow rope. Once released, the resilience of the tow rope allows the rope and handle to spring toward the motorboat with the potential for overtaking the craft and impacting its crew. This paper examines this safety problem; specifically, it analyzes the wakeboard which subsumes water skiing, slaloming, kneeboarding and barefooting. A first order formulation is developed for describing the tow handle trajectory in terms of the system geometry, the skier’s grip strength and the mechanical properties of the tow rope. A rope stiffness criterion is established that guarantees the released tow handle will fall harmlessly into the water as opposed to striking the motorboat. The handle fight time and maximum impact speed are predicted for a worst case scenario. Further, the formulation provides a guideline for refining its conservative predictions by testing rope candidates.

Sign in / Sign up

Export Citation Format

Share Document