Institut für Computersprachen AG Theoretische Informatik und Logik (Theory and Logic Group)

Research
(see also individual homepages of group members)

Research fields

• Resolution- and tableaux-based theorem proving
  • Decidable fragments and decision procedures
  • Automated model building
  • Proof theory
  • Complexity issues
• Non-classical logics
  • Proof theory
  • Automated reasoning
  • Knowledge representation
  • Reasoning with vague and uncertain information
• Molecular computing
• DNA computing
• Neural networks
• Formal Languages
• Array grammars
• Graph grammars
• Infinite words
• Equational reasoning and term rewriting
• Schematization of infinite sets of terms, rules, clauses etc.
• Modular properties of term rewriting systems
• Rewriting under strategies
• Proof techniques for confluence and termination
• Formal methods for specification and verification
• Algebraic approaches
• Inductive theorem proving / program verification
• Strategies in proof engineering

Activities

• Conferences and workshops (committees)
• Editorial activities
• KGS (Kurt Gödel Society)

Projects
(selected ones; see also individual homepages of group members)

• LoMoReVI - Logical Models of Reasoning with Vague Information (Subprojects):
  Collaborative Research Project within the EUROCORES programme LogiCCC of the European Science Foundation (ESF)
  funded by FWF (Der Wissenschaftsfonds)
• Rechnerunterstützte Analyse von induktiven Beweisen:
  funded by FWF (Der Wissenschaftsfonds)

Publications

Software

• CERES, a program for cut-elimination by resolution
• 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