Research
Broadly my research is situated in computational logic and automated
reasoning. My main research involves the development and theoretical
analysis of reasoning methodologies and automated reasoning tools as
well as applying these in areas such as artificial intelligence,
knowledge representation, agentbased systems and mathematics.
Specific topics of interest are:
 (fully) automated reasoning
 forgetting, uniform interpolation, secondorder quantifier elimination, hierarchical reasoning
 model generation, minimal model reasoning
 resolutionbased proof techniques, resolution decision procedures
 most other styles of proof systems: tableau, sequent calculus, natural
deduction, inverse method, RasiowaSikorski 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 agentbased systems
 firstorder logic, decidable fragments of firstorder 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
I have been actively involved in the development of a range of reasoning
tools. These include:

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).
 SPASSYarralumla 
A bottomup model generater and firstorder theorem prover implementing
sophisticated forms of blocking and other enhancements.

SPASS  a fully automatic
theorem prover for sorted firstorder 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 firstorder theorem prover SPASS
with a translator of modal and description logic formulae into
firstorder 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 firstorder bottomup 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 firstorder theorem prover SPASS which simulates
derivations of tableauxbased 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 lineartime logic.

pdltableau  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 secondorder 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
 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 MultiAgent Systems,
collaborative research project with the University of Liverpool funded by the EPSRC.
Principal investigator.
 Jan 2001 to Jan 2004

Proof Methods for MultiAgent
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

PathBased Reasoning for Guarded
Formulae, PhD Project funded by the EPSRC.
Principal investigator.
 1998 to 1999

Verification and Animation of Agent Theories,
UKDutch 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 NonClassical Logics funded by the
GermanFrench 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.
Renate A. Schmidt
Home 
Publications 
Tools 
FM Group 
School 
Man Univ
Last modified: 24 Nov 16
Copyright © 19982016
Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk