pcseq.ml : a sequent calculus for classical proposition logic

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