Ullrich Hustadt's Papers and Publications

BibBase hustadt, u
generated by bibbase.org
  2023 (1)
Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic. Nalon, C.; Hustadt, U.; Papacchini, F.; and Dixon, C. In Pientka, B.; and Tinelli, C., editor(s), Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings, volume 14132, of Lecture Notes in Computer Science, pages 382–400, 2023. Springer
Paper (external PDF)Paper   doi   link   bibtex  
  2022 (3)
Local is Best: Efficient Reductions to Modal Logic K. Papacchini, F.; Nalon, C.; Hustadt, U.; and Dixon, C. J. Autom. Reason., 66(4): 639–666. 2022.
Paper (external PDF)Paper   doi   link   bibtex  
Correction to: Local is Best: Efficient Reductions to Modal Logic K. Papacchini, F.; Nalon, C.; Hustadt, U.; and Dixon, C. J. Autom. Reason., 66(4): 1099. 2022.
Paper (external PDF)Paper   doi   link   bibtex  
Local Reductions for the Modal Cube. Nalon, C.; Hustadt, U.; Papacchini, F.; and Dixon, C. In Blanchette, J.; Kovács, L.; and Pattinson, D., editor(s), Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385, of Lecture Notes in Computer Science, pages 486–505, 2022. Springer
Paper (external PDF)Paper   doi   link   bibtex  
  2021 (1)
Efficient Local Reductions to Basic Modal Logic. Papacchini, F.; Nalon, C.; Hustadt, U.; and Dixon, C. In Platzer, A.; and Sutcliffe, G., editor(s), Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699, of Lecture Notes in Computer Science, pages 76–92, 2021. Springer
Paper (external PDF)Paper   doi   link   bibtex  
  2020 (3)
Multi-scale verification of distributed synchronisation. Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M. Formal Methods Syst. Des., 55(3): 171–221. 2020.
Paper (external PDF)Paper   doi   link   bibtex  
KSP: Architecture, Refinements, Strategies and Experiments. Nalon, C.; Hustadt, U.; and Dixon, C. J. Autom. Reason., 64(3): 461–484. 2020.
Paper (external PDF)Paper   doi   link   bibtex  
Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations. Hustadt, U.; Ozaki, A.; and Dixon, C. J. Autom. Reason., 64(8): 1553–1610. 2020.
Paper (external PDF)Paper   doi   link   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   link   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   link   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   link   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   link   bibtex  
  2017 (9)
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), Proceedings of the Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems (FMICS-AVoCS 2017), volume 10471, of Lecture Notes in Computer Science, pages 119–133, 2017. Springer
Paper (external PDF)Paper   doi   link   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   link   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   link   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), pages 4919–4923, 2017.
Paper (external PDF)Paper   doi   link   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   link   bibtex  
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   link   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   link   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   link   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   link   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
link   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.
link   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   link   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   link   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   link   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   link   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ław, Poland, September 21-24, 2015. Proceedings, volume 9323, of Lecture Notes in Computer Science, pages 169–184, 2015. Springer
Paper (external PDF)Paper   doi   link   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ław, Poland, September 21-24, 2015. Proceedings, volume 9323, of Lecture Notes in Computer Science, pages 185–200, 2015. Springer
Paper (external PDF)Paper   doi   link   bibtex  
  2014 (6)
A resolution-based calculus for Coalition Logic. Nalon, C.; Zhang, L.; Dixon, C.; and Hustadt, U. 2014.
Paper (external PDF)Paper   link   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.
link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   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   doi   link   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   link   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   link   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   link   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   link   bibtex   abstract  
Preface. Ranise, S.; and Hustadt, U. Ann. Math. Artif. Intell., 55(1-2): 1–2. 2009.
Paper (external PDF)Paper   doi   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   bibtex   abstract  
Reasoning in Description Logics by a Reduction to Disjunctive Datalog. Hustadt, U.; Motik, B.; and Sattler, U. J. Autom. Reason., 39(3): 351–384. 2007.
Paper (external PDF)Paper   doi   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   bibtex  
First-Order Temporal Verification in Practice. Gago, M. C. F.; Hustadt, U.; Dixon, C.; Fisher, M.; and Konev, B. J. Autom. Reason., 34(3): 295–321. 2005.
Paper (external PDF)Paper   doi   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   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   link   bibtex   abstract