Start Colosseum over the Web

Please use lower case characters!

Syntax

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

Example (The Peirce Formula)

• Hypothesis: a or neg a
• Thesis: ( (a ---> b) ---> a) ---> a

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)

        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)

• Thesis: all(x, exi(y, all(z, p(x) and q(y) and r(z)))) <--> all(z, exi(y, all(x, p(x) and q(y) and r(z))))
• Thesis: all(x, exi(y, all(z, exi(w, p(x) and q(y) and r(z) and s(w))))) <--> exi(w, all(z, exi(y, all(x, p(x) and q(y) and r(z) and s(w)))))
• Thesis: all(x, exi(y, all(z, exi(w, all(u, p(x) and q(y) and r(z) and s(w) and t(u)))))) <--> all(u, exi(w, all(z, exi(y, all(x, p(x) and q(y) and r(z) and s(w) and t(u))))))
• Thesis: exi(z, all(x, exi(y, p(x) and q(y) and r(z)))) <--> exi(y, all(x, exi(z, p(x) and q(y) and r(z))))
• Thesis: exi(z, all(x, exi(y, all(w, p(x) and q(y) and r(z) and s(w))))) <--> all(w, exi(y, all(x, exi(z, p(x) and q(y) and r(z) and s(w)))))
• Thesis: exi(z, all(x, exi(y, all(w, exi(u, p(x) and q(y) and r(z) and s(w) and t(u)))))) <--> exi(u, all(w, exi(y, all(x, exi(z, p(x) and q(y) and r(z) and s(w) and t(u))))))
• Thesis: exi(x1, all(y1, exi(x2, all(y2, p(x1,y1) and q(x2, y2))))) ---> all(y2, exi(x2, all(y1, exi(x1, p(x1,y1) and q(x2, y2)))))
• Thesis: exi(x1, all(y1, exi(x2, all(y2, exi(x3, all(y3, p(x1,y1) and q(x2, y2) and r(x3,y3))))))) ---> all(y3, exi(x3, all(y2, exi(x2, all(y1, exi(x1, p(x1,y1) and q(x2, y2) and r(x3, y3)))))))