Research

• Research interests
• Publications
• Software
• More resources on the web
• Research projects

Research interests

• (fully) automated reasoning
• forgetting, uniform interpolation, second-order quantifier elimination, hierarchical reasoning
• model generation, minimal model reasoning
• resolution-based proof techniques, resolution decision procedures
• most other styles of proof systems: tableau, sequent calculus, natural deduction, inverse method, Rasiowa-Sikorski proof systems, ...
• relationships between proof systems, relative complexity of proof systems, simulating proof procedures
• deduction calculus synthesis, automated prover generation
• implementing theorem provers and other logical tools
• empirical evaluation of algorithms
• knowledge representation and reasoning, ontology reasoning, semantic web
• formalisations and deduction for agent-based systems
• first-order logic, decidable fragments of first-order logic, solvable clausal classes
• modal logics, dynamic logic, temporal logic
• description logics, dynamic modal logics, Peirce logic
• Tarski's relational calculus and relation algebra
• Boolean modules, Peirce algebra

Publications

• Publications ordered by publication date
• Publications ordered by theme

Software

• FAME - An automated tool for semantic forgetting in expressive description logics.
• LETHE - a tool for uniform interpolation, forgetting and related tasks for OWL ontologies using expressive description logics. The current version comes with functionality for computing uniform interpolants, forgetting solutions, logical differences and TBox abduction.
• MetTeL - an easy to use tableau prover generator producing Java code from the specification of a set of inference rules; supports blocking based on equality reasoning. (Tishkovsky, Schmidt and Khodadadi 2012, Tishkovsky and Schmidt 2013).
• SPASS-Yarralumla - A bottom-up model generater and first-order theorem prover implementing sophisticated forms of blocking and other enhancements.
• SPASS - a fully automatic theorem prover for sorted first-order logic with equality, description logics, traditional modal logics, dynamic modal logics, and relational logics. (Weidenbach, Schmidt et al. 2007).
• The MSPASS theorem prover (Hustadt and Schmidt 2000a) - an enhancement of the first-order theorem prover SPASS with a translator of modal and description logic formulae into first-order logic with equality.
• Axiomatic translation of modal logics - implementation in SPASS by John Kevin Smith. Web interface
• SPASS as a modal tableau prover - extension of SPASS by Rawan G. AlBarakati.
• Yarralumla (Baumgartner and Schmidt 2006) - implements various transformations on clause logic formulas for the purpose of applying first-order bottom-up model generation (BUMG) systems.
• MLTP - an efficient and generic modal logic tableau prover inplemented by Zhen Li.
• The TABSPASS theorem prover (Hustadt and Schmidt 2000b, Hustadt and Schmidt 2002a) - a modified version of the first-order theorem prover SPASS which simulates derivations of tableaux-based decision procedures for basic modal logic.
• The TRP theorem prover (Hustadt and Schmidt 2001, Hustadt and Schmidt 2002b) - a prototypical implementation of a temporal resolution calculus for propositional linear-time logic.
• pdl-tableau - a prototypical implementation of the tableau calculus for PDL.
• The Agent Dynamic Logic package - an implementation of algorithms for the reduction of the satisfiability problem in Agent Dynamic Logic (ADL) to the satisfiability problems in CPDL and PDL. Together with any implementation of a decision procedure for PDL or CPDL it gives a prover for ADL.
• SCAN - a tool for the elimination of second-order quantifiers; facilitates automated correspondence theory (mentioned on the Page of Positive Reviews of Research in Logical AI).
• Empirical analysis of decision procedures for modal logic
• The MOTEL Knowledge Representation System

More resources on the web

• Computational tools for modal logics - a webpage I maintain (contributions and suggestions are most welcome).
• Benchmark Problems for Modal and Description Logics
• Empirical analysis of decision procedures for modal logic

Research projects

May 2010 to Mar 2014

Automated Prover Generation, funded by the EPSRC.
Principal investigator.

Oct 2007 to Sep 2010

Consequence Relations in Logics of AI, collaborative research project with Manchester Metropolitan University funded by the EPSRC.
Principal investigator.

Jan 2007 to Dec 2009

Practical Reasoning Approaches for Web Ontologies and Multi-Agent Systems, collaborative research project with the University of Liverpool funded by the EPSRC.
Principal investigator.

Jan 2001 to Jan 2004

Proof Methods for Multi-Agent Systems, collaborative research project with the University of Liverpool funded by the EPSRC.
Principal investigator.

2001 to 2005

Theory and Applications of Relational Structures as Knowledge Instruments, COST Action 274.
Consulted expert and active participant.

Aug 1999 to Aug 2002

Path-Based Reasoning for Guarded Formulae, PhD Project funded by the EPSRC.
Principal investigator.

1998 to 1999

Verification and Animation of Agent Theories, UK-Dutch Joint Scientific Resesearch Project with Wiebe van der Hoek, Department of Computer Science, Utrecht University, funded by a British Council/NWO research grant.
Principal investigator.

1995 to 1997

Transformation of Logical Systems (TRALOS) funded by the Deutsche Forschungsgesellschaft.
Investigator.

1993 to 1995

Construction of Non-Classical Logics funded by the German-French PROCOPE Programme, Deutscher Akademischer Austauschdienst. Partners: Univ. Paul Sabatier and Inst. de Recherche CNRS.
Investigator.

1991 to 199?

Techniques for Inference in Communicating Systems (TICS), Project D2 of the SFB 314, funded by the Deutsche Forschungsgesellschaft. In cooperation with the Project Processing Arguments Between Controversially Minded Actors (Department of Computer Science, Saarbrücken).
Investigator.