%-------------------------------------------------------------------------- % File : COM003+2 : TPTP v3.4.2. Bugfixed v2.2.0. % Domain : Computing Theory % Problem : The halting problem is undecidable % Version : [Bru91] axioms. % English : % Refs : [Gan98] Ganzinger (1998), Email to Geoff Sutcliffe % : [Bur87b] Burkholder (1987), A 76th Automated Theorem Proving Pr % : [Bru91] Brushi (1991), The Halting Problem % Source : [Bru91] % Names : - [Bru91] % Status : Theorem % Rating : 0.12 v3.4.0, 0.08 v3.3.0, 0.11 v3.2.0, 0.22 v3.1.0, 0.00 v2.5.0, 0.33 v2.4.0, 0.33 v2.2.1 % Syntax : Number of formulae : 16 ( 1 unit) % Number of atoms : 52 ( 0 equality) % Maximal formula depth : 8 ( 6 average) % Number of connectives : 39 ( 3 ~ ; 0 |; 15 &) % ( 11 <=>; 10 =>; 0 <=) % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 17 ( 0 propositional; 1-4 arity) % Number of functors : 2 ( 2 constant; 0-0 arity) % Number of variables : 44 ( 0 singleton; 37 !; 7 ?) % Maximal term depth : 1 ( 1 average) % Comments : % Bugfixes : v2.2.0 - Clauses program_halts2_halts3_outputs_def, program_ % not_halts2_halts3_outputs_def, program_halts2_halts2_outputs_ % def, program_not_halts2_halts2_outputs_def, p4 by [Gan98]. %-------------------------------------------------------------------------- fof(program_decides_def,axiom, ( ! [X] : ( program_decides(X) <=> ! [Y] : ( program(Y) => ! [Z] : decides(X,Y,Z) ) ) )). fof(program_program_decides_def,axiom, ( ! [X] : ( program_program_decides(X) <=> ( program(X) & program_decides(X) ) ) )). fof(algorithm_program_decides_def,axiom, ( ! [X] : ( algorithm_program_decides(X) <=> ( algorithm(X) & program_decides(X) ) ) )). fof(program_halts2_def,axiom, ( ! [X,Y] : ( program_halts2(X,Y) <=> ( program(X) & halts2(X,Y) ) ) )). fof(halts3_outputs_def,axiom, ( ! [X,Y,Z,W] : ( halts3_outputs(X,Y,Z,W) <=> ( halts3(X,Y,Z) & outputs(X,W) ) ) )). fof(program_not_halts2_def,axiom, ( ! [X,Y] : ( program_not_halts2(X,Y) <=> ( program(X) & ~ halts2(X,Y) ) ) )). fof(halts2_outputs_def,axiom, ( ! [X,Y,W] : ( halts2_outputs(X,Y,W) <=> ( halts2(X,Y) & outputs(X,W) ) ) )). fof(program_halts2_halts3_outputs_def,axiom, ( ! [X,Y,Z,W] : ( program_halts2_halts3_outputs(X,Y,Z,W) <=> ( program_halts2(Y,Z) => halts3_outputs(X,Y,Z,W) ) ) )). fof(program_not_halts2_halts3_outputs_def,axiom, ( ! [X,Y,Z,W] : ( program_not_halts2_halts3_outputs(X,Y,Z,W) <=> ( program_not_halts2(Y,Z) => halts3_outputs(X,Y,Z,W) ) ) )). fof(program_halts2_halts2_outputs_def,axiom, ( ! [X,Y,W] : ( program_halts2_halts2_outputs(X,Y,W) <=> ( program_halts2(Y,Y) => halts2_outputs(X,Y,W) ) ) )). fof(program_not_halts2_halts2_outputs_def,axiom, ( ! [X,Y,W] : ( program_not_halts2_halts2_outputs(X,Y,W) <=> ( program_not_halts2(Y,Y) => halts2_outputs(X,Y,W) ) ) )). fof(p1,axiom, ( ? [X] : algorithm_program_decides(X) => ? [W] : program_program_decides(W) )). fof(p2,axiom, ( ! [W] : ( program_program_decides(W) => ! [Y,Z] : ( program_halts2_halts3_outputs(W,Y,Z,good) & program_not_halts2_halts3_outputs(W,Y,Z,bad) ) ) )). fof(p3,axiom, ( ? [W] : ( program(W) & ! [Y] : ( program_halts2_halts3_outputs(W,Y,Y,good) & program_not_halts2_halts3_outputs(W,Y,Y,bad) ) ) => ? [V] : ( program(V) & ! [Y] : ( program_halts2_halts2_outputs(V,Y,good) & program_not_halts2_halts2_outputs(V,Y,bad) ) ) )). fof(p4,axiom, ( ? [V] : ( program(V) & ! [Y] : ( program_halts2_halts2_outputs(V,Y,good) & program_not_halts2_halts2_outputs(V,Y,bad) ) ) => ? [U] : ( program(U) & ! [Y] : ( ( program_halts2(Y,Y) => ~ halts2(U,Y) ) & program_not_halts2_halts2_outputs(U,Y,good) ) ) )). fof(prove_this,conjecture, ( ~ ( ? [X] : algorithm_program_decides(X) ) )). %--------------------------------------------------------------------------