Start Colosseum over the Web

Please use lower case characters!

Input theorem to be proved (the thesis)

Input theory (list of hypotheses)

Options

Syntax

TraditionalColosseum
¬ Aneg a
A ∧ Ba and b
A ∨ Ba or b
A → Ba ---> b
A ↔ Ba <--> b
∀ x: p(x)all(x, p(x))
∃ x: p(x)exi(x, p(x))

Experimental version: please respect the syntax for the input formulae !

Example (The Peirce Formula)

Note, that Colosseum is an automated theorem prover for intuitionistic first order logic. The Peirce Formula is not valid without the hypothesis, Tertium Non Datur.

Examples (Prof. Thiels Dschungelbuch)

For all examples: no hypotheses.

        all(x, a(x) and b(x)) <--> ( all(y, a(y)) and all(z, b(z)) )       % 46
        exi(x, a(x) or  b(x)) <--> ( exi(y, a(y)) or  exi(z, b(z)) )       % 45
        
        exi(x, a(x) and b(x))  ---> ( exi(y, a(y)) and exi(z, b(z)) )      % 47
        all(x, a(x) or  b(x))  <--- ( all(y, a(y)) or  all(z, b(z)) )      % 48
        
        all(x, a(x) ---> b(x)) <--- ( exi(y, a(y)) ---> all(z, b(z)))      % 56
        exi(x, a(x) ---> b(x)) ---> ( all(y, a(y)) ---> exi(z, b(z)))      % 55
        
        exi(x, a(x)) ---> neg all(y, neg a(y))                             % 39
        all(x, a(x)) ---> neg exi(y, neg a(y))                             % 41
        
        all(x, neg a(x)) <--> neg exi(y, a(y))                             % 37/38
        exi(x, neg a(x))  ---> neg all(y, a(y))                            % 42
        
        all(x, neg neg a(x)) <--- neg neg all(y, a(y))                     % 76
        exi(x, neg neg a(x)) ---> neg neg exi(y, a(y))                     % 78
        
        all(x, a and b(x)) <--> a and all(y, b(y))                         % 58
        exi(x, a or  b(x)) <--> a or  exi(y, b(y))                         % 63
        
        exi(x, a and b(x)) <--> a and exi(y, b(y))                         % 62
        all(x, a or b(x))  <---  a or  all(y, b(y))                        % 59
         
        all(x, a ---> b(x))  <-->  ( a --->  all(y, b(y)) )                % 61
        exi(x, a ---> b(x))   --->  ( a --->  exi(y, b(y)) )               % 65
        
        exi(x, a(x) ---> b(x)) <--- ( exi(y, a(y)) ---> all(z, b(z)) )     % 57
        
        all(x, a(x) ---> b(x)) ---> ( exi(y, a(y)) ---> exi(z, b(z)) )     % 50
        all(x, a(x) ---> b(x)) ---> ( all(y, a(y)) ---> all(z, b(z)) )     % 51
        all(x, a(x) ---> b(x)) ---> ( all(y, a(y)) ---> exi(z, b(z)) )     % 53
        
        all(x, a(x) and b) <--> all(y, a(y) and b)                         % 66
        exi(x, a(x) or  b) <--> exi(y, a(y) or  b)                         % 72
        
        exi(x, a(x) and b) <--> exi(y, a(y) and b)                         % 71
        all(x, a(x) or  b)  <--- all(y, a(y) or  b)                        % 67
        
        all(x, a(x) ---> b)  ---> all(y, a(y) ---> b)                      % 69
        all(x, a(x) ---> b) <--> exi(y, a(y) ---> b)                       % 70
        
        exi(x, a(x) ---> b)  ---> all(y, a(y) ---> b)                      % 75
        exi(x, a(x) ---> b)  <--- exi(y, a(y) ---> b)                      % 73
        
        exi(x, all(y, a(x,y))) --->  all(y, exi(x, a(x,y)))                % 34
        all(x, all(y, a(x,y))) <--> all(y, all(x, a(x,y)))                 % 35
        neg all(y, all(z, a(x,y))) <--> neg a(x,x)                         % 36

Examples (extracted from a benchmark)

For all examples: no hypotheses.

Valid HTML 4.01 Transitional Valid CSS

Claus Zinn, Martin Gropp (2009-05-08)