scholarly journals Redirecting Proofs by Contradiction

10.29007/wm8b ◽  
2018 ◽  
Author(s):  
Jasmin Christian Blanchette
Keyword(s):  
Natural Deduction ◽  
Direct Proof ◽  
Theorem Prover ◽  
Automatic Theorem

This paper presents an algorithm that redirects proofs by contradiction. The input is a refutation graph, as produced by an automatic theorem prover (e.g., E, SPASS, Vampire, Z3); the output is a direct proof expressed in natural deduction extended with case analyses and nested subproofs. The algorithm is implemented in Isabelle’s Sledgehammer, where it enhances the legibility of machine-generated proofs.

scholarly journals A Fully Automatic Theorem Prover with Human-Style Output

2016 ◽  
Vol 58 (2) ◽  
pp. 253-291 ◽  
Author(s):  
M. Ganesalingam ◽  
W. T. Gowers
Keyword(s):  
Theorem Prover ◽  
Fully Automatic ◽  
Automatic Theorem

Gentzen's Proof of Normalization for Natural Deduction

2008 ◽  
Vol 14 (2) ◽  
pp. 240-257 ◽  
Author(s):  
Jan von Plato
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Direct Proof ◽  
Cut Elimination ◽  
Doctoral Thesis ◽  
Detailed Proof ◽  
Normalization Theorem ◽  
The One ◽  
The Right ◽  
Special Case

AbstractGentzen writes in the published version of his doctoral thesis Untersuchungen über das logische Schliessen (Investigations into logical reasoning) that he was able to prove the normalization theorem only for intuitionistic natural deduction, but not for classical. To cover the latter, he developed classical sequent calculus and proved a corresponding theorem, the famous cut elimination result. Its proof was organized so that a cut elimination result for an intuitionistic sequent calculus came out as a special case, namely the one in which the sequents have at most one formula in the right, succedent part. Thus, there was no need for a direct proof of normalization for intuitionistic natural deduction. The only traces of such a proof in the published thesis are some convertibilities, such as when an implication introduction is followed by an implication elimination [1934–35, II.5.13]. It remained to Dag Prawitz in 1965 to work out a proof of normalization. Another, less known proof was given also in 1965 by Andres Raggio.We found in February 2005 an early handwritten version of Gentzen's thesis, with exactly the above title, but with rather different contents: Most remarkably, it contains a detailed proof of normalization for what became the standard system of natural deduction. The manuscript is located in the Paul Bernays collection at the ETH-Zurichwith the signum Hs. 974: 271. Bernays must have gotten it well before the time of his being expelled from Göttingen on the basis of the racial laws in April 1933.

scholarly journals Improving ENIGMA-style Clause Selection while Learning From History

2021 ◽  
pp. 543-561
Author(s):  
Martin Suda
Keyword(s):  
Neural Network ◽  
Real Time ◽  
Theorem Prover ◽  
Central Idea ◽  
Theorem Provers ◽  
Recursive Neural Network ◽  
Time Evaluation ◽  
Automatic Theorem ◽  
Learning From History

AbstractWe re-examine the topic of machine-learned clause selection guidance in saturation-based theorem provers. The central idea, recently popularized by the ENIGMA system, is to learn a classifier for recognizing clauses that appeared in previously discovered proofs. In subsequent runs, clauses classified positively are prioritized for selection. We propose several improvements to this approach and experimentally confirm their viability. For the demonstration, we use a recursive neural network to classify clauses based on their derivation history and the presence or absence of automatically supplied theory axioms therein. The automatic theorem prover Vampire guided by the network achieves a 41 % improvement on a relevant subset of SMT-LIB in a real time evaluation.

scholarly journals Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions

2012 ◽  
Vol 50 (1) ◽  
pp. 99-117 ◽  
Author(s):  
James P. Bridge ◽  
Lawrence Charles Paulson
Keyword(s):  
Special Functions ◽  
Theorem Prover ◽  
Automatic Theorem

Implicational logics in natural deduction systems

1982 ◽  
Vol 47 (1) ◽  
pp. 184-186 ◽  
Author(s):  
E.G.K. López-Escobar
Keyword(s):  
Natural Deduction ◽  
Short Note ◽  
Direct Proof ◽  
Modus Ponens ◽  
Implicational Logics

In 1959 M. Dummett [3] introduced the logic LC obtained by adding the axiom ACpqCqp to the formalization of the intuitionistic prepositional calculus having modus ponens and substitution as its rules of inference. Later on R. A. Bull [1] showed, by quite a roundabout way, that the implicational theses of LC were precisely the theses of the implicational calculus obtained by adding the axiom CCCpqrCCCqprr to the system of positive implication. In 1964 Bull [2] gave another proof, this time using results of Birkhoff concerning subdirectly reducible algebras.The aim of this short note is to emphasize that the use of Gentzen's natural deduction systems (see Prawitz [4]) allows us to give a much more direct proof.

scholarly journals Aiming for the Goal with SInE

10.29007/q4pt ◽  
2020 ◽  
Author(s):  
Martin Suda
Keyword(s):  
Experimental Evaluation ◽  
Main Idea ◽  
Inference Engine ◽  
Theorem Prover ◽  
Selection Algorithm ◽  
First Order ◽  
Theorem Provers ◽  
The Individual ◽  
Goal Distance ◽  
Automatic Theorem

The Sumo INference Engine (SInE) is a well-established premise selection algorithm for first-order theorem provers, routinely used, especially on large theory problems. The main idea of SInE is to start from the goal formula and to iteratively add other formulas to those already added that are related by sharing signature symbols. This implicitly defines a certain heuristical distance of the individual formulas and symbols from the goal.In this paper, we show how this distance can be successfully used for other purposes than just premise selection. In particular, biasing clause selection to postpone introduction of input clauses further from the goal helps to solve more problems. Moreover, a precedence which respects such goal distance of symbols gives rise to a goal sensitive simplification ordering. We implemented both ideas in the automatic theorem prover Vampire and present their experimental evaluation on the TPTP benchmark.

scholarly journals A subsumption architecture for theorem proving?

1994 ◽  
Vol 349 (1689) ◽  
pp. 71-85 ◽  
Keyword(s):  
Theorem Proving ◽  
Reaction Times ◽  
Theorem Prover ◽  
Fast Reaction ◽  
Simple Task ◽  
Subsumption Architecture ◽  
Efficient Alternative ◽  
Traditional Approaches ◽  
Automatic Theorem ◽  
Resolution Theorem Proving

Brooks has criticized traditional approaches to artificial intelligence as too inefficient. In particular, he has singled out techniques involving search as inadequate to achieve the fast reaction times required by robots and other AI products that need to work in the real world. Instead he proposes the subsumption architecture as an overall organizing principle. This consists of layers of behavioural modules, each of which is capable of carrying out a complete (usually simple) task. He has employed this architecture to build a series of simple mobile robots, but he claims that it is appropriate for all AI products. Brooks’s proposal is usually seen as an example of nouvelle AI, in contrast to good old-fashioned AI (GOFAl). Automatic theorem proving is the archetypal example of GOFAl. The resolution theorem proving technique once served as the engine of AI. Of all areas of AI it seems the most difficult to implement using Brooks’s ideas. It would thus serve as a keen test of Brooks’s proposal to explore to what extent the task of theorem proving can be achieved by a subsumption architecture. Tactics are programs for guiding a theorem prover. They were introduced as an efficient alternative to search-based techniques. In this paper I compare recent work on tactic-based theorem proving with Brooks’s proposals and show that, surprisingly, there is a similarity between them. It thus seems that the distinction between nouvelle AI and GOFAl is not so great as is sometimes claimed. However, this exercise also identifies some criticisms of Brooks’s proposal.

Sign in / Sign up

Export Citation Format

Share Document