Note: these tests are running on a shared server, so that times may vary between runs, and they are substantially [an order of magnitude] slower than on a comparable dedicated machine.
In some cases we have not sought to supply the shortest proof (from fewest premises), but have tested the prover's 'discernment' by supplying unneeded premises.
Note: A few of these tests are deliberate disproofs, as a check on soundness. These tests are positively proved invalid and are noted as such when they are run.
Tau accepts input in KIF (Knowledge Interchange Format), a first-order notation in ASCII. Documentation for KIF is found here:
See also a list of various axioms which may be pasted into the prover. Note that some proofs in Peano arithmetic and Presburger arithmetic require that Tau apply mathematical induction (see the checkbox) or use previously proved results, while others do not. We leave it as an exercise for the reader to determine which. See the Wikipedia articles, Peano arithmetic and Presburger arithmetic.
Montague, Richard and
Donald Kalish
Logic, Techniques of Formal Reasoning
New York, Harcourt, Brace and World, Inc., 1964.
Montague,
Richard , Kalish, Donald, and Mar, Gary (Ed. Robert Fogelin)
Logic: Techniques of Formal Reasoning
Harcourt Brace, New York, 1980
Thomas, James A.
Symbolic Logic
Charles E. Merrill Publishing Co., Columbus, Ohio, 1977
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Tests adapted from Enderton, Herbert B.
A Mathematical Introduction to Logic, 2nd Ed.
Harcourt Academic Press, New York, 2001
Simple Peano Arithmetic tests (no induction used)
Peano axioms:
(forall ?X (not (= 0 (succ ?X))))
(forall ?X (forall ?Y (=> (= (succ ?X) (succ ?Y)) (= ?X ?Y))))
(forall ?X (= (+ ?X 0) ?X))
(forall ?X (forall ?Y (= (+ ?X (succ ?Y)) (succ (+ ?X ?Y)))))
(forall ?X (forall ?Y (= (* 0 ?X) 0)))
(forall ?X (forall ?Y (= (* ?X (succ ?Y)) (+ (* ?X ?Y) ?X))))
|
|
|
|
|
|
|
|
|
|
|
|
Peano Arithmetic (PA, with mathematical induction)
Induction (all instances of):
(=> (and (F 0) (forall ?X (=> (F ?X) (F (succ ?X)))) (forall ?X (F ?X))))
Commutativity axioms (proved with induction):
(forall ?X (forall ?Y (= (+ ?X ?Y) (+ ?Y ?X))))
(forall ?X (forall ?Y (= (* ?X ?Y) (* ?Y ?X))))
|
|
|
|
|
|
Presburger Arithmetic (PrA)
(forall ?X (not (= 0 (succ ?X))))
(forall ?X (forall ?Y (=> (= (succ ?X) (succ ?Y)) (= ?X ?Y))))
(forall ?X (= (+ ?X 0) ?X))
(forall ?X (forall ?Y (= (+ ?X (succ ?Y)) (succ (+ ?X ?Y)))))
Induction (all instances of):
(=> (and (F 0) (forall ?X (=> (F ?X) (F (succ ?X)))) (forall ?X (F ?X)))) , where F represents any formula with one free variable.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Tests from Nolt, J. and D.
Rohatyn, A. Varzi
Schaum's Outline of Logic
McGraw-Hill, 1998
|
|
||||
|
|
|
|||
|
|
|
|
|
|
Commutative ordered field tests
From Kalish & Montague, 1st. ed. Chapter VIII page 280
See also Field
Axioms
|
|
|
|
|
|
|
|
|
|
|
|
TPTP tests
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Unresolved proof attempts (invalid, but unable to disprove directly)
|
|
|
|
|
|
Hard tests (currently unprovable within Tau's normal resource limits)
|
T329 (K&M) |
T328 (K&M) |
|
|
|
Do you have a good problem for us to test? Submit it here, in KIF or ?