The TWB (despite the name) is a generic tableau/sequent engine. In this section we give a simple sequent calculus for classical propositional logic.
We point out only the differences with the tableau interface. For reference see [[k_ml_tableau_prover_normal_modal_logic_k]]
CONNECTIVES [ "~" ; "&" ; "v" ; "->" ; "<->" ; "=>"]
GRAMMAR
formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| ~ formula
;;
expr := formula ;;
node := set => set ;;
END
SEQUENT
RULE Id Close === { A } => { A } END
RULE False Close === { Falsum } => END
RULE True Close === => { Verum } END
RULE AndL A ; B => === { A & B } => END
RULE AndR => A | => B === => { A & B } END
RULE OrL A => | B => === { A v B } => END
RULE OrR => A ; B === => { A v B } END
RULE NegR A => === => { ~ A } END
RULE NegL => A === { ~ A } => END
RULE ImpL => A | B => === { A -> B } => END
RULE ImpR A => B === => { A -> B } END
RULE IffL (A -> B) & (B -> A) => === { A <-> B } => END
RULE IffR => (A -> B) & (B -> A) === => { A <-> B } END
END
let exit = function
|"Open" -> "Not Derivable"
|"Close" -> "Derivable"
|s -> assert(false)
EXIT := exit(status@1)
STRATEGY := tactic ( ( Id
! True ! False
! NegL ! NegR
! AndL ! AndR
! ImpL ! ImpR
! OrL ! OrR
! IffL ! IffR )* )
MAIN