[Albrecht Heeffer]
Home Logic Math Publications Shogi Sites About Me
         
Logic theorem provers

Logic theorem provers

Propositional

  • Tableaux-based for CL (Classical Logic)
  • Tableaux-based for ParaLogics CLuN, CLaN, CLoN
  • Goal-directed for CL and CLUN
  • EFQ-resolution for CL and CLuN
  • Goal-directed for adaptive logic ACLuN1
  • Gentzen-style sequent calculus based on Socratic proofs
  • Socratic proofs for modal logics K, D, K4, T, S4, B and S5

    Predicative

  • Goal-directed for classical logic
  • Goal-directed for Adapative logic ACLuN1