M. Ludwig and U. Hustadt (2010a):
``Implementing a fair monodic temporal logic prover.''
In AI Communications 23(2-3):69-96.
Abstract,
BibTeX,
PDF (IOS Press).
L. Zhang,
U. Hustadt, and
C. Dixon (2010a):
``CTL-RP: A computation tree logic resolution prover.''
In AI Communications 23(2-3):111-136.
Abstract,
BibTeX,
PDF (IOS Press).
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). IEEE Computer Society.
Abstract,
BibTeX,
PDF.
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, August 2-7, 2009), pp. 261-276. LNAI 5663, Spinger.
Abstract (via Springer),
BibTeX (via DBLP),
Full text (via Springer).
L. Zhang,
U. Hustadt, and
C. Dixon (2009a):
``A Refined Resolution Calculus for CTL.''
In R. A. Schmidt, editor,
Proceedings of the 22nd International Conference on
Automated Deduction CADE-22 (Montreal, Canada, August 2-7, 2009), pp. 245-260. LNAI 5663, Spinger.
Abstract (via Springer),
BibTeX (via DBLP),
Full text (via 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,
PDF (© ACM Press).
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.
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, July 22-27, 2005), pp. 204-218.
LNAI 3632, Springer.
Abstract,
BibTeX,
PDF,
Full text (via Springer) (© Springer-Verlag).
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, July 26-28, 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, March 14-18, 2005),
pp. 21-35.
LNAI 3452,
Springer.
Abstract,
BibTeX,
Full text (via Springer) (© Springer-Verlag).
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, July 30-August 5 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,
Full text (via ScienceDirect).
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.
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, July 4-8 2004),
pp. 326-330. LNAI 3097, Springer.
Abstract,
BibTeX,
PDF (© Springer-Verlag).
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,
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 KR2004
(Whistler, Canada, June 2-5 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, August 22-27, 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, May 12-17 2003), pp. 238-251.
LNCS 3051, Springer.
Abstract,
BibTeX,
PDF (© Springer-Verlag).
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,
Springer site.
L. Georgieva, U. Hustadt,
and R. A. Schmidt
(2003):
``Hyperresolution for Guarded Formulae.''
Journal of Symbolic Computation 36(1-2):163-192.
Abstract,
BiBTeX,
ScienceDirect.
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, May 12-17 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 and PDF at Springer-Verlag
(© Springer-Verlag).
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,
PostScript.
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 (Miamia Beach, USA, July/August 2003), pp. 412-426.
LNAI 2741, Springer.
Abstract,
BiBTeX,
PDF,
Abstract and PDF at Springer-Verlag
(© Springer-Verlag).
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-Verlag).
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.
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, April 19-21 2002), pp. 25-36.
Abstract,
BiBTeX,
PostScript
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,
Kluwer's title page (with access to PDF file).
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 KR2002
(Toulouse, France, April 22-25, 2002), pp. 533-544. Morgan Kaufmann.
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, July 27-30, 2002), pp. 258--272.
LNAI 2392,
Springer.
Abstract,
BibTeX,
PDF (© Springer-Verlag).
H. Ganzinger,
U. Hustadt,
C. Meyer, and
R. A. Schmidt(2001):
``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).
L. Georgieva,
U. Hustadt,
R. A. Schmidt
(2001b):
``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, December 3-7, 2001), pp. 85-99.
LNAI 2250,
Springer.
Abstract,
BibTeX,
PDF (© Springer-Verlag).
L. Georgieva,
U. Hustadt,
R. A. Schmidt
(2001a):
``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,
PostScript.
B. Hirsch and
U. Hustadt (2001):
``Translating PLTL into WS1S: Application Description.'' In Methods for Modalities II. University of Amsterdam, 2001.
Abstract,
PostScript,
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, April 5-7 2000),
pp. 33-47.
LNAI 1871,
Springer.
Abstract,
BibTeX,
PDF (© Springer-Verlag).
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), 206-213. IEEE Press.
Abstract,
BibTeX.
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,
PostScript.
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, July 2-4 2000), pp. 101-112.
Fachberichte Informatik 5/2000, Institut für Informatik, Universität Koblenz-Landau.
Abstract,
BibTeX,
PostScript,
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, March 22-24, 2000), pp. 73-87.
LNAI 1794, Springer.
Abstract,
BibTeX,
PostScript (© Springer-Verlag).
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,
PostScript,
PostScript (gzip),
PDF (© Springer-Verlag).
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.
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, July 3-7, 2000),
pp. 67-71.
LNAI 1847, Springer.
Abstract,
BibTeX,
Postscript,
PDF (© Springer-Verlag).
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, 2000),
pp. 433-448.
LNAI 1831,
Springer.
Abstract,
BibTeX
PostScript (gzip)
(© Springer-Verlag).
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, July 7-10, 1999), pp. 172-186.
LNAI 1632, Springer.
Abstract,
BibTeX,
Postscript,
Postscript (gzip),
PDF (© Springer-Verlag).
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, July 31-August 6, 1999),
Volume 1, pp. 110-115. Morgan Kaufmann.
Abstract,
BibTeX.
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.
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,
PostScript
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 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,
Postscript (gzip).
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, May 5-8, 1998),
pp. 36-37.
LNAI 1397, Springer.
Abstract,
BibTeX,
Postscript,
Postscript (gzip),
PDF,
PDF (gzip) (© Springer-Verlag).
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.
H. J. Ohlbach, R. A. Schmidt, and U. Hustadt
(1995c):
``Symbolic arithmetical reasoning with qualified number restrictions.''
In A. Borgida, M. Lenzerini, D. Nardi, and B. Nebel, editors, International
Workshop on Description Logics (Rome, Italy), pp. 89--95. Appeared
as Technical Report RAP.07.95, Dipartimento di Informatica e Sistemistica,
Univ. degli studia di Roma.
Abstract,
BibTeX,
DVI (gzip),
Postscript (gzip).
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,
Postscript (gzip).
U. Hustadt (1994c): ``A multi-modal logic for user
modeling''. In B. A. Goodman, editor, Proceedings of the Fourth International
Conference on User Modeling UM94 (Hyannis, MA), pp. 87--92. The MITRE Coorporation.
Abstract,
BibTeX,
Postscript (gzip).
U. Hustadt (1993a): ``Automated support for the
development of non-classical logics''. In H.-J. Bürckert and W. Nutt,
editors, Workshop on Modeling Epistemic Propositions at KI'93
(Berlin, Germany).
Abstract,
BibTeX,
Postscript (gzip).
U. Hustadt (1993b): ``Abductive disjunctive logic
programming''. In P. Codognet, P. M. Dung, A. C. Kakas, P. Mancarella,
editors, ICLP'93 Postconference Workshop on Abductive Reasoning
(Budapest, Hungary).
Abstract,
BibTeX,
Postscript (gzip).
| Maintained by Ullrich Hustadt, U.Hustadt@csc.liv.ac.uk, last updated Wednesday, 25-Aug-2010 19:12:22 BST © 1998-2004 by Ullrich Hustadt. |