BBeye Demo

This page provides a simple web interface of our theorem prover BBeye. For a given formula of Boolean BI, it performs proof search and prints the proof tree both in the labelled CS_BBI and in S_BBI. For the sake of server stability, this web prover allows up to one minute to solve the formula. If the proof search takes more time, it gives up. To prove complex formulas, please install and run BBeye on your machine.

Syntax

Special Character: T=true, F=false, I=unit
Variables: [A-EGHJ-SU-Za-z]([A-Za-Z0-9]*)
Connectives (in the order of precedence): !, *, /\, \/, -*, ->

Examples

Depth >= 2
I /\ A -> A * A
A -> I * A
!(((A * (C -* (!(!(A -* B) * C)))) /\ !B) * C)
(I -* !(!A * I)) -> A
A -> (A * B) \/ (A * !B)
I -> (A * B) -* (B * A)
I -> (A * (B /\ C)) -* ((A * B) /\ (A * C))
I -> (A -* (B -> C)) -* ((A -* B) -> (A -* C))
I -> ((A -> a) -* ((A -* A) -> A)) -> (A -* A)
(A -* B) /\ (T * (I /\ A)) -> B
(I -* !(!A * I)) -> A
!((A  -* !(A * B)) /\ ((!A  -* !B) /\ B))
I -> (A -* B -* C) -* A * B -* C
I -> A * (B * C) -* A * B * C
I -> A * ((B1 -* B2) * C) -* A * (B1 -* B2) * C
!((A  -* !(!(D -* !(A * (C * B))) * A)) /\ C * (D /\ (A * B)))
!((C1 * (C2 * C3))/\((A  -* !(!(B  -* !(C2 * (C3 * C1))) * A)) * (B /\ (A * T))))
A * (B * (C * D)) -> D * (C * (B * A))

Depth >= 3
A * (B * (C * D)) -> D * (B * (C * A))
A * (B * (C * (D * E))) -> E * (D * (A * (B * C)))
I -> A * ((B1 -* B2) * (C * D)) -* A * D * (C * (B1 -* B2))

Depth >= 4
A * (B * (C * (D * E))) -> E * (B * (A * (C * D)))