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, Framinator, AxiomCalc and InvAxiomCalc)
  • 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
  • Deontic prover, a prover for reasoning with the specificity principle in deontic or modal logics.
  • nnProver: A nested sequent prover for bimodal monotone modal logic M, aka. the Logic of Ability.
  • VINTE: A prover for Lewis’ conditional logics
  • LNSprover: A modular prover for normal and non-normal modal logics using linear nested sequents
  • POULE: An embedding of linear nested sequent calculi for classical modal logics in linear logic