Ullrich Hustadt

Research interests

First-order reasoning

I am interested in resolution-based and tableaux-based decision procedures for decidable fragments of first-order logic, including fragments resulting from the relational, semi-functional and optimised functional translation of decidable propositional modal logics. See, for example, De Nivelle, Hustadt, and Schmidt (2000), Hustadt and Schmidt (2000a, 1999a).

Reasoning in non-classical logics

I'm concerned with the design and analysis, both theoretical and empirical, of modal and temporal theorem provers. Some details of our findings are presented here. Related publications concerning modal theorem provers are, for example, Hustadt and Schmidt (2000b, 1999c, 1998a). Concerning temporal logic, I have been involved with the development of TRP, TRP++, and their evaluations. See, for example, Hirsch and Hustadt (2001a); Hustadt and Konev (2003); Hustadt, Konev, Riazanov and Voronkov (2004); Hustadt, Konev and Schmidt (2005; Hustadt and Schmidt (2002b); Konev, Degtyarev, Dixon, Fisher and Hustadt (2005).

Agent Logics

I've also investigated proof methods for temporal logics of knowledge and belief, and more recently general frameworks for the combination of temporal and modal logics, in particular, the KARO framework. For further details see, for example, Hustadt, Dixon, Schmidt and Fisher (2000); Hustadt, Dixon, Schmidt, Fisher, Meyer, van der Hoek (2005, 2001a, 2001b).

Web Ontologies

Together with Boris Motik and Ulrike Sattler, University of Manchester, I been involved in the development of a decision procedure the web ontology languages SHIQ and SHIQ(D) based on the basic superposition calculus. This approach offers a radical alternative to tableaux calculi for such languages. See Hustadt, Motik and Sattler (2005a, 2005b, 2004a, 2004b, 2004c); Motik, Sattler and Hustadt (2003a).


Papers and Publications (Link)


Project involvement (past and present)


Software

  • CLProver++ - a C++ implementation of a theorem prover for Coalition Logic (CL), developed by Paul Gainer.
  • CTL-RP - a C implementation of a theorem prover for Computation Tree Logic (CTL), developed by Lan Zhang. Uses the SPASS theorem prover as `computational engine'.
  • MOTEL - an experimental knowledge representation system which provides deductive, abductive, and non-monotonic inference meachanisms for a knowledge representation formalism combining modal and description logics.
  • MSPASS - an enhancement of the first-order theorem prover SPASS with a translator of modal formulae and formulae of the relational calculus into first-order logic with equality.
  • MKE - an implementation of a tableaux-based decision procedure for basic modal logic.
  • pdl-tableau - an implementation of the tableau calculus introduced in De Giacomo and Massacci (2000), "Combining Deduction and Model Checking into Tableaux and Algorithms for Converse-PDL" (Information and Computation 162, pp. 117-137).
  • PLTLmona - a translator from propositional linear-time logic to MONA input syntax.
  • TABSPASS - a modified version of the first-order theorem prover SPASS which simulates derivations of tableaux-based decision procedures for basic modal logic.
  • TRP - a protoypical implementation of a theorem prover for propositional linear-time logic based on the temporal resolution calculus.
  • TRP++ - a C++ implementation of a theorem prover for propositional linear-time logic based on the temporal resolution calculus, developed by Boris Konev.
  • TeMP - a C++ implementation of a theorem prover for the monodic fragment of first-order linear-time temporal logic over expanding domains based on the temporal resolution calculus, developed by Boris Konev. Uses the Vampire theorem prover as theorem proving kernel.
  • TSPASS. a C implementation of a fair theorem prover for the monodic fragment of first-order linear-time temporal logic over expanding domains based on the temporal resolution calculus, developed by Michel Ludwig. Uses the SPASS theorem prover as `computational engine'.

Renate A. Schmidt maintains a list of computational tools for modal logics.