In this directory I have collected a number of experiments with a prover based on coherent logic. For any experiment : .in contains the input .p contains the input in TPTP format .out contains the output .prf contains an intermediate proof format .v contains a Coq (version 8) script of the proof .vo contains a Coq (version 8) compiled proof ----------------------------------------------------------------- Experiments : drinker: the Drinker Paradox ser : the inconsistency of p(x) <-> (all y)(x p(y)) for transitive and serial < on a non-empty domain dpe : the preservation of the diamond property under reflexive closure nl : the induction step in the proof of Newman's Lemma p1p2 and p2p1: equivalence of two versions of Pappus' Axiom pd_hes : Hessenberg's incomplete argument for Pappus -> Desargues, that is, Case 1 in Cronheim's proof cro_8_2: Cronheim's reduction of 8 to 2 cases pd_cro : Cronheim's proof of Case 2, the last 2 (symmetric) cases --------------------------------------------------------------------- Rough estimation of the difficulty: drinker, ser, dpe: all theorem provers should be able to do this nl, p2p1, cro_8_2: some theorem provers can, others cannot p1p2: difficult for most provers (CL still manages in over 5000 steps) pd_hes,pd_cro: out of reach for all theorem provers (CL needs a script) All problems have been submitted to the TPTP data base. Upon entrance they have been tested with the following test environment: CPUModel : Intel(R) Pentium(R) 4 CPU 2.80GHz RAMPerCPU : 1005MB OS : Linux 2.4.20-6 CPUSpeed : 2793MHz Time limit : 300s Timings are in wall clock seconds. E 0.82 ------ cro_8_2 Theorem 257.8 dpe Theorem 0.0 drinker Theorem 0.0 nl Theorem 1.7 p1p2 Timeout 305.7 p2p1 Theorem 16.3 pd_cro Timeout 305.7 pd_hes Timeout 305.8 ser Theorem 0.0 Vampire 7.0 ----------- cro_8_2 Theorem 8.7 dpe Theorem 0.0 drinker Theorem 0.0 nl Theorem 44.6 p1p2 GaveUp 303.9 p2p1 GaveUp 303.8 pd_cro GaveUp 302.9 pd_hes GaveUp 303.4 ser Theorem 0.0 E-SETHEO csp04 -------------- cro_8_2+noeq Theorem 1.0 dpe+noeq Theorem 0.5 drinker+noeq Theorem 0.1 nl+noeq Theorem 30.2 p1p2+noeq Timeout 305.9 p2p1+noeq Theorem 46.7 pd_cro+noeq GaveUp 303.1 pd_hes+noeq GaveUp 304.7 ser+noeq Theorem 0.2 SPASS 2.1 --------- cro_8_2 Theorem 3.6 dpe Theorem 0.0 drinker Theorem 0.0 nl Timeout 305.6 p1p2 GaveUp 300.6 p2p1 GaveUp 300.6 pd_cro Timeout 305.7 pd_hes GaveUp 301.9 ser Theorem 0.0 CL (tested by Bezem on a slightly less powerful machine) -- cro_8_2 proof found 0.40 dpe proof found 0.00 drinker proof found 0.00 nl proof found 0.01 p1p2 proof found 2.31 p2p1 proof found 0.27 pd_cro proof script 2.51 (not automatic) pd_hes proof script 4.84 (not automatic) ser proof found 0.00 Here "proof found" means that CL could find the proof all by itself. In order to get a fair comparison of CL with the other systems, the timings of CL do not include the generation of a Coq proof object.