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, agent-based systems and mathematics.
Specific topics of interest are:
- ontology reengineering, ontology extractions, tracking versions of ontologies
- abduction and induction for description logic based ontology languages
- querying and query rewriting for expressive ontology languages, familisy of guarded fragments
- (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
I have been actively involved in the development of a range of reasoning
tools. These include:
- Protege-TS - An OWL Ontology Term Selection Tool.
- 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
- Sep 2018 to Feb 2019
-
Comparison and Abstraction of SNOMED CT Ontologies,
Partner: IHTSDO (SNOMED International).
EPSRC Impact Acceleration Account Project,
IAA 228, Proof of Concept Scheme.
Principal investigator.
- Sep 2017 to Apr 2018
-
AR4MO: Advanced Reasoning Technologies for Medical Ontologies,
Partner: Babylon Health.
EPSRC Impact Acceleration Account Project,
IAA 204, Proof of Concept Scheme.
Principal Investigator.
- Apr 2015 - Sep 2015
-
ApplyUI: Application of Uniform Interpolation Technology to Large Corporate Ontologies,
Partner: Klappo Ltd.
EPSRC IAA Impact Acceleration Project,
IAA 084, Concept and Feasibility Scheme.
Principal Investigator.
- Jan 2015 - Mar 2015
-
Early Stage Scoping of Food Ontology Engineering Support,
Partner: Klappo Ltd.
EPSRC IAA Impact Acceleration Project,
Relationship Incubator Scheme.
Principal Investigator.
- 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.
Renate A. Schmidt
Home |
Publications |
Tools |
FM Group |
School |
Man Univ
Last modified: 27 Sep 20
Copyright © 1998-2016
Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk