Software

See the staff page for the links to the dblp page of each group member.

Software

  • CERES, a program for cut-elimination by resolution
  • TINC, tools for the Investigation of Non-Classical logics (Paralyzer and AxiomCalc)
  • Genesis, a resolution-based theorem prover using term schematizations
  • MUltlog, a system which takes as input the specification of a finitely-valued first-order logic and produces a sequent calculus, a natural deduction system, and clause formation rules for this logic
  • MUltseq, a generic sequent prover for propositional finitely-valued logics (companion system for MUltlog)
  • TILT, a (first-order) deduction system for classification of clause sets, model building, and clause evaluation
  • VMTL, the Vienna Modular Termination Laboratory, a tool for the (semi-)automatic termination analysis of (standard, context-sensitive and conditional) term rewriting systems