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