Research

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

Research interests

• subontology generation, forgetting-based knowledge extraction, modularisation, logical difference computation
• knowledge representation and reasoning, knowledge exploitation and re-engineering, ontology-based data access, tracking ontology versions
• abduction and induction for description logic based ontology languages
• query answering and rewriting for expressive ontology languages, family of guarded fragments
• 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

• SNOMED CT Subontology browser - Contains a number of builds of subontologies created with our subontology extractor.
• SNOMED Subontology extractor - Produces an extracted subontology for a given background ontology and set of focus concepts (Del-Pinto, Schmidt and Gao 2022).
• 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

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

Jul 2020 to Sept 2021

Just the Right Amount: SNOMED CT Content Extraction and Sharing, Partner: IHTSDO (SNOMED International).
EPSRC Impact Acceleration Account Project, IAA 290, Secondment Scheme.
Principal investigator.

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.