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