See the staff page for the links to the dblp page of each group member.
- 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