Ullrich Hustadt's Publications and Papers

2016

Cláudia Nalon, Ullrich Hustadt, and Clare Dixon (2016): ``KSP: A Resolution-Based Prover for Multimodal K.'' In N. Olivetti and A. Tiwari, editors, Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016) [Coimbra, Portugal, 27 June-2 July 2016], pp. 406-415. LNAI 9706, Springer, 2016.
Abstract, BibTeX. PDF (© Springer).

Paul Gainer, Clare Dixon, and Ullrich Hustadt (2016): ``Probabilistic Model Checking of Ant-Based Positionless Swarming.'' In L. Alboul, D. D. Damian, and J. M. Aitken, editors, Proceedings of the 17th Annual Conference Towards Autonomous Robotic Systems (TAROS 2016) [Sheffield, UK, 26 June-1 July 2016], pp. 127-138. LNCS 9716, Springer 2016.
Abstract, BibTeX. PDF (© Springer).

2015

Ullrich Hustadt, Paul Gainer, Clare Dixon, Cláudia Nalon, and Lan Zhang (2015): ``Ordered Resolution for Coalition Logic.'' In H. de Nivelle, editor, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015) [Wroclaw, Poland, 20-24 September 2015], pp. 165-180. LNAI 9323, Springer International Publishing Switzerland 2015.
Abstract, BibTeX. PDF (© Springer).

Cláudia Nalon, Ullrich Hustadt, and Clare Dixon (2015): In H. de Nivelle, editor, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015) [Wroclaw, Poland, 20-24 September 2015], pp. 181-196. LNAI 9323, Springer International Publishing Switzerland 2015.
Abstract, BibTeX. PDF (© Springer).

2014

Cláudia Nalon, Lan Zhang, Clare Dixon, and Ullrich Hustadt (2014a): ``A Resolution Prover for Coalition Logic.'' In F.~Mogavero, A.~Murano and M.~Y.~Vardi, editors, Proceedings 2nd International Workshop on Strategic Reasoning (SR 2014), Electronic Proceedings in Theoretical Computer Science, 146:65--74, 2014.
Abstract, BibTeX, PDF.

Cláudia Nalon, Lan Zhang, Clare Dixon, and Ullrich Hustadt (2014b): ``A resolution-based calculus for Coalition Logic.'' In Journal of Logic and Computation 24(4):883-917, 2014.
Abstract, BibTeX, PDF.

L. Zhang, U. Hustadt, and C. Dixon (2014): ``A Resolution Calculus for Branching-Time Temporal Logic CTL.'' In ACM Transactions on Computational Logic 15(1):10/1-38.
Abstract, BibTeX, PDF.

2013

Cláudia Nalon, Lan Zhang, Clare Dixon, and Ullrich Hustadt (2013): ``A resolution-based calculus for Coalition Logic (Extended Version).'' Technical Report ULCS-13-004, Department of Computer Science, University of Liverpool.
Abstract, BibTeX, PDF.

R. A. Schmidt and U. Hustadt (2013): ``First-Order Resolution Methods for Modal Logics.'' In A. Voronkov and C. Weidenbach, editors, Programming Logics, pp. 345-391. Lecture Notes in Computer Science 7797, Springer.
Abstract, BibTeX, Abstract + PDF (Springer).

2010

U. Hustadt and R. A. Schmidt (2010): ``A Comparison of Solvers for Propositional Dynamic Logic.'' In B. Konev, R. A. Schmidt and S. Schulz, editors, Proceedings of the Workshop on Practical Aspects of Automated Reasoning PAAR-2010 [Edinburgh, Scotland, 14 July 2010].
Abstract (including benchmarking formulae), BibTeX, PDF.

M. Ludwig and U. Hustadt (2010): ``Implementing a fair monodic temporal logic prover.'' In AI Communications 23(2-3):69-96.
Abstract, BibTeX, Abstract + PDF (IOS Press).

L. Zhang, U. Hustadt, and C. Dixon (2010): ``CTL-RP: A computation tree logic resolution prover.'' In AI Communications 23(2-3):111-136.
Abstract, BibTeX, Abstract + PDF (IOS Press).

2009

M. Ludwig and U. Hustadt (2009a): ``Redundancy Elimination in Monodic Temporal Reasoning.'' In N. Peltier and V. Sofronie-Stokkermans, editors, Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP 2009) [Oslo, Norway, 6-7 July 2009].
Abstract, BibTeX, PDF.

M. Ludwig and U. Hustadt (2009b): ``Resolution-Based Model Construction for PLTL.'' In C. Lutz and J.-F. Raskin, editors, Proceedings of the 16th International Symposium on Temporal Representation and Reasoning (TIME-2009) [Brixen-Bressanone, Italy, 23-25 July 2009], pp. 73-80. IEEE Computer Society.
Abstract, BibTeX, PDF (© IEEE Press).

M. Ludwig and U. Hustadt (2009c): ``Fair Derivations in Monodic Temporal Reasoning.'' In R. A. Schmidt, editor, Proceedings of the 22nd International Conference on Automated Deduction (CADE-22) [Montreal, Canada, 2-7 August 2009], pp. 261-276. LNAI 5663, Spinger.
Abstract, BibTeX, Abstract + PDF (Springer).

L. Zhang, U. Hustadt, and C. Dixon (2009): ``A Refined Resolution Calculus for CTL.'' In R. A. Schmidt, editor, Proceedings of the 22nd International Conference on Automated Deduction (CADE-22) [Montreal, Canada, 2-7 August 2009], pp. 245-260. LNAI 5663, Spinger.
Abstract, BibTeX, Abstract + PDF (Springer).

2008

U. Hustadt, B. Motik, and U. Sattler (2008): ``Deciding expressive description logics in the framework of resolution.'' In Information and Computation 206(5): 579-601.
Abstract, BibTeX, Abstract + PDF (Elsevier).

2007

U. Hustadt, B. Motik, and U. Sattler (2007): ``Reasoning in Description Logics by a Reduction to Disjunctive Datalog.'' In Journal of Automated Reasoning 39(3):351-384.
Abstract, BibTeX, Abstract + PDF (Springer).

R. A. Schmidt and U. Hustadt (2007): ``The Axiomatic Translation Principle for Modal Logic.'' In ACM Transactions on Computational Logic 8(4):19/1-55.
Abstract, BibTeX, Abstract + PDF (ACM Press).

2006

U. Hustadt, D. Tishkovsky, F. Wolter, and M. Zakharyaschev (2006): ``Automated reasoning about metric and topology.'' In Michael Fisher, Wiebe van der Hoek, Boris Konev and Alexei Lisitsa, editors, Proceedings of the 10th European Conference on Logics in Artificial Intelligence (JELIA 2006) [Liverpool, UK, 13-15 September 2006], pp. 490-493. LNAI 4160, Springer.
Abstract, BibTeX, Abstract + PDF (Springer).

2005

M. C. Fernández-Gago, U. Hustadt, C. Dixon, M. Fisher, and B. Konev (2005): ``First-Order Temporal Verification in Practice.'' In Journal of Automated Reasoning 34:295-321.
Abstract, BibTeX, Abstract + PDF (Springer).

U. Hustadt, C. Dixon, R. A. Schmidt, M. Fisher, J.-J. Ch. Meyer, and W. van der Hoek (2005): ``Verification Within the KARO Agent Theory.'' In C. Rouff, M. Hinchey, J. Rash, W. Truszkowski, and D. Gordon-Spears, editors, Agent Technology from a Formal Perspective. Springer, 2005.
Abstract, BibTeX, PDF (© Springer).

U. Hustadt, B. Konev, and R. A. Schmidt (2005): ``Deciding Monodic Fragments by Temporal Resolution.'' In R. Nieuwenhuis, editor, Procceedings of the 20th International Conference on Automated Deduction (CADE-20) [Tallinn, Estonia, 22-27 July 2005], pp. 204-218. LNAI 3632, Springer.
Abstract, BibTeX, PDF, Abstract + PDF (Springer).

U. Hustadt and B. Motik (2005): ``Description Logics and Disjunctive Datalog - The Story so Far.'' In Ian Horrocks, Ulrike Sattler, and Frank Wolter, editors, Proceedings of the 2005 International Workshop on Description Logics (DL2005) [Edinburgh, Scotland, UK, 26-28 July 2005].
Abstract, BibTeX, PDF.

U. Hustadt, B. Motik, and U. Sattler (2005a): ``A Decomposition Rule for Decision Procedures by Resolution-Based Calculi.'' In F. Baader and A. Voronkov, editors, Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2004) [Montevideo, Uruguay, 14-18 March 2005], pp. 21-35. LNAI 3452, Springer.
Abstract, BibTeX, Abstract + PDF (Springer).

U. Hustadt, B. Motik, and U. Sattler (2005b): ``Data Complexity of Reasoning in Very Expressive Description Logics.'' In Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI 2005) [Edinburgh, Scotland, 30 July-5 August 2005], pp. 466-471.
Abstract, BibTeX, PDF (IJCAI).

B. Konev, A. Degtyarev, C. Dixon, M. Fisher, and U. Hustadt (2005): ``Mechanising first-order temporal resolution.'' In Information and Computation 199(1-2):55-86.
Abstract, BibTeX, Abstract + PDF (Elsevier).

2004

V. Goranko, U. Hustadt, R. A. Schmidt, and D. Vakarelov (2004): ``SCAN is complete for all Sahlqvist formulae.'' In R. Berghammer, B. Möller, and G. Struth, editors, Revised Selected Papers of the 7th International Seminar on Relational Methods in Computer Science and the 2nd International Workshop on Applications of Kleene Algebra [Bad Malente, Germany, 12-17 May 2003], pp. 149-162. LNCS 3051, Springer.
Abstract, BibTeX, PDF (© Springer).

U. Hustadt and B. Konev (2004): ``TRP++: A temporal resolution prover.'' In M. Baaz, J. Makowsky, and A. Voronkov, editors, Collegium Logicum, volume 8. Kurt Gödel Society, Wien, 2004.
Abstract, BibTeX, PDF (preprint).

U. Hustadt, B. Konev, A. Riazanov, and A. Voronkov (2004a): ``TeMP: A Temporal Monodic Prover.'' In D. A. Basin and M. Rusinowitch, editors, Proceedings of the Second International Joint Conference on Automated Reasoning (IJCAR 2004) [Cork, Ireland, 4-8 July 2004], pp. 326-330. LNAI 3097, Springer.
Abstract, BibTeX, PDF (© Springer).

U. Hustadt, B. Konev, A. Riazanov, and A. Voronkov (2004b): ``TeMP: A Temporal Monodic Prover.'' Technical Report ULCS-04-004, Department of Computer Science, University of Liverpool.
Abstract, BibTeX, PostScript

U. Hustadt, B. Motik, and U. Sattler (2004a): ``Reducing SHIQ- Description Logic to Disjunctive Datalog Programs.'' In D. Dubois, C. Welty, and M.-A. Williams, editors, Proceedings of the 9th International Conference on Knowledge Representation and Reasoning (KR 2004) [Whistler, Canada, 2-5 June 2004], pp. 152-162. AAAI Press.
Abstract, BibTeX, PDF (© AAAI Press).

U. Hustadt, B. Motik, and U. Sattler (2004b): ``Reasoning in Description Logics with a Concrete Domain in the Framework of Resolution.'' In R. Lopez de Mantaras and L. Saitta, editors, Proceedings of the 16th European Conference on Artificial Intelligence (ECAI 2004) [Valencia, Spain, 22-27 August 2004], pp. 353-357. IOS Press.
Abstract, BibTeX, PDF (© IOS Press).

U. Hustadt, B. Motik, and U. Sattler (2004c): ``Reasoning for Description Logics around SHIQ in a Resolution Framework.'' FZI-Report 3-8-04/04, FZI Karlsruhe, Germany.
Abstract, BibTeX, PDF.

U. Hustadt, R. A. Schmidt, and L. Georgieva (2004): ``A Survey of Decidable First-Order Fragments and Description Logics.'' Journal on Relational Methods in Computer Science 1:251-276.
Abstract, BibTeX, PDF.

R. A. Schmidt, E. Orlowska, and U. Hustadt (2004): ``Two proof systems for Peirce algebras.'' In R. Berghammer, B. Möller, and G. Struth, editors, Revised Selected Papers of the 7th International Seminar on Relational Methods in Computer Science and the 2nd International Workshop on Applications of Kleene Algebra [Bad Malente, Germany, 12-17 May 2003], pp. 238-251. LNCS 3051, Springer.
Abstract, BibTeX, PDF (© Springer).

R. A. Schmidt, Dmitry Tishkovsky, and U. Hustadt (2004): ``Interactions between Knowledge, Action, and Commitment within Agent Dynamic Logic.'' Studia Logica 78(3):381-415.
Abstract, BibTeX, Abstract + PDF (Springer).

2003

B. Konev, A. Degtyarev, C. Dixon, M. Fisher, and U. Hustadt (2003): ``Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case.'' In Proceedings of the 10th International Symposium on Temporal Representation and Reasoning / 4th International Conference on Temporal Logic (TIME-ICTL 2003) [Cairns, Queensland, Australia, 8-10 July 2003], 72-82. IEEE Computer Society.
Abstract, BibTeX, Abstract + PDF (IEEE Press).

B. Motik, U. Sattler, and U. Hustadt (2003): ``Reducing SHIQ- Description Logic to Disjunctive Datalog Programs.'' FZI-Report 1-8-11/03, FZI Karlsruhe, Germany.
Abstract, BibTeX, PDF.

L. Georgieva, U. Hustadt, and R. A. Schmidt (2003): ``Hyperresolution for Guarded Formulae.'' Journal of Symbolic Computation 36(1-2):163-192.
Abstract, BiBTeX, Abstract + PDF (Elsevier).

V. Goranko, U. Hustadt, R. A. Schmidt, and D. Vakarelov (2003): ``SCAN is complete for all Sahlqvist formulae.'' In R. Berghammer and B. Möller, editors, Proceedings of the 7th International Seminar on Relational Methods in Computer Science (RelMiCS-7) [Bad Malente, Germany, 12-17 May 2003], pp. 230-241. Christian-Albrechts-Universität Kiel.
Abstract, BibTeX, PDF.

U. Hustadt and B.Konev (2003): ``TRP++ 2.0: A Temporal Resolution Prover.'' In F. Baader, editor, Proceedings of the 19th International Conference on Automated Deduction (CADE-19) [Miamia Beach, USA, July/August 2003], pp. 274-278. LNAI 2741, Springer.
Abstract, BiBTeX, PDF, Abstract + PDF (Springer) (© Springer).

R. A. Schmidt and U. Hustadt (2003a): ``Mechanised Reasoning and Model Generation for Extended Modal Logics.'' Preprint Series CSPP-19, University of Manchester, UK.
Abstract, BibTeX, PDF.

R. A. Schmidt and U. Hustadt (2003b): ``A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae.'' In F. Baader, editor, Proceedings of the 19th International Conference on Automated Deduction (CADE-19) [Miami Beach, USA, July/August 2003], pp. 412-426. LNAI 2741, Springer.
Abstract, BiBTeX, PDF (© Springer), Abstract + PDF (Springer).

R. A. Schmidt and U. Hustadt (2003c): ``Mechanised Reasoning and Model Generation for Extended Modal Logics.'' In H. de Swart, E. Orlowska, G. Schmidt, and M. Roubens, editors, Theory and Applications of Relational Structures as Knowledge Instruments. COST Action 274, TARSKI. Revised Papers., pp. 38-67. Lecture Notes in Computer Science 2929, Springer.
Abstract, BiBTeX, PDF (© Springer).

R. A. Schmidt, E. Orlowska, and U. Hustadt (2003): ``Two proof systems for Peirce algebras.'' In R. Berghammer and B. Möller, editors, Proceedings of the 7th International Seminar on Relational Methods in Computer Science RelMiCS-7 (Bad Malente, Germany, May 12-17 2003), pp. 197-203. Christian-Albrechts-Universität Kiel.
Abstract, BibTeX, PDF.

2002

B. Bennett, C. Dixon, M. Fisher, U. Hustadt, E. Franconi, I. Horrocks, and M. de Rijke (2002): ``Combinations of Modal Logics.'' Artificial Intelligence Review 17(1):1-20.
Abstract, BibTeX, PDF (© Springer), Abstract + PDF (Springer).

L. Georgieva, U. Hustadt, R. A. Schmidt (2002a): ``On the relationship between decidable fragments, non-classical logics, and description logics.'' In I. Horrocks and S. Tessaris, editors, Proceedings of the International Workshop on Description Logics (DL2002) [Toulouse, France, 19-21 April 2002], pp. 25-36.
Abstract, BiBTeX, PDF.

L. Georgieva, U. Hustadt, R. A. Schmidt (2002b): ``A new clausal class decidable by hyperresolution.'' In A. Voronkov, editor, Proceedings of the 18th International Conference on Automated Deduction CADE-18 [Copenhagen, Denmark, 27-30 July 2002], pp. 258--272. LNAI 2392, Springer.
Abstract, BibTeX, PDF (© Springer), Abstract + PDF (Springer).

U. Hustadt and R. A. Schmidt (2002a): ``Using resolution for testing modal satisfiability and building models.'' Journal of Automated Reasoning 28(2):205-232.
Abstract, BibTeX, Abstract + PDF (Springer).

U. Hustadt and R. A. Schmidt (2002b): ``Scientific benchmarking with temporal logic decision procedures.'' In D. Fensel, F. Giunchiglia, D. McGuinness, and M.-A. Williams, editors, Proceedings of the Eighth International Conference on Principles of Knowledge Representation and Reasoning (KR 2002) [Toulouse, France, 22-25 April 2002], pp. 533-544. Morgan Kaufmann.
Abstract, BiBTeX, PDF (© Morgan Kaufmann).

2001

C. Fermüller, A. Leitsch, U. Hustadt, and T. Tammet (2001): ``Resolution decision procedures.'' In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, pp. 1791-1850. Elsevier.
Abstract, BibTeX, PDF (© Elsevier).

L. Georgieva, U. Hustadt, R. A. Schmidt (2001a): ``Computational space efficiency and minimal model generation for guarded formulae.'' In R. Nieuwenhuis and A. Voronkov, editors, Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001) [Havana, Cuba, 3-7 December 2001], pp. 85-99. LNAI 2250, Springer.
Abstract, BibTeX, PDF (© Springer).

L. Georgieva, U. Hustadt, R. A. Schmidt (2001b): ``Computational space efficiency and minimal model generation for guarded formulae.'' In R. Gore, A. Leitsch, and T. Nipkow, editors, IJCAR 2001: Short Papers, pp. 34-43. Technical Report DII 11/01, Dipartimento di Ingegneria dell'Informazione, Unversitá degli Studi di Siena.
Abstract, BibTeX, PDF.

B. Hirsch and U. Hustadt (2001): ``Translating PLTL into WS1S: Application Description.'' In Methods for Modalities II. University of Amsterdam, 2001.
Abstract, BibTeX, PDF, Software: TRP.

U. Hustadt, C. Dixon, R. A. Schmidt, M. Fisher, J.-J. Meyer, and W. van der Hoek (2001a): ``Verification within the KARO agent theory.'' In J. L. Rash, C. A. Rouff, W. Truszkowski, D. Gordon, and M. G. Hinchey, editors, Proceedings of the First International Workshop on Formal Approaches to Agent-Based Systems (FAABS 2000) [Goddard Space Flight Center, Greenbelt, MD, USA, 5-7 April 2000], pp. 33-47. LNAI 1871, Springer.
Abstract, BibTeX, PDF (© Springer).

U. Hustadt, C. Dixon, R. A. Schmidt, M. Fisher, J.-J. Meyer, and W. van der Hoek (2001b): ``Reasoning about agents in the KARO framework.'' In C. Bettini and A. Montanari, editors, Proceedings of the Eighth International Symposium on Temporal Representation and Reasoning (TIME-01) [Cividale del Friuli, Italy, June 14-16 2001], pp. 206-213. IEEE Press.
Abstract, BibTeX, PDF (© IEEE Press).

U. Hustadt and R. A. Schmidt (2001): ``Formulae which highlight differences between temporal logic and dynamic logic provers.'' In E. Giunchiglia and F. Massacci, editors, Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, pp. 68-76. Technical Report DII 14/01, Dipartimento di Ingegneria dell'Informazione, Unversitá degli Studi di Siena.
Abstract, BibTeX, PDF.

2000

H. Ganzinger, U. Hustadt, C. Meyer, and R. A. Schmidt(2000): ``A resolution-based decision procedure for extensions of K4.'' In M. Zakharyaschev, K. Segerberg, and M. de Rijke, and H. Wansing, editors, Advances in Modal Logic 2, pp. 243-263. CSLI Publications.
Abstract, BiBTeX, PDF (© CSLI Publications).

H. de Nivelle,, R. A. Schmidt, and U. Hustadt (2000): ``Resolution-based methods for modal logics.'' Logic Journal of the IGPL (8)3:265-292.
Abstract, BibTeX, Abstract + PDF (Oxford University Press), Errata.

L. Georgieva, U. Hustadt, R. A. Schmidt (2000): ``Hyperresolution for guarded formulae.'' In P. Baumgartner and H. Zhang, editors, Proceedings of the Third International Workshop on First-Order Theorem Proving (FTP 2000) [St. Andrews, Scotland, 2-4 July 2000], pp. 101-112. Fachberichte Informatik 5/2000, Institut für Informatik, Universität Koblenz-Landau.
Abstract, BibTeX, PDF.

U. Hustadt, C. Dixon, R. A. Schmidt, and M. Fisher (2000): ``Normal forms and proofs in combined modal and temporal logics.'' In H. Kirchner and C. Ringeissen, editors, Proceedings of the Third International Workshop on Frontiers of Combining Systems (FroCoS 2000) [Nancy, France, 22-24 March 2000], pp. 73-87. LNAI 1794, Springer.
Abstract, BibTeX, PDF (© Springer).

U. Hustadt and R. A. Schmidt (2000a): ``Issues of decidability for description logics in the framework of resolution.'' In G. Salzer and R. Caferra, editors, Automated Deduction in Classical and Non-Classical Logics, pp. 192-206. LNAI 1761, Springer.
Abstract, BiBTeX, PDF (© Springer).

U. Hustadt and R. A. Schmidt (2000b): ``Using resolution for testing modal satisfiability and building models.'' In I. Gent, H. van Maaren and T. Walsh, editors, SAT 2000: Highlights of Satisfiability Research in the Year 2000, pp. 459-483. Frontiers in Artificial Intelligence and Applications 63, IOS Press.
Abstract, BiBTeX, PDF (© IOS Press).

U. Hustadt and R. A. Schmidt (2000c): ``MSPASS: Modal reasoning by translation and first-order resolution.'' In R. Dyckhoff, editor, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000) [St. Andrews, Scotland, 3-7 July 2000], pp. 67-71. LNAI 1847, Springer.
Abstract, BibTeX, PDF (© Springer).

R. A. Schmidt and U. Hustadt (2000): ``A resolution decision procedure for fluted logic.'' In D. McAllester, editor, Proceedings of the 17th International Conference on Automated Deduction (CADE-17) [Pittsburgh, USA, 17-20 June 2000], pp. 433-448. LNAI 1831, Springer.
Abstract, BibTeX, PDF (© Springer).

1999

U. Hustadt (1999): ``Resolution-based decision procedures for subclasses of first-order logic.'' PhD thesis, Universität des Saarlandes, Saarbrücken, Germany.
Abstract, BibTeX, PDF.

U. Hustadt and R. A. Schmidt (1999a): ``Maslov's class K revisited.'' In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16) [Trento, Italy, 7-10 July 1999], pp. 172-186. LNAI 1632, Springer.
Abstract, BibTeX, PDF (© Springer).

U. Hustadt and R. A. Schmidt (1999b): ``On the relation of resolution and tableaux proof systems for description logics.'' In D. Thomas, editor, Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI'99) [Stockholm, Sweden, 31 July-6 August 1999], Volume 1, pp. 110-115. Morgan Kaufmann.
Abstract, BibTeX, PDF (© Morgan Kaufmann).

U. Hustadt and R. A. Schmidt (1999c): ``An empirical analysis of modal theorem provers.'' Journal of Applied Non-Classical Logics (9)4:479-522.
Abstract, BibTeX, PDF (© Taylor & Francis), Abstract + PDF (Taylor & Francis).

U. Hustadt, R. A. Schmidt, and C. Weidenbach (1999): ``MSPASS: Subsumption testing with SPASS.'' In P. Lambrix et al., editors, Proceedings of the International Workshop on Description Logics (DL'99) [Linköping University, Sweden], pp. 136-137.
Abstract, BiBTeX, PDF.

1998

U. Hustadt and R. A. Schmidt (1998a): ``Simplification and backjumping in modal tableau.'' In H. de Swart, editor, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'98) [Oisterwijk, The Netherlands, 5-8 May 1998], pp. 187-201. LNAI 1397, Springer.
Abstract, BibTeX, PDF (© Springer).

U. Hustadt and R. A. Schmidt (1998b): ``Issues of decidability for description logics in the framework of resolution.'' In G. Salzer and R. Caferra, editors, Proceedings of the 2nd International Workshop on First-order Theorem Proving FTP'98 (Vienna, Austria, November 23-25, 1998), pp. 152-161. Technical report E1852-GS-981, Technische Universität Wien.
Abstract, BiBTeX, PDF.

U. Hustadt, R. A. Schmidt, and C. Weidenbach (1998): ``Optimised functional translation and resolution.'' In H. de Swart, editor, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'98) [Oisterwijk, The Netherlands, 5-8 May 1998], pp. 36-37. LNAI 1397, Springer.
Abstract, BibTeX, PDF (© Springer), Abstract + PDF (Springer)

1997

U. Hustadt and R. A. Schmidt (1997a): ``On evaluating decision procedures for modal logic.'' Research Report MPI-I-97-2-003, Max-Planck-Institut für Informatik.
Abstract, BibTeX, PDF.

U. Hustadt and R. A. Schmidt (1997b): ``On evaluating decision procedures for modal logic.'' In M. A. Pollack, editor, Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence IJCAI-97 (Nagoya, Japan, August 23-29, 1997), Volume 1, pp. 202-207. Morgan Kaufmann.
Abstract, BibTeX, PDF (© IJCAI).

1996

H. J. Ohlbach, R. A. Schmidt, and U. Hustadt (1996): ``Translating graded modalities into predicate logics.'' In H. Wansing, editor, Proof Theory of Modal Logic, pp. 253-291. Applied Logic Series 2, Kluwer.
Abstract, BibTeX, Abstract + PDF (Springer).

1995

H. J. Ohlbach, R. A. Schmidt, and U. Hustadt (1995a): ``Translating graded modalities into predicate logic.'' Research Report MPI-I-95-2-008, Max-Planck-Institut für Informatik.
Abstract, BibTeX, PDF.

H. J. Ohlbach, R. A. Schmidt, and U. Hustadt (1995b): ``Symbolic arithmetical reasoning with qualified number restrictions.'' In A. Borgida, M. Lenzerini, D. Nardi, and B. Nebel, editors, International Workshop on Description Logics (DL'95) [Rome, Italy, 2-3 June 1995], pp. 89-95. Appeared as Technical Report RAP.07.95, Dipartimento di Informatica e Sistemistica, Univ. degli studia di Roma.
Abstract, BibTeX, PDF.

1994

U. Hustadt (1994a): ``Common and mutual belief for agent modeling.'' In A. Laux and H. Wansing, editors, Modeling Epistemic Propositions: Workshop during the 18th German Conference on Artificial Intelligence (KI'94). Appeared in KI-94 Workshops: Extended Abstracts, pp. 123-124. Gesellschaft für Informatik.
Abstract, BibTeX, PDF.

U. Hustadt (1994b): ``Do we need the closed-world assumption in knowledge representation?'' In J. Kunze and H. Stoyan, editors, KI-94 Workshops: Extended Abstracts, pp. 123-124. Gesellschaft für Informatik.
Abstract, BibTeX, PDF.

U. Hustadt (1994c): ``A multi-modal logic for user modeling.'' In B. A. Goodman, editor, Proceedings of the Fourth International Conference on User Modeling (UM'94) [Hyannis, MA, USA, 15-19 August 1994], pp. 87-92. The MITRE Corporation.
Abstract, BibTeX, PDF (© The MITRE Corporation).

1993

U. Hustadt and A. Nonnengart (1993): ``Modalities in knowledge representation.'' In C. Rowles, H. Liu, and N. Foo, editors, Proceedings of the 6th Australian Joint Conference on Artificial Intelligence (AI'93) [Melbourne, Australia,], pp. 249-254. World Scientific.
Abstract, BibTeX, PDF (© World Scientific).

U. Hustadt (1993a): ``Automated support for the development of non-classical logics.'' In H.-J. Bürckert and W. Nutt, editors, Modeling Epistemic Propositions: Workshop during the 17th German Conference on Artificial Intelligence (KI'93) [Berlin, Germany, 13-14 September 1993].
Abstract, BibTeX, PDF.

U. Hustadt (1993b): ``Abductive disjunctive logic programming.'' In P. Codognet, P. M. Dung, A. C. Kakas, P. Mancarella, editors, Proceedings of the ICLP'93 Postconference Workshop on Abductive Reasoning (Budapest, Hungary).
Abstract, BibTeX, PDF.

1992

U. Hustadt, A. Nonnengart, R. A. Schmidt, and J. Timm (1992): ``MOTEL user manual.'' Technical Report MPI-I-92-236, Max-Planck-Institut für Informatik.
Abstract, BibTeX, PDF.