Back home

Bi-intuitionistic logic: theorem prover demo

Please choose one of the examples below, or enter your own sequent according to the syntax on the left. Then click "Prove!". If you want to see what the prover did then turn on the trace option by pressing the Trace On/Off button. This will print out the rules applied by the prover and will allow you to extract a proof/counter-model if the sequent is provable/unprovable.

Examples:

p => q; r -> ((p -< q) & r)
 Uustalu's example (valid) 
=> p; (((True -< p) & (True -< q)) -> False) -> False
 Falsifiable example
Other sequent:     

Trace on/off: