Ullrich Hustadt's Papers and Publications

BibBase: hustadt, u
generated by bibbase.org
  2020 (1)
KSP: Architecture, Refinements, Strategies and Experiments. Nalon, C.; Hustadt, U.; and Dixon, C. J. Autom. Reasoning, 64(3): 461–484. 2020.
Paper (external PDF)Paper   doi   bibtex
  2019 (1)
Modal Resolution: Proofs, Layers, and Refinements. Nalon, C.; Dixon, C.; and Hustadt, U. ACM Trans. Comput. Log., 20(4): 23:1–23:38. 2019.
Paper (external PDF)Paper   doi   bibtex
  2018 (3)
Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics. Hustadt, U.; Nalon, C.; and Dixon, C. In Konev, B.; Urban, J.; and Rümmer, P., editor(s), Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, July 19th, 2018, volume 2162, of CEUR Workshop Proceedings, pages 34–48, 2018. CEUR-WS.org
Paper (local PDF)Paper   bibtex
The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators. Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M. In Sun, J.; and Sun, M., editor(s), Formal Methods and Software Engineering - 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, November 12-16, 2018, Proceedings, volume 11232, of Lecture Notes in Computer Science, pages 160–176, 2018. Springer
Paper (external PDF)Paper   doi   bibtex
Multi-Scale Verification of Distributed Synchronisation. Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M. CoRR, abs/1809.10655. 2018.
Paper (external PDF)Paper   bibtex
  2017 (7)
CRutoN: Automatic Verification of a Robotic Assistant's Behaviours. Gainer, P.; Dixon, C.; Dautenhahn, K.; Fisher, M.; Hustadt, U.; Saunders, J.; and Webster, M. In Petrucci, L.; Seceleanu, C.; and Cavalcanti, A., editor(s), Critical Systems: Formal Methods and Automated Verification - Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems - and - 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18-20, 2017, Proceedings, volume 10471, of Lecture Notes in Computer Science, pages 119–133, 2017. Springer
Paper (external PDF)Paper   doi   bibtex
The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators. Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M. arXiv, abs/1709.04385. 2017.
Paper (external PDF)Paper   bibtex   abstract
Theorem Proving for Metric Temporal Logic over the Naturals. Hustadt, U.; Ozaki, A.; and Dixon, C. In de Moura, L., editor(s), Proceedings of the 26th International Conference on Automated Deduction (CADE-26), volume 10395, of Lecture Notes in Computer Science, pages 326–343, 2017. Springer
Paper (external PDF)Paper   doi   bibtex
KSP: A Resolution-based Prover for Multimodal K, Abridged Report. Nalon, C.; Hustadt, U.; and Dixon, C. In Sierra, C., editor(s), Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 4919–4923, 2017. ijcai.org
Paper (external PDF)Paper   doi   bibtex
Theorem Proving for Metric Temporal Logic over the Naturals. Hustadt, U.; Ozaki, A.; and Dixon, C. In de Moura, L., editor(s), Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395, of Lecture Notes in Computer Science, pages 326–343, 2017. Springer
Paper (external PDF)Paper   doi   bibtex
Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking. Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M. In Bertrand, N.; and Bortolussi, L., editor(s), Quantitative Evaluation of Systems - 14th International Conference, QEST 2017, Berlin, Germany, September 5-7, 2017, Proceedings, volume 10503, of Lecture Notes in Computer Science, pages 224–239, 2017. Springer
Paper (external PDF)Paper   doi   bibtex
The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators. Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M. CoRR, abs/1709.04385. 2017.
Paper (external PDF)Paper   bibtex
  2016 (4)
Probabilistic Model Checking of Ant-Based Positionless Swarming. Gainer, P.; Dixon, C.; and Hustadt, U. In Alboul, L.; Damian, D. D.; and Aitken, J. M., editor(s), Proceedings of the 17th Annual Conference Towards Autonomous Robotic Systems (TAROS 2016), volume 9716, of Lecture Notes in Computer Science, pages 127–138, 2016. Springer
bibtex
KSP: A Resolution-Based Prover for Multimodal K. Nalon, C.; Hustadt, U.; and Dixon, C. In Olivetti, N.; and Tiwari, A., editor(s), Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016), volume 9706, of Lecture Notes in Computer Science, pages 406–415, 2016.
bibtex
: A Resolution-Based Prover for Multimodal K. Nalon, C.; Hustadt, U.; and Dixon, C. In Olivetti, N.; and Tiwari, A., editor(s), Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, volume 9706, of Lecture Notes in Computer Science, pages 406–415, 2016. Springer
Paper (external PDF)Paper   doi   bibtex
Probabilistic Model Checking of Ant-Based Positionless Swarming. Gainer, P.; Dixon, C.; and Hustadt, U. In Alboul, L.; Damian, D. D.; and Aitken, J. M., editor(s), Towards Autonomous Robotic Systems - 17th Annual Conference, TAROS 2016, Sheffield, UK, June 26 - July 1, 2016, Proceedings, volume 9716, of Lecture Notes in Computer Science, pages 127–138, 2016. Springer
Paper (external PDF)Paper   doi   bibtex
  2015 (4)
Ordered Resolution for Coalition Logic. Hustadt, U.; Gainer, P.; Dixon, C.; Nalon, C.; and Zhang, L. In de Nivelle, H., editor(s), Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015) [Wroclaw, Poland, 20–24 September 2015], volume 9323, of LNAI, pages 165-180, 2015. Springer International Publishing Switzerland
Paper (local PDF)Paper   bibtex   abstract
A Modal-Layered Resolution Calculus for K. Nalon, C.; Hustadt, U.; and Dixon, C. In de Nivelle, H., editor(s), Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015) [Wroclaw, Poland, 20–24 September 2015], volume 9323, of LNAI, pages 181–196, 2015. Springer International Publishing Switzerland
Paper (local PDF)Paper   bibtex   abstract
Ordered Resolution for Coalition Logic. Hustadt, U.; Gainer, P.; Dixon, C.; Nalon, C.; and Zhang, L. In de Nivelle, H., editor(s), Automated Reasoning with Analytic Tableaux and Related Methods - 24th International Conference, TABLEAUX 2015, Wroc\law, Poland, September 21-24, 2015. Proceedings, volume 9323, of Lecture Notes in Computer Science, pages 169–184, 2015. Springer
Paper (external PDF)Paper   doi   bibtex
A Modal-Layered Resolution Calculus for K. Nalon, C.; Hustadt, U.; and Dixon, C. In de Nivelle, H., editor(s), Automated Reasoning with Analytic Tableaux and Related Methods - 24th International Conference, TABLEAUX 2015, Wroc\law, Poland, September 21-24, 2015. Proceedings, volume 9323, of Lecture Notes in Computer Science, pages 185–200, 2015. Springer
Paper (external PDF)Paper   doi   bibtex
  2014 (6)
A resolution-based calculus for Coalition Logic. Nalon, C.; Zhang, L.; Dixon, C.; and Hustadt, U. 2014.
Paper (external PDF)Paper   bibtex   abstract
A Resolution Prover for Coalition Logic. Nalon, C.; Zhang, L.; Dixon, C.; and Hustadt, U. In F.~Mogavero; A.~Murano; and M.~Y.~Vardi, editor(s), Proceedings 2nd International Workshop on Strategic Reasoning (SR 2014), volume 146, of Electronic Proceedings in Theoretical Computer Science, pages 65-74, 2014.
bibtex   abstract
A Resolution Calculus for Branching-Time Temporal Logic CTL. Zhang, L.; Hustadt, U.; and Dixon, C. ACM Transactions on Computational Logic, 15(1): 10:1-38. February 2014.
Paper (local PDF)Paper   bibtex   abstract
A resolution-based calculus for Coalition Logic. Nalon, C.; Zhang, L.; Dixon, C.; and Hustadt, U. J. Log. Comput., 24(4): 883–917. 2014.
Paper (external PDF)Paper   doi   bibtex
A resolution calculus for the branching-time temporal logic CTL. Zhang, L.; Hustadt, U.; and Dixon, C. ACM Trans. Comput. Log., 15(1): 10:1–10:38. 2014.
Paper (external PDF)Paper   doi   bibtex
A Resolution Prover for Coalition Logic. Nalon, C.; Zhang, L.; Dixon, C.; and Hustadt, U. In Mogavero, F.; Murano, A.; and Vardi, M. Y., editor(s), Proceedings 2nd International Workshop on Strategic Reasoning, SR 2014, Grenoble, France, April 5-6, 2014, volume 146, of EPTCS, pages 65–73, 2014.
Paper (external PDF)Paper   doi   bibtex
  2013 (3)
A resolution-based calculus for Coalition Logic (Extended Version). Nalon, C.; Zhang, L.; Dixon, C.; and Hustadt, U. Technical Report ULCS-13-004, Department of Computer Science, University of Liverpool, Liverpool, UK, 2013.
Paper (local PDF)Paper   bibtex   abstract
First-Order Resolution Methods for Modal Logics. Schmidt, R. A.; and Hustadt, U. In Voronkov, A.; and Weidenbach, C., editor(s), Programming Logics, volume 7797, of Lecture Notes in Computer Science, pages 345-391. Springer, 2013.
Paper (external PDF)Paper   doi   bibtex   abstract
First-Order Resolution Methods for Modal Logics. Schmidt, R. A.; and Hustadt, U. In Voronkov, A.; and Weidenbach, C., editor(s), Programming Logics - Essays in Memory of Harald Ganzinger, volume 7797, of Lecture Notes in Computer Science, pages 345–391, 2013. Springer
Paper (external PDF)Paper   doi   bibtex
  2010 (6)
A Comparison of Solvers for Propositional Dynamic Logic. Hustadt, U.; and Schmidt, R. In Konev, B.; Schmidt, R. A.; and Schulz, S., editor(s), Proceedings of the Workshop on Practical Aspect of Automated Reasoning (PAAR-2010) [Edinburgh, Scotland, 14 July 2010], 2010.
Paper (local PDF)Paper   bibtex   abstract
Implementing a fair monodic temporal logic prover. Ludwig, M.; and Hustadt, U. AI Communications, 23(2–3): 69-96. 2010.
Paper (local PDF)Paper   bibtex   abstract
CTL-RP: A computation tree logic resolution prover. Zhang, L.; Hustadt, U.; and Dixon, C. AI Communications, 23(2–3): 111-136. 2010.
Paper (local PDF)Paper   bibtex   abstract
Implementing a fair monodic temporal logic prover. Ludwig, M.; and Hustadt, U. AI Commun., 23(2-3): 69–96. 2010.
Paper (external PDF)Paper   doi   bibtex
CTL-RP: A computation tree logic resolution prover. Zhang, L.; Hustadt, U.; and Dixon, C. AI Commun., 23(2-3): 111–136. 2010.
Paper (external PDF)Paper   doi   bibtex
A Comparison of Solvers for Propositional Dynamic Logic. Hustadt, U.; and Schmidt, R. A. In Schmidt, R. A.; Schulz, S.; and Konev, B., editor(s), Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh, Scotland, UK, July 14, 2010, volume 9, of EPiC Series in Computing, pages 63–73, 2010. EasyChair
Paper (external PDF)Paper   bibtex
  2009 (9)
Fair Derivations in Monodic Temporal Reasoning. Ludwig, M.; and Hustadt, U. In Schmidt, R. A., editor(s), Proceedings of the 22nd International Conference on Automated Deduction (CADE-22), [Montreal, Canada, 2-7 August 2009], volume 5663, of Lecture Notes in Computer Science, pages 261-276, 2009. Springer
Paper (external PDF)Paper   bibtex   abstract
Redundancy Elimination in Monodic Temporal Reasoning. Ludwig, M.; and Hustadt, U. In Peltier, N.; and Sofronie-Stokkermans, V., editor(s), Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP 2009) [Oslo, Norway, 6-7 July 2009], 2009.
Paper (local PDF)Paper   bibtex   abstract
Resolution-Based Model Construction for PLTL. Ludwig, M.; and Hustadt, U. In Lutz, C.; and Raskin, J., editor(s), Proceedings of the 16th International Symposium on Temporal Representation and Reasoning (TIME-2009) [Brixen-Bressanone, Italy, 23-25 July 2009], pages 73-80, 2009. IEEE Computer Society
Paper (local PDF)Paper   bibtex   abstract
A Refined Resolution Calculus for CTL. Zhang, L.; Hustadt, U.; and Dixon, C. In Schmidt, R. A., editor(s), Proceedings of the 22nd International Conference on Automated Deduction (CADE-22), Montreal, Canada, August 2-7, 2009, volume 5663, of Lecture Notes in Computer Science, pages 245-260, 2009. Springer
Paper (external PDF)Paper   bibtex   abstract
Preface. Ranise, S.; and Hustadt, U. Ann. Math. Artif. Intell., 55(1-2): 1–2. 2009.
Paper (external PDF)Paper   doi   bibtex
A Refined Resolution Calculus for CTL. Zhang, L.; Hustadt, U.; and Dixon, C. In Schmidt, R. A., editor(s), Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, volume 5663, of Lecture Notes in Computer Science, pages 245–260, 2009. Springer
Paper (external PDF)Paper   doi   bibtex
Fair Derivations in Monodic Temporal Reasoning. Ludwig, M.; and Hustadt, U. In Schmidt, R. A., editor(s), Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, volume 5663, of Lecture Notes in Computer Science, pages 261–276, 2009. Springer
Paper (external PDF)Paper   doi   bibtex
Redundancy Elimination in Monodic Temporal Reasoning. Ludwig, M.; and Hustadt, U. In Peltier, N.; and Sofronie-Stokkermans, V., editor(s), Proceedings of the 7th International Workshop on First-Order Theorem Proving, FTP 2009, Oslo, Norway, July 6-7, 2009, volume 556, of CEUR Workshop Proceedings, 2009. CEUR-WS.org
Paper (local PDF)Paper   bibtex
Resolution-Based Model Construction for PLTL. Ludwig, M.; and Hustadt, U. In Lutz, C.; and Raskin, J., editor(s), TIME 2009, 16th International Symposium on Temporal Representation and Reasoning, Bressanone-Brixen, Italy, 23-25 July 2009, Proceedings, pages 73–80, 2009. IEEE Computer Society
Paper (external PDF)Paper   doi   bibtex
  2008 (2)
Deciding expressive description logics in the framework of resolution. Hustadt, U.; Motik, B.; and Sattler, U. Information and Computation, 206(5): 579-601. 2008.
Paper (external PDF)Paper   bibtex   abstract
Deciding expressive description logics in the framework of resolution. Hustadt, U.; Motik, B.; and Sattler, U. Inf. Comput., 206(5): 579–601. 2008.
Paper (external PDF)Paper   doi   bibtex
  2007 (5)
Reasoning in Description Logics by a Reduction to Disjunctive Datalog. Hustadt, U.; Motik, B.; and Sattler, U. Journal of Automated Reasoning, 39(3): 351-384. 2007.
Paper (external PDF)Paper   bibtex   abstract
The Axiomatic Translation Principle for Modal Logic. Schmidt, R. A.; and Hustadt, U. ACM Transactions on Computational Logic, 8(4): 19/1-55. 2007.
Paper (external PDF)Paper   bibtex   abstract
Reasoning in Description Logics by a Reduction to Disjunctive Datalog. Hustadt, U.; Motik, B.; and Sattler, U. J. Autom. Reasoning, 39(3): 351–384. 2007.
Paper (external PDF)Paper   doi   bibtex
The axiomatic translation principle for modal logic. Schmidt, R. A.; and Hustadt, U. ACM Trans. Comput. Log., 8(4): 19. 2007.
Paper (external PDF)Paper   doi   bibtex
Computational modal logic. Horrocks, I.; Hustadt, U.; Sattler, U.; and Schmidt, R. A. In Blackburn, P.; van Benthem, J. F. A. K.; and Wolter, F., editor(s), Handbook of Modal Logic, volume 3, of Studies in logic and practical reasoning, pages 181–245. North-Holland, 2007.
Paper (external PDF)Paper   doi   bibtex
  2006 (2)
Automated reasoning about metric and topology. Hustadt, U.; Tishkovsky, D.; Wolter, F.; and Zakharyaschev, M. In Fisher, M.; van der Hoek, W.; Konev, B.; and Lisitsa, A., editor(s), Proceedings of the 10th European Conference on Logics in Artificial Intelligence (JELIA 2006) [Liverpool, UK, 13-15 September 2006], volume 4160, of LNAI, pages 490-493, 2006. Springer
Paper (external PDF)Paper   bibtex   abstract
Automated Reasoning About Metric and Topology. Hustadt, U.; Tishkovsky, D.; Wolter, F.; and Zakharyaschev, M. In Fisher, M.; van der Hoek, W.; Konev, B.; and Lisitsa, A., editor(s), Logics in Artificial Intelligence, 10th European Conference, JELIA 2006, Liverpool, UK, September 13-15, 2006, Proceedings, volume 4160, of Lecture Notes in Computer Science, pages 490–493, 2006. Springer
Paper (external PDF)Paper   doi   bibtex
  2005 (11)
First-Order Temporal Verification in Practice. Fernández-Gago, M. C.; Hustadt, U.; Dixon, C.; Fisher, M.; and Konev, B. Journal of Automated Reasoning, 34(3): 295-321. April 2005.
Paper (external PDF)Paper   bibtex   abstract
Deciding Monodic Fragments by Temporal Resolution. Hustadt, U.; Konev, B.; and Schmidt, R. A. In Nieuwenhuis, R., editor(s), Proceedings of the 20th International Conference on Automated Deduction (CADE-20) [Tallin, Estonia, 22-27 July 2005], volume 3632, of LNAI, pages 204-218, 2005. Springer
Paper (external PDF)Paper   bibtex   abstract
Description Logics and Disjunctive Datalog — The Story so Far. Hustadt, U.; and Motik, B. In Horrocks, I.; Sattler, U.; and Wolter, F., editor(s), Proceedings of the 2005 International Workshop on Description Logics (DL2005) [Edinburgh, Scotland, 26-28 July 2005], volume 189, of CEUR Workshop Proceedings, 2005.
Paper (local PDF)Paper   bibtex   abstract
Data Complexity of Reasoning in Very Expressive Description Logics. Hustadt, U.; Motik, B.; and Sattler, U. In Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI 2005) [Edinburg, Scotland, 30 July - 5 August 2005], pages 466-471, 2005. International Joint Conferences on Artificial Intelligence
Paper (local PDF)Paper   bibtex   abstract
A Decomposition Rule for Decision Procedures by Resolution-Based Calculi. Hustadt, U.; Motik, B.; and Sattler, U. In Baader, F.; and Voronkov, A., editor(s), Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2004) [Montevideo, Uruguay, 14-18 March 2005), pages 21-35, 2005. Springer
Paper (external PDF)Paper   bibtex   abstract
Mechanising first-order temporal resolution. Konev, B.; Degtyarev, A.; Dixon, C.; Fisher, M.; and Hustadt, U. Information and Computation, 199(1-2): 55-86. 2005.
Paper (external PDF)Paper   bibtex   abstract
Mechanising first-order temporal resolution. Konev, B.; Degtyarev, A.; Dixon, C.; Fisher, M.; and Hustadt, U. Inf. Comput., 199(1-2): 55–86. 2005.
Paper (external PDF)Paper   doi   bibtex
First-Order Temporal Verification in Practice. Gago, M. C. F.; Hustadt, U.; Dixon, C.; Fisher, M.; and Konev, B. J. Autom. Reasoning, 34(3): 295–321. 2005.
Paper (external PDF)Paper   doi   bibtex
Deciding Monodic Fragments by Temporal Resolution. Hustadt, U.; Konev, B.; and Schmidt, R. A. In Nieuwenhuis, R., editor(s), Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, volume 3632, of Lecture Notes in Computer Science, pages 204–218, 2005. Springer
Paper (external PDF)Paper   doi   bibtex
Description Logics and Disjunctive Datalog - The Story so Far. Hustadt, U.; and Motik, B. In Horrocks, I.; Sattler, U.; and Wolter, F., editor(s), Proceedings of the 2005 International Workshop on Description Logics (DL2005), Edinburgh, Scotland, UK, July 26-28, 2005, volume 147, of CEUR Workshop Proceedings, 2005. CEUR-WS.org
Paper (local PDF)Paper   bibtex
Data Complexity of Reasoning in Very Expressive Description Logics. Hustadt, U.; Motik, B.; and Sattler, U. In Kaelbling, L. P.; and Saffiotti, A., editor(s), IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30 - August 5, 2005, pages 466–471, 2005. Professional Book Center
Paper (local PDF)Paper   bibtex
  2004 (15)
SCAN is complete for all Sahlqvist formulae. Goranko, V.; Hustadt, U.; Schmidt, R.; and Vakarelov, D. In Berghammer, R.; Möller, B.; and Struth, G., editor(s), Revised Selected Papers of the 7th International Seminar on Relational Methods in Computer Science and the 2nd International Workshop on Kleene Algebra [Bad Malente, Germany, 12-17 May 2003], volume 3051, of LNCS, pages 149-162, 2004. Springer
Paper (local PDF)Paper   bibtex   abstract
TRP++: A temporal resolution prover. Hustadt, U.; and Konev, B. In Baaz, M.; Makowsky, J.; and Voronkov, A., editor(s), Collegium Logicum, pages 65-79. Kurt Gödel Society, 2004.
Paper (local PDF)Paper   bibtex   abstract
TeMP: A Temporal Monodic Prover. Hustadt, U.; Konev, B.; Riazanov, A.; and Voronkov, A. In Basin, D. A.; and Rusinowitch, M., editor(s), Proceedings of the Second International Joint Conference on Automated Reasoning (IJCAR 2004) [Cork, Ireland, 4-8 July 2004], volume 3097, of LNAI, pages 326-330, 2004. Springer
Paper (local PDF)Paper   bibtex   abstract
TeMP: A Temporal Monodic Prover. Hustadt, U.; Konev, B.; Riazanov, A.; and Voronkov, A. Technical Report ULCS-04-004, Department of Computer Science, University of Liverpool, Liverpool, UK, 2004.
Paper (local PostScript)Paper   bibtex   abstract
Reasoning in Description Logics with a Concrete Domain in the Framework of Resolution. Hustadt, U.; Motik, B.; and Sattler, U. In de Mántaras, R. L.; and Saitta, L., editor(s), Proceedings of the 16th European Conference on Artificial Intelligence (ECAI 2004), pages 353-357, 2004. IOS Press
Paper (local PDF)Paper   bibtex   abstract
Reasoning for Description Logics around SHIQ in a Resolution Framework. Hustadt, U.; Motik, B.; and Sattler, U. Technical Report 3-8-04/04, FZI, Karlsruhe, Germany, June 2004.
Paper (local PDF)Paper   bibtex   abstract
Reducing SHIQ- Description Logic to Disjunctive Datalog Programs. Hustadt, U.; Motik, B.; and Sattler, U. In Dubois, D.; Welty, C.; and Williams, M., editor(s), Proceedings of the 9th International Conference on Knowledge Representation and Reasoning (KR2004) [Whistler, Canada, June 2-5, 2004], pages 152-162, 2004. AAAI Press
Paper (local PDF)Paper   bibtex   abstract
A Survey of Decidable First-Order Fragments and Description Logics. Hustadt, U.; Schmidt, R. A.; and Georgieva, L. JoRMiCS, 1: 251-276. 2004.
Paper (local PDF)Paper   bibtex   abstract
Two proof systems for Peirce algebras. Schmidt, R. A.; Or\lowska, E.; and Hustadt, U. In Berghammer, R.; Möller, B.; and Struth, G., editor(s), Revised Selected Papers of the 7th International Seminar on Relational Methods in Computer Science and the 2nd International Workshop on Kleene Algebra, volume 3051, of LNCS, pages 238-251, 2004. Springer
Paper (local PDF)Paper   bibtex   abstract
Interactions between Knowledge, Action, and Commitment within Agent Dynamic Logic. Schmidt, R. A.; Tishkovsky, D.; and Hustadt, U. Studia Logica, 78(3): 381-415. December 2004.
Paper (external PDF)Paper   bibtex   abstract
Interactions between Knowledge, Action and Commitment within Agent Dynamic Logic. Schmidt, R. A.; Tishkovsky, D.; and Hustadt, U. Studia Logica, 78(3): 381–415. 2004.
Paper (external PDF)Paper   doi   bibtex
TeMP: A Temporal Monodic Prover. Hustadt, U.; Konev, B.; Riazanov, A.; and Voronkov, A. In Basin, D. A.; and Rusinowitch, M., editor(s), Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, volume 3097, of Lecture Notes in Computer Science, pages 326–330, 2004. Springer
Paper (external PDF)Paper   doi   bibtex
Reasoning in Description Logics with a Concrete Domain in the Framework of Resolution. Hustadt, U.; Motik, B.; and Sattler, U. In de Mántaras, R. L.; and Saitta, L., editor(s), Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI'2004, including Prestigious Applicants of Intelligent Systems, PAIS 2004, Valencia, Spain, August 22-27, 2004, pages 353–357, 2004. IOS Press
bibtex
Reducing SHIQ-Description Logic to Disjunctive Datalog Programs. Hustadt, U.; Motik, B.; and Sattler, U. In Dubois, D.; Welty, C. A.; and Williams, M., editor(s), Principles of Knowledge Representation and Reasoning: Proceedings of the Ninth International Conference (KR2004), Whistler, Canada, June 2-5, 2004, pages 152–162, 2004. AAAI Press
Paper (external PDF)Paper   bibtex
A Decomposition Rule for Decision Procedures by Resolution-Based Calculi. Hustadt, U.; Motik, B.; and Sattler, U. In Baader, F.; and Voronkov, A., editor(s), Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings, volume 3452, of Lecture Notes in Computer Science, pages 21–35, 2004. Springer
Paper (external PDF)Paper   doi   bibtex
  2003 (16)
Hyperresolution for Guarded Formulae. Georgieva, L.; Hustadt, U.; and Schmidt, R. A. Journal of Symbolic Computation, 36(1-2): 163-192. 2003.
Paper (external PDF)Paper   bibtex   abstract
SCAN is complete for all Sahlqvist formulae. Goranko, V.; Hustadt, U.; Schmidt, R.; and Vakarelov, D. In Berghammer, R.; and Möller, B., editor(s), Proceedings of the 7th International Seminar on Relational Methods in Computer Science (RelMiCS-7) [Bad Malente, Germany, 12-17 May 2003], pages 230-241, 2003. Christian-Albrechts-Universität Kiel
Paper (external PDF)Paper   bibtex   abstract
TRP++ 2.0: A temporal resolution prover. Hustadt, U.; and Konev, B. In Proceedings of the 19th International Conference on Automated Deduction (CADE-19) [Miamia Beach, USA, July/August 2003], volume 2741, of Lecture Notes in Artificial Intelligence, pages 274-278, 2003. Springer
Paper (local PDF)Paper   bibtex   abstract
Reducing SHIQ- Description Logic to Disjunctive Datalog Programs. Hustadt, U.; Motik, B.; and Sattler, U. Technical Report 1-8-11/03, FZI, Karlsruhe, Germany, November 2003. Revised version submitted to KR conference, http://www.fzi.de/wim/eng/publikationen.php?id=1103
Paper (local PDF)Paper   bibtex   abstract
Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case. Konev, B.; Degtyarev, A.; Dixon, C.; Fisher, M.; and Hustadt, U. 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], pages 72-82, 2003. IEEE Computer Society
Paper (external PDF)Paper   bibtex   abstract
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. Schmidt, R. A.; and Hustadt, U. In Proceedings of the 19th International Conference on Automated Deduction (CADE-19) [Miami Beach, USA, July/August 2003], volume 2741, of Lecture Notes in Artificial Intelligence, pages 412-426, 2003. Springer
Paper (external PDF)Paper   bibtex   abstract
Mechanised Reasoning and Model Generation for Extended Modal Logics. Schmidt, R. A.; and Hustadt, U. In de Swart, H.; Orlowska, E.; Schmidt, G.; and Roubens, M., editor(s), Theory and Applications of Relational Structures as Knowledge Instruments. COST Action 274, TARSKI. Revised Papers, volume 2929, of LNCS, pages 38-67. December 2003.
Paper (external PDF)Paper   bibtex   abstract
Mechanised Reasoning and Model Generation for Extended Modal Logics. Schmidt, R. A.; and Hustadt, U. Technical Report CSPP-19, University of Manchester, UK, January 2003. Submitted for publication.
Paper (local PDF)Paper   bibtex   abstract
Two proof systems for Peirce algebras. Schmidt, R. A.; Or\lowska, E.; and Hustadt, U. In Berghammer, R.; and Möller, B., editor(s), Proceedings of the 7th International Seminar on Relational Methods in Computer Science (RelMiCS-7) [Bad Malente, Germany, 12-17 May 2003], pages 197–203, 2003. Christian-Albrechts-Universität Kiel
Paper (local PDF)Paper   bibtex   abstract
Hyperresolution for guarded formulae. Georgieva, L.; Hustadt, U.; and Schmidt, R. A. J. Symb. Comput., 36(1-2): 163–192. 2003.
Paper (external PDF)Paper   doi   bibtex
SCAN Is Complete for All Sahlqvist Formulae. Goranko, V.; Hustadt, U.; Schmidt, R. A.; and Vakarelov, D. In Berghammer, R.; Möller, B.; and Struth, G., editor(s), Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Bad Malente, Germany, May 12-17, 2003, Revised Selected Papers, volume 3051, of Lecture Notes in Computer Science, pages 149–162, 2003. Springer
Paper (external PDF)Paper   doi   bibtex
Two Proof Systems for Peirce Algebras. Schmidt, R. A.; Orlowska, E.; and Hustadt, U. In Berghammer, R.; Möller, B.; and Struth, G., editor(s), Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Bad Malente, Germany, May 12-17, 2003, Revised Selected Papers, volume 3051, of Lecture Notes in Computer Science, pages 238–251, 2003. Springer
Paper (external PDF)Paper   doi   bibtex
TRP++2.0: A Temporal Resolution Prover. Hustadt, U.; and Konev, B. In Baader, F., editor(s), Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, volume 2741, of Lecture Notes in Computer Science, pages 274–278, 2003. Springer
Paper (external PDF)Paper   doi   bibtex
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. Schmidt, R. A.; and Hustadt, U. In Baader, F., editor(s), Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, volume 2741, of Lecture Notes in Computer Science, pages 412–426, 2003. Springer
Paper (external PDF)Paper   doi   bibtex
Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case. Konev, B.; Degtyarev, A.; Dixon, C.; Fisher, M.; and Hustadt, U. In 10th International Symposium on Temporal Representation and Reasoning / 4th International Conference on Temporal Logic (TIME-ICTL 2003), 8-10 July 2003, Cairns, Queensland, Australia, pages 72–82, 2003. IEEE Computer Society
Paper (external PDF)Paper   doi   bibtex
Mechanised Reasoning and Model Generation for Extended Modal Logics. Schmidt, R. A.; and Hustadt, U. In de Swart, H. C. M.; Orlowska, E.; Schmidt, G.; and Roubens, M., editor(s), Theory and Applications of Relational Structures as Knowledge Instruments, COST Action 274, TARSKI, Revised Papers, volume 2929, of Lecture Notes in Computer Science, pages 38–67. Springer, 2003.
Paper (external PDF)Paper   doi   bibtex
  2002 (10)
Combinations of Modal Logics. Bennett, B.; Dixon, C.; Fisher, M.; Hustadt, U.; Franconi, E.; Horrocks, I.; and de Rijke, M. AI Review, 17(1): 1-20. March 2002.
Paper (external PDF)Paper   bibtex   abstract
A new clausal class decidable by hyperresolution. Georgieva, L.; Hustadt, U.; and Schmidt, R. A. In Voronkov, A., editor(s), Proceedings of the 18th International Conference on Automated Deduc tion (CADE-18) [Copenhagen, Denmark, 27-30 July 2002], volume 2392, of LNAI, pages 258-272, 2002. Springer
Paper (external PDF)Paper   bibtex   abstract
On the relationship between decidable fragments, non-classical logics, and de scription logics. Georgieva, L.; Hustadt, U.; and Schmidt, R. A. In Horrocks, I.; and Tessaris, S., editor(s), Proceedings of the 2002 International Workshop on Description Logics (DL 2002) [Toulouse, France, 19-21 April 2002], pages 25-36, 2002. Proceedings are also available as CEUR Publication at http://CEUR-WS.org/Vol-53/
Paper (local PDF)Paper   bibtex   abstract
Using Resolution for Testing Modal Satisfiability and Building Models. Hustadt, U.; and Schmidt, R. A. Journal of Automated Reasoning, 28(2): 205-232. February 2002.
Paper (external PDF)Paper   bibtex   abstract
Scientific Benchmarking with Temporal Logic Decision Procedures. Hustadt, U.; and Schmidt, R. A. In Fensel, D.; Giunchiglia, F.; McGuinness, D.; and Williams, M., editor(s), Principles of Knowledge Representation and Reasoning: Proceedings of the Eighth International Conference (KR 2002) [Toulouse, France, 22-25 April 2002], pages 533-544, 2002. Morgan Kaufmann
Paper (local PDF)Paper   bibtex   abstract
Combinations of Modal Logics. Bennett, B.; Dixon, C.; Fisher, M.; Hustadt, U.; Franconi, E.; Horrocks, I.; and de Rijke, M. Artif. Intell. Rev., 17(1): 1–20. 2002.
Paper (external PDF)Paper   doi   bibtex
Using Resolution for Testing Modal Satisfiability and Building Models. Hustadt, U.; and Schmidt, R. A. J. Autom. Reasoning, 28(2): 205–232. 2002.
Paper (external PDF)Paper   doi   bibtex
A New Clausal Class Decidable by Hyperresolution. Georgieva, L.; Hustadt, U.; and Schmidt, R. A. In Voronkov, A., editor(s), Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings, volume 2392, of Lecture Notes in Computer Science, pages 260–274, 2002. Springer
Paper (external PDF)Paper   doi   bibtex
On the relationship between decidable fragments, non-classical logics, and description logics. Georgieva, L.; Hustadt, U.; and Schmidt, R. A. In Horrocks, I.; and Tessaris, S., editor(s), Proceedings of the 2002 International Workshop on Description Logics (DL2002), Toulouse, France, April 19-21, 2002, volume 53, of CEUR Workshop Proceedings, 2002. CEUR-WS.org
Paper (local PostScript)Paper   bibtex
Scientific Benchmarking with Temporal Logic Decision Procedures. Hustadt, U.; and Schmidt, R. A. In Fensel, D.; Giunchiglia, F.; McGuinness, D. L.; and Williams, M., editor(s), Proceedings of the Eights International Conference on Principles and Knowledge Representation and Reasoning (KR-02), Toulouse, France, April 22-25, 2002, pages 533–546, 2002. Morgan Kaufmann
bibtex
  2001 (12)
Resolution Decision Procedures. Fermüller, C.; Leitsch, A.; Hustadt, U.; and Tammet, T. In Robinson, A.; and Voronkov, A., editor(s), Handbook of Automated Reasoning, 25, pages 1791-1850. Elsevier, 2001.
Paper (external PDF)Paper   bibtex   abstract
Computational space efficiency and minimal model generation for guarded formulae. Georgieva, L.; Hustadt, U.; and Schmidt, R. A. In Goreé, R.; Leitsch, A.; and Nipkow, T., editor(s), International Joint Conference on Automated Reasoning IJCAR 2001: Short Papers, volume DII 11/01, of Technical Report, pages 34-43, 2001. Departimento di Ingegneria dell'Informazione, Universitá degli Studi di Siena
Paper (local PDF)Paper   bibtex   abstract
Computational space efficiency and minimal model generation for guarded formulae. Georgieva, L.; Hustadt, U.; and Schmidt, R. A. In Nieuwenhuis, R.; and Voronkov, A., editor(s), Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001) [Havana, Cuba, 3-7 December 2001], volume 2250, of LNAI, pages 85-99, 2001. Springer
Paper (local PDF)Paper   bibtex   abstract
Translating PLTL into WS1S: Application Description. Hirsch, B.; and Hustadt, U. In Methods for Modalities II. University of Amsterdam, 2001.
Paper (local PDF)Paper   bibtex   abstract
Verification within the KARO Agent Theory. Hustadt, U.; Dixon, C.; Schmidt, R. A.; Fisher, M.; Meyer, J. C.; and van der Hoek, W. In Rouff, C. A.; Hinchey, M. G.; Rash, J. L.; Truszkowski, W.; and Gordon-Spears, D., editor(s), Agent Technology from a Formal Perspective, of NASA Monographs in Systems and Software Engineering, pages 193-226. Springer, 2001.
Paper (local PDF)Paper   bibtex   abstract
Verification within the KARO Agent Theory. Hustadt, U.; Dixon, C.; Schmidt, R. A.; Fisher, M.; Meyer, J. C.; and van der Hoek, W. In Rash, J. L.; Rouff, C. A.; Truszkowski, W.; Gordon, D.; and Hinchey, M. G., editor(s), 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], volume 1871, of LNAI, pages 33-47, 2001. Springer
Paper (local PDF)Paper   bibtex   abstract
Reasoning about agents in the KARO framework. Hustadt, U.; Dixon, C.; Schmidt, R. A.; Fisher, M.; Meyer, J.; and van der Hoek, W. In Bettini, C.; and Montanari, A., editor(s), Proceedings of the Eighth International Symposium on Temporal Representation and Reasoning (TIME-01) [Cividale del Friuli, Italy, 14-16 June 2001], pages 206-213, 2001. IEEE Press
Paper (external PDF)Paper   bibtex   abstract
Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers. Hustadt, U.; and Schmidt, R. A. In Giunchiglia, E.; and Massacci, F., editor(s), Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, of Technical Report DII 14/01, pages 68-76, 2001. Dipartimento di Ingegneria dell'Informazione, Unversitá degli Studi di Siena
Paper (local PDF)Paper   bibtex   abstract
Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 2, Dov M. Gabbay, Mark A. Reynolds, and Marcelo Finger. Hustadt, U. Journal of Logic, Language and Information, 10(3): 406–410. 2001.
Paper (external PDF)Paper   doi   bibtex
Computational Space Efficiency and Minimal Model Generation for Guarded Formulae. Georgieva, L.; Hustadt, U.; and Schmidt, R. A. In Nieuwenhuis, R.; and Voronkov, A., editor(s), Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings, volume 2250, of Lecture Notes in Computer Science, pages 85–99, 2001. Springer
Paper (external PDF)Paper   doi   bibtex
Reasoning about agents in the KARO framework. Hustadt, U.; Dixon, C.; Schmidt, R. A.; Fisher, M.; Meyer, J. C.; and van der Hoek, W. In Eigth International Symposium on Temporal Representation and Reasoning, TIME-01, Civdale del Friuli, Italy, June 14-16, 2001, pages 206–213, 2001. IEEE Computer Society
Paper (external PDF)Paper   doi   bibtex
Resolution Decision Procedures. Fermüller, C. G.; Leitsch, A.; Hustadt, U.; and Tammet, T. In Robinson, J. A.; and Voronkov, A., editor(s), Handbook of Automated Reasoning (in 2 volumes), pages 1791–1849. Elsevier and MIT Press, 2001.
Paper (external PDF)Paper   doi   bibtex
  2000 (14)
Resolution-Based Methods for Modal Logics. De Nivelle, H.; Schmidt, R. A.; and Hustadt, U. Logic Journal of the IGPL, 8(3): 265-292. May 2000.
Paper (local PDF)Paper   bibtex   abstract
A Resolution-Based Decision Procedure for Extensions of K4. Ganzinger, H.; Hustadt, U.; Meyer, C.; and Schmidt, R. A. In Zakharyaschev, M.; Segerberg, K.; de Rijke, M.; and Wansing, H., editor(s), Advances in Modal Logic 2, papers from the second workshop on "Advances in Modal logic," held in Uppsala, Sweden, 1998, pages 225-246, 2000. CSLI Publications
Paper (local PDF)Paper   bibtex   abstract
Hyperresolution for Guarded Formulae. Georgieva, L.; Hustadt, U.; and Schmidt, R. A. In Baumgartner, P.; and Zhang, H., editor(s), Proceedings of the Third International Workshop on First-Order Theorem Proving (FTP 2000) [St. Andrews, Scotland, 2-4 July 2000], volume 5/2000, of Fachberichte Informatik, pages 101-112, 2000. Institut für Informatik, Universität Koblenz-Landau
Paper (local PDF)Paper   bibtex   abstract
Normal Forms and Proofs in Combined Modal and Temporal Logics. Hustadt, U.; Dixon, C.; Schmidt, R. A.; and Fisher, M. In Proceedings of the Third International Workshop on Frontiers of Combining Systems (FroCoS 2000) [Nancy, France, 22-24 March 2000], volume 1794, of LNAI, pages 73-87, 2000. Springer
Paper (local PDF)Paper   bibtex   abstract
Using Resolution for Testing Modal Satisfiability and Building Models. Hustadt, U.; and Schmidt, R. A. In Gent, I.; van Maaren, H.; and Walsh, T., editor(s), SAT2000: Highlights of Satisfiability Research in the Year 2000, volume 63, of Frontiers in Artificial Intelligence and Applications, pages 459-483. IOS Press, 2000.
Paper (local PDF)Paper   bibtex   abstract
MSPASS: Modal reasoning by translation and first-order resolution. Hustadt, U.; and Schmidt, R. In Dyckhoff, R., editor(s), Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000) [St. Andrews, Scotland, 3-7 July 2000], volume 1847, of LNAI, pages 67-71, 2000. Springer
Paper (local PDF)Paper   bibtex   abstract
A Resolution Decision Procedure for Fluted Logic. Schmidt, R. A.; and Hustadt, U. In McAllester, D., editor(s), Proceedings of the 17th International Conference on Automated Deduction (CADE-17) [Pittsburgh, USA, 17-20 June2000], volume 1831, of Lecture Notes in Artificial Intelligence, pages 433-448, 2000. Springer
Paper (external PDF)Paper   bibtex   abstract
Resolution-Based Methods for Modal Logics. Hustadt, U.; de Nivelle, H.; and Schmidt, R. A. Log. J. IGPL, 8(3): 265–292. 2000.
Paper (external PDF)Paper   doi   bibtex
Hyperresolution for Guarded Formulae. Georgieva, L.; Hustadt, U.; and Schmidt, R. A. In Ohlbach, H. J.; Endriss, U.; Rodrigues, O.; and Schlobach, S., editor(s), Proceedings of the Seventh Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice, King's College London, UK, 20-21 July 2000, volume 32, of CEUR Workshop Proceedings, 2000. CEUR-WS.org
Paper (external PDF)Paper   bibtex
Practical Proof Methods for Combined Modal and Temporal Logics. Hustadt, U. In Ohlbach, H. J.; Endriss, U.; Rodrigues, O.; and Schlobach, S., editor(s), Proceedings of the Seventh Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice, King's College London, UK, 20-21 July 2000, volume 32, of CEUR Workshop Proceedings, 2000. CEUR-WS.org
Paper (external PDF)Paper   bibtex
A Resolution Decision Procedure for Fluted Logic. Schmidt, R. A.; and Hustadt, U. In McAllester, D. A., editor(s), Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, volume 1831, of Lecture Notes in Computer Science, pages 433–448, 2000. Springer
Paper (external PDF)Paper   doi   bibtex
Verification within the KARO Agent Theory. Hustadt, U.; Dixon, C.; Schmidt, R. A.; Fisher, M.; Meyer, J. C.; and van der Hoek, W. In Rash, J. L.; Rouff, C. A.; Truszkowski, W.; Gordon, D. F.; and Hinchey, M. G., editor(s), Formal Approaches to Agent-Based Systems, First International Workshop, FAABS 2000 Greenbelt, MD, USA, April 5-7, 2000, Revised Papers, volume 1871, of Lecture Notes in Computer Science, pages 33–47, 2000. Springer
Paper (external PDF)Paper   doi   bibtex
Normal Forms and Proofs in Combined Modal and Temporal Logics. Hustadt, U.; Dixon, C.; Schmidt, R. A.; and Fisher, M. In Kirchner, H.; and Ringeissen, C., editor(s), Frontiers of Combining Systems, Third International Workshop, FroCoS 2000, Nancy, France, March 22-24, 2000, Proceedings, volume 1794, of Lecture Notes in Computer Science, pages 73–87, 2000. Springer
Paper (external PDF)Paper   doi   bibtex
MSPASS: Modal Reasoning by Translation and First-Order Resolution. Hustadt, U.; and Schmidt, R. A. In Dyckhoff, R., editor(s), Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings, volume 1847, of Lecture Notes in Computer Science, pages 67–71, 2000. Springer
Paper (external PDF)Paper   doi   bibtex
  1999 (11)
Maslov's Class K Revisited. Hustadt, U.; and Schmidt, R. A. In Ganzinger, H., editor(s), Proceedings of the 16th International Conference on Automated Deduction (CADE-16) [Trento, Italy, 7-10 July 1999], volume 1632, of Lecture Notes in Artificial Intelligence, pages 172-186, 1999. Springer
Paper (local PDF)Paper   bibtex   abstract
On the relation of resolution and tableaux proof systems for description logics. Hustadt, U.; and Schmidt, R. A. In Dean, T., editor(s), Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI'99) [Stockholm, Sweden, 31 July-6 August 1999], volume 1, pages 202-207, 1999. Morgan Kaufmann
Paper (local PDF)Paper   bibtex   abstract
An Empirical Analysis of Modal Theorem Provers. Hustadt, U.; and Schmidt, R. A. Journal of Applied Non-Classical Logics, 9(4): 479-522. 1999.
Paper (local PDF)Paper   bibtex   abstract
Issues of Decidability for Description Logics in the Framework of Resolution. Hustadt, U.; and Schmidt, R. A. In Caferra, R.; and Salzer, G., editor(s), Automated Deduction in Classical and Non-Classical Logics, volume 1761, of LNAI, pages 192-206, 1999. Springer
Paper (external PDF)Paper   bibtex   abstract
MSPASS: Subsumption Testing with SPASS. Hustadt, U.; Schmidt, R. A.; and Weidenbach, C. In Lambrix, P.; Borgida, A.; Lenzerini, M.; Möller, R.; and Patel-Schneider, P., editor(s), Proceedings of the International Workshop on Description Logics (DL'99) [Linköping University, Sweden], pages 136-137, 1999. Linköping University
Paper (local PDF)Paper   bibtex   abstract
Resolution-Based Decision Procedures for Subclasses of First-Order Logic. Hustadt, U. Ph.D. Thesis, Universität des Saarlandes, Saarbrücken, Germany, November 1999.
Paper (local PDF)Paper   bibtex   abstract
Resolution based decision procedures for subclasses of first-order logic. Hustadt, U. Ph.D. Thesis, Saarland University, Saarbrücken, Germany, 1999.
Paper (external PDF)Paper   bibtex
An empirical analysis of modal theorem provers. Hustadt, U.; and Schmidt, R. A. J. Appl. Non Class. Logics, 9(4): 479–522. 1999.
Paper (external PDF)Paper   doi   bibtex
Maslov's Class K Revisited. Hustadt, U.; and Schmidt, R. A. In Ganzinger, H., editor(s), Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, volume 1632, of Lecture Notes in Computer Science, pages 172–186, 1999. Springer
Paper (external PDF)Paper   doi   bibtex
MSPASS: Subsumption Testing with SPASS. Hustadt, U.; Schmidt, R. A.; and Weidenbach, C. In Lambrix, P.; Borgida, A.; Lenzerini, M.; Möller, R.; and Patel-Schneider, P. F., editor(s), Proceedings of the 1999 International Workshop on Description Logics (DL'99), Linköping, Sweden, July 30 - August 1, 1999, volume 22, of CEUR Workshop Proceedings, 1999. CEUR-WS.org
Paper (local PostScript)Paper   bibtex
On the Relation of Resolution and Tableaux Proof Systems for Description Logics. Hustadt, U.; and Schmidt, R. A. In Dean, T., editor(s), Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, IJCAI 99, Stockholm, Sweden, July 31 - August 6, 1999. 2 Volumes, 1450 pages, pages 110–117, 1999. Morgan Kaufmann
Paper (local PDF)Paper   bibtex
  1998 (6)
Issues of Decidability for Description Logics in the Framework of Resolution. Hustadt, U.; and Schmidt, R. A. In Caferra, R.; and Salzer, G., editor(s), Proceedings of the 2nd International Workshop on First-order Theorem Proving (FTP'98), volume E1852-GS-981, of Technical report, pages 152-161, Vienna, Austria, 1998. Technische Universität Wien
Paper (local PDF)Paper   bibtex   abstract
Simplification and Backjumping in Modal Tableau. Hustadt, U.; and Schmidt, R. A. In de Swart, H., editor(s), Proceedings the the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'98) [Oisterwijk, The Netherlands, 5-8 May 1998], volume 1397, of Lecture Notes in Computer Science, pages 187-201, 1998. Springer
Paper (local PDF)Paper   bibtex   abstract
Optimised Functional Translation and Resolution. Hustadt, U.; Schmidt, R. A.; and Weidenbach, C. In de Swart, H., editor(s), Proceddings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'98) [Oisterwijk, The Netherlands, 5-8 May 1998], volume 1397, of Lecture Notes in Computer Science, pages 36-37, 1998. Springer
Paper (external PDF)Paper   bibtex   abstract
A Resolution-Based Decision Procedure for Extensions of K4. Ganzinger, H.; Hustadt, U.; Meyer, C.; and Schmidt, R. A. In Zakharyaschev, M.; Segerberg, K.; de Rijke, M.; and Wansing, H., editor(s), Advances in Modal Logic 2, papers from the second workshop on "Advances in Modal logic," held in Uppsala, Sweden, 16-18 October 1998, pages 225–246, 1998. CSLI Publications
bibtex
Issues of Decidability for Description Logics in the Framework of Resolution. Hustadt, U.; and Schmidt, R. A. In Caferra, R.; and Salzer, G., editor(s), Automated Deduction in Classical and Non-Classical Logics, Selected Papers, volume 1761, of Lecture Notes in Computer Science, pages 191–205, 1998. Springer
Paper (external PDF)Paper   doi   bibtex
Simplification and Backjumping in Modal Tableau. Hustadt, U.; and Schmidt, R. A. In de Swart, H. C. M., editor(s), Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX '98, Oisterwijk, The Netherlands, May 5-8, 1998, Proceedings, volume 1397, of Lecture Notes in Computer Science, pages 187–201, 1998. Springer
Paper (external PDF)Paper   doi   bibtex
  1997 (3)
On Evaluating Decision Procedures for Modal Logics. Hustadt, U.; and Schmidt, R. A. In Pollack, M., editor(s), Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97) [Nagoya, Japan, 23-29 August 1997], volume 1, pages 202-207, August 1997. Morgan Kaufmann An extended version is available as Research Report MPI-I-97-2-003, Max-Planck-Institut für Informatik, Saarbrücken, Germany.
Paper (local PDF)Paper   bibtex   abstract
On evaluating decision procedures for modal logic. Hustadt, U.; and Schmidt, R. A. Technical Report MPI-I-97-2-003, Max-Planck-Institut für Informatik, Saarbrücken, Germany, February 1997.
Paper (local PDF)Paper   bibtex   abstract
On Evaluating Decision Procedures for Modal Logic. Hustadt, U.; and Schmidt, R. A. In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, IJCAI 97, Nagoya, Japan, August 23-29, 1997, 2 Volumes, pages 202–209, 1997. Morgan Kaufmann
Paper (local PDF)Paper   bibtex
  1996 (1)
Translating Graded Modalities into Predicate Logics. Ohlbach, H. J.; Schmidt, R. A.; and Hustadt, U. In Wansing, H., editor(s), Proof Theory of Modal Logic, volume 2, of Applied Logic Series, pages 253-291. Kluwer, Dordrecht, The Netherlands, 1996.
Paper (external PDF)Paper   bibtex   abstract
  1995 (2)
Symbolic Arithmetical Reasoning with Qualified Number Restrictions. Ohlbach, H. J.; Schmidt, R. A.; and Hustadt, U. In Borgida, A.; Lenzerini, M.; Nardi, D.; and Nebel, B., editor(s), International Workshop on Description Logics (DL'95) [Rome, Italy, 2-3 June 1995], pages 89-95, 1995. Proceedings appeared as Technical Report RAP.07.95, Dipartimento di Informatica e Sistemistica, Univ. degli studia di Roma, 1995
Paper (local PDF)Paper   bibtex   abstract
Translating Graded Modalities into Predicate Logic. Ohlbach, H. J.; Schmidt, R. A.; and Hustadt, U. Technical Report MPI-I-95-2-008, Max-Planck-Institut für Informatik, Saarbrücken, 1995. Also appeared in H. Wansing, editor, Proof Theory of Modal Logic, Kluwer, 1996.
Paper (local PDF)Paper   bibtex   abstract
  1994 (4)
Do we need the closed-world assumption in knowledge representation. Hustadt, U. In Baader, F.; Buchheit, M.; Jeusfeld, M. A.; and Nutt, W., editor(s), Working Notes of the KI'94 Workshop: Reasoning about Structured Objects: Knowledge Representation Meets Databases (KRDB'94) [Saarbrücken, Germany, 20-21 September 1994], pages 24-26, 1994. Appeared as Document D-94-11, DFKI, Saarbrücken, Germany as well as CEUR Workshop Proceedings, Vol. 1
Paper (local PDF)Paper   bibtex   abstract