Photo of Dr Ullrich Hustadt

Dr Ullrich Hustadt Dr

Reader Computer Science

    Publications

    2020

    Multi-Scale Verification of Distributed Synchronisation (Journal article)

    Gainer, P., Linker, S., Dixon, C., Hustadt, U., & Fisher, M. (n.d.). Multi-Scale Verification of Distributed Synchronisation. Formal Methods in System Design. doi:10.1007/s10703-020-00347-z

    DOI: 10.1007/s10703-020-00347-z

    A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments (Journal article)

    Nalon, C., Hustadt, U., & Dixon, C. L. (2020). A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments. Journal of Automated Reasoning, 64(3), 461-484. doi:10.1007/s10817-018-09503-x

    DOI: 10.1007/s10817-018-09503-x

    KSP A Resolution-Based Theorem Prover for K_n : Architecture, Refinements, Strategies and Experiments (Journal article)

    Nalon, C., Hustadt, U., & Dixon, C. (2020). KSP A Resolution-Based Theorem Prover for K_n : Architecture, Refinements, Strategies and Experiments. Journal of Automated Reasoning, 64, 461-484. doi:10.1007/s10817-018-09503-x

    DOI: 10.1007/s10817-018-09503-x

    Theorem Proving for Pointwise Metric Temporal Logic Overthe Naturals via Translations (Journal article)

    Hustadt, U., Ozaki, A., & Dixon, C. (2020). Theorem Proving for Pointwise Metric Temporal Logic Overthe Naturals via Translations. Journal of Automated Reasoning. doi:10.1007/s10817-020-09541-4

    DOI: 10.1007/s10817-020-09541-4

    sf Kn : Architecture, Refinements, Strategies and Experiments. (Journal article)

    Nalon, C., Hustadt, U., & Dixon, C. (2020). sf Kn : Architecture, Refinements, Strategies and Experiments.. J. Autom. Reason., 64, 461-484.

    2019

    Modal Resolution: Proofs, Layers, and Refinements. (Journal article)

    Nalon, C., Dixon, C., & Hustadt, U. (2019). Modal Resolution: Proofs, Layers, and Refinements.. ACM Trans. Comput. Log., 20, 23:1.

    Modal Resolution: Proofs, Layers and Refinements (Journal article)

    Nalon, C., Dixon, C., & Hustadt, U. (2019). Modal Resolution: Proofs, Layers and Refinements. ACM Transactions on Computational Logic, 20(4). doi:10.1145/3331448

    DOI: 10.1145/3331448

    2018

    The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators (Journal article)

    Gainer, P., Linker, S., Dixon, C., Hustadt, U., & Fisher, M. (2018). The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators. Quantitative Evaluation of Systems. Retrieved from http://arxiv.org/abs/1709.04385v3

    Evaluating pre-processing techniques for the separated normal form for temporal logics (Conference Paper)

    Hustadt, U., Nalon, C., & Dixon, C. (2018). Evaluating pre-processing techniques for the separated normal form for temporal logics. In CEUR Workshop Proceedings Vol. 2162 (pp. 34-48).

    Multi-Scale Verification of Distributed Synchronisation (Journal article)

    Gainer, P., Linker, S., Dixon, C., Hustadt, U., & Fisher, M. (n.d.). Multi-Scale Verification of Distributed Synchronisation. Retrieved from http://arxiv.org/abs/1809.10655v1

    The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators. (Conference Paper)

    Gainer, P., Linker, S., Dixon, C., Hustadt, U., & Fisher, M. (2018). The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators.. In J. Sun, & M. Sun (Eds.), ICFEM Vol. 11232 (pp. 160-176). Springer. Retrieved from https://doi.org/10.1007/978-3-030-02450-5

    2017

    CRutoN: Automatic Verification of a Robotic Assistant's Behaviours (Conference Paper)

    Gainer, P., Dixon, C. L., Dautenhahn, K., Fisher, M., Hustadt, U., Saunders, J., & Webster, M. (2017). CRutoN: Automatic Verification of a Robotic Assistant's Behaviours. In Lecture Notes in Computer Science Vol. 10471 (pp. 119-133). Torino, Italy: Springer Nature. Retrieved from https://link.springer.com/chapter/10.1007/978-3-319-67113-0_8

    KSP: A resolution-based prover for multimodal K abridged report (Conference Paper)

    Nalon, C., Hustadt, U., & Dixon, C. (2017). KSP: A resolution-based prover for multimodal K abridged report. In IJCAI International Joint Conference on Artificial Intelligence (pp. 4919-4923).

    Theorem Proving for Metric Temporal Logic over the Naturals (Conference Paper)

    Hustadt, U., Ozaki, A., & Dixon, C. (2017). Theorem Proving for Metric Temporal Logic over the Naturals. In Lecture Notes in Computer Science Vol. 10395 (pp. 326-343). Springer Nature. doi:10.1007/978-3-319-63046-5_20

    DOI: 10.1007/978-3-319-63046-5_20

    Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking (Conference Paper)

    Gainer, P., Linker, S., Dixon, C., Hustadt, U., & Fisher, M. (2017). Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking. In Unknown Conference (pp. 224-239). Springer International Publishing. doi:10.1007/978-3-319-66335-7_14

    DOI: 10.1007/978-3-319-66335-7_14

    KSP: A Resolution-based Prover for Multimodal K, Abridged Report. (Conference Paper)

    Nalon, C., Hustadt, U., & Dixon, C. (2017). KSP: A Resolution-based Prover for Multimodal K, Abridged Report.. In C. Sierra (Ed.), IJCAI (pp. 4919-4923). ijcai.org. Retrieved from http://www.ijcai.org/Proceedings/2017/

    2016

    Probabilistic Model Checking of Ant-Based Positionless Swarming (Conference Paper)

    Gainer, P., Dixon, C., & Hustadt, U. (2016). Probabilistic Model Checking of Ant-Based Positionless Swarming. In Lecture Notes in Computer Science. Sheffield: Springer Verlag (Germany).

    : A Resolution-Based Prover for Multimodal K. (Conference Paper)

    Nalon, C., Hustadt, U., & Dixon, C. (2016). : A Resolution-Based Prover for Multimodal K.. In N. Olivetti, & A. Tiwari (Eds.), IJCAR Vol. 9706 (pp. 406-415). Springer. Retrieved from https://doi.org/10.1007/978-3-319-40229-1

    KSP: A Resolution-Based Prover for Multimodal K (Conference Paper)

    Nalon, C., Hustadt, U., & Dixon, C. (2016). KSP: A Resolution-Based Prover for Multimodal K. In AUTOMATED REASONING (IJCAR 2016) Vol. 9706 (pp. 406-415). doi:10.1007/978-3-319-40229-1_28

    DOI: 10.1007/978-3-319-40229-1_28

    2015

    A Modal-Layered Resolution Calculus for K (Conference Paper)

    Nalon, C., Hustadt, U., & Dixon, C. (2015). A Modal-Layered Resolution Calculus for K. In AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS (TABLEAUX 2015) Vol. 9323 (pp. 185-200). doi:10.1007/978-3-319-24312-2_13

    DOI: 10.1007/978-3-319-24312-2_13

    Ordered Resolution for Coalition Logic (Conference Paper)

    Hustadt, U., Gainer, P., Dixon, C., Nalon, C., & Zhang, L. (2015). Ordered Resolution for Coalition Logic. In AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS (TABLEAUX 2015) Vol. 9323 (pp. 169-184). doi:10.1007/978-3-319-24312-2_12

    DOI: 10.1007/978-3-319-24312-2_12

    2014

    A resolution-based calculus for Coalition Logic (Journal article)

    Nalon, C., Zhang, L., Dixon, C., & Hustadt, U. (2014). A resolution-based calculus for Coalition Logic. Journal of Logic and Computation, 24(4), 883-917. doi:10.1093/logcom/ext074

    DOI: 10.1093/logcom/ext074

    A Resolution Calculus for the Branching-Time Temporal Logic CTL (Journal article)

    Zhang, L., Hustadt, U., & Dixon, C. (2014). A Resolution Calculus for the Branching-Time Temporal Logic CTL. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 15(1). doi:10.1145/2529993

    DOI: 10.1145/2529993

    A Resolution Prover for Coalition Logic (Conference Paper)

    Nalon, C., Zhang, L., Dixon, C., & Hustadt, U. (n.d.). A Resolution Prover for Coalition Logic. In EPTCS 146, 2014, pp. 65-73. doi:10.4204/EPTCS.146.9

    DOI: 10.4204/EPTCS.146.9

    2013

    First-Order Resolution Methods for Modal Logics (Chapter)

    Schmidt, R. A., & Hustadt, U. (2013). First-Order Resolution Methods for Modal Logics. In Programming Logics (pp. 345-391). Springer Berlin Heidelberg. doi:10.1007/978-3-642-37651-1_15

    DOI: 10.1007/978-3-642-37651-1_15

    2010

    CTL-RP: A computation tree logic resolution prover (Journal article)

    Zhang, L., Hustadt, U., & Dixon, C. (2010). CTL-RP: A computation tree logic resolution prover. AI COMMUNICATIONS, 23(2-3), 111-136. doi:10.3233/AIC-2010-0463

    DOI: 10.3233/AIC-2010-0463

    Implementing a fair monodic temporal logic prover (Journal article)

    Ludwig, M., & Hustadt, U. (2010). Implementing a fair monodic temporal logic prover. AI Communications, 23(2-3), 69-96. doi:10.3233/aic-2010-0457

    DOI: 10.3233/aic-2010-0457

    A Comparison of Solvers for Propositional Dynamic Logic (Conference Paper)

    Hustadt, U., & Schmidt, R. A. (2010). A Comparison of Solvers for Propositional Dynamic Logic. In B. Konev, R. A. Schmidt, & S. Schulz (Eds.), PAAR (pp. 1-10). Liverpool, UK: Department of Computer Science, University of Liverpool.

    2009

    Redundancy elimination in monodic temporal reasoning (Conference Paper)

    Ludwig, M., & Hustadt, U. (2009). Redundancy elimination in monodic temporal reasoning. In CEUR Workshop Proceedings Vol. 556 (pp. 34-48).

    Resolution-Based Model Construction for PLTL (Conference Paper)

    Ludwig, M., & Hustadt, U. (2009). Resolution-Based Model Construction for PLTL. In TIME 2009: 16TH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS (pp. 73-80). doi:10.1109/TIME.2009.11

    DOI: 10.1109/TIME.2009.11

    Preface (Book)

    Ranise, S., & Hustadt, U. (2009). Preface (Vol. 55). doi:10.1007/s10472-009-9149-2

    DOI: 10.1007/s10472-009-9149-2

    A Refined Resolution Calculus for CTL (Conference Paper)

    Zhang, L., Hustadt, U., & Dixon, C. (2009). A Refined Resolution Calculus for CTL. In AUTOMATED DEDUCTION - CADE-22 Vol. 5663 (pp. 245-260). Retrieved from http://gateway.webofknowledge.com/

    Fair Derivations in Monodic Temporal Reasoning (Conference Paper)

    Ludwig, M., & Hustadt, U. (2009). Fair Derivations in Monodic Temporal Reasoning. In AUTOMATED DEDUCTION - CADE-22 Vol. 5663 (pp. 261-276). Retrieved from http://gateway.webofknowledge.com/

    Implementing a Fair Monodic Temporal Logic Prover (Journal article)

    Ludwig, M., & Hustadt, U. (2009). Implementing a Fair Monodic Temporal Logic Prover. AI Communications, 30.

    2008

    Deciding expressive description logics in the framework of resolution (Journal article)

    Hustadt, U., Motik, B., & Sattler, U. (2008). Deciding expressive description logics in the framework of resolution. INFORMATION AND COMPUTATION, 206(5), 579-601. doi:10.1016/j.ic.2007.11.006

    DOI: 10.1016/j.ic.2007.11.006

    2007

    4 Computational modal logic (Journal article)

    Horrocks, I., Hustadt, U., Sattler, U., & Schmidt, R. (2007). 4 Computational modal logic. Unknown Journal, 181-245. doi:10.1016/s1570-2464(07)80007-3

    DOI: 10.1016/s1570-2464(07)80007-3

    Reasoning in description logics by a reduction to disjunctive datalog (Journal article)

    Hustadt, U., Motik, B., & Sattler, U. (2007). Reasoning in description logics by a reduction to disjunctive datalog. JOURNAL OF AUTOMATED REASONING, 39(3), 351-384. doi:10.1007/s10817-007-9080-3

    DOI: 10.1007/s10817-007-9080-3

    The axiomatic translation principle for modal logic (Journal article)

    Schmidt, R. A., & Hustadt, U. (2007). The axiomatic translation principle for modal logic. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 8(4). doi:10.1145/1276920.1276921

    DOI: 10.1145/1276920.1276921

    Computational Modal Logic (Chapter)

    Horrocks, I., Hustadt, U., Sattler, U., & Schmidt, R. A. (2007). Computational Modal Logic. In P. Blackburn, J. van Benthem, F. Wolter, D. M. Gabbay, P. Gaerdenfors, J. Siekmann, . . . J. Woods (Eds.), Handbook of Modal Logic (pp. 181-245). Elsevier.

    2006

    Automated reasoning about metric and topology (Conference Paper)

    Hustadt, U., Tishkovsky, D., Wolter, F., & Zakharyaschev, M. (2006). Automated reasoning about metric and topology. In LOGICS IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS Vol. 4160 (pp. 490-493). doi:10.1007/11853886_44

    DOI: 10.1007/11853886_44

    Verification Within the KARO Agent Theory (Chapter)

    Hustadt, U., Dixon, C., Schmidt, R. A., Fisher, M., Meyer, J. -J. C., & van der Hoek, W. (2006). Verification Within the KARO Agent Theory. In NASA Monographs in Systems and Software Engineering (pp. 193-225). Springer London. doi:10.1007/1-84628-271-3_7

    DOI: 10.1007/1-84628-271-3_7

    2005

    Data complexity of reasoning in very expressive description logics (Conference Paper)

    Hustadt, U., Motik, B., & Sattler, U. (2005). Data complexity of reasoning in very expressive description logics. In IJCAI International Joint Conference on Artificial Intelligence (pp. 466-471).

    Description logics and disjunctive datalog : The story so far (Conference Paper)

    Hustadt, U., & Motik, B. (2005). Description logics and disjunctive datalog : The story so far. In CEUR Workshop Proceedings Vol. 147.

    Mechanising first-order temporal resolution (Journal article)

    Konev, B., Degtyarev, A., Dixon, C., Fisher, M., & Hustadt, U. (2005). Mechanising first-order temporal resolution. INFORMATION AND COMPUTATION, 199(1-2), 55-86. doi:10.1016/j.ic.2004.10.005

    DOI: 10.1016/j.ic.2004.10.005

    First-order temporal verification in practice (Journal article)

    Fernandez-Gago, M. C., Hustadt, U., Dixon, C., Fisher, M., & Konev, B. (2005). First-order temporal verification in practice. JOURNAL OF AUTOMATED REASONING, 34(3), 295-321. doi:10.1007/s10817-005-7354-1

    DOI: 10.1007/s10817-005-7354-1

    A decomposition rule for decision procedures by resolution-based calculi (Conference Paper)

    Hustadt, U., Motik, B., & Sattler, U. (2005). A decomposition rule for decision procedures by resolution-based calculi. In LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS Vol. 3452 (pp. 21-35). Retrieved from http://gateway.webofknowledge.com/

    Deciding Monodic Fragments by Temporal Resolution (Conference Paper)

    Hustadt, U., Konev, B., & Schmidt, R. A. (2005). Deciding Monodic Fragments by Temporal Resolution. In Unknown Conference (pp. 204-218). Springer Berlin Heidelberg. doi:10.1007/11532231_15

    DOI: 10.1007/11532231_15

    Deciding monodic fragments by temporal resolution (Conference Paper)

    Hustadt, U., Konev, B., & Schmidt, R. A. (2005). Deciding monodic fragments by temporal resolution. In AUTOMATED DEDUCTION - CADE-20, PROCEEDINGS Vol. 3632 (pp. 204-218). Retrieved from http://gateway.webofknowledge.com/

    2004

    Interactions between Knowledge, Action and Commitment within Agent Dynamic Logic (Journal article)

    Schmidt, R. A., Tishkovsky, D., & Hustadt, U. (2004). Interactions between Knowledge, Action and Commitment within Agent Dynamic Logic. Studia Logica, 78(3), 381-415. doi:10.1007/s11225-004-6042-1

    DOI: 10.1007/s11225-004-6042-1

    Mechanised reasoning and model generation for extended modal logics (Journal article)

    Schmidt, R. A., & Hustadt, U. (2003). Mechanised reasoning and model generation for extended modal logics. THEORY AND APPLICATIONS OF RELATIONAL STRUCTURES AS KNOWLEDGE INSTRUMENTS, 2929, 38-67. Retrieved from http://gateway.webofknowledge.com/

    Reasoning in Description Logics with a Concrete Domain in the Framework of Resolution (Conference Paper)

    Hustadt, U., Motik, B., & Sattler, U. (2004). Reasoning in Description Logics with a Concrete Domain in the Framework of Resolution. In R. Lopez de Mantaras, & L. Saitta (Eds.), 16th European Conference on Artificial Intelligenc Vol. 110 (pp. 353-357). Valencia, Spain: IOS Press.

    Reasoning in description logics with a concrete domain in the framework of resolution (Conference Paper)

    Hustadt, U., Motik, B., & Sattler, U. (2004). Reasoning in description logics with a concrete domain in the framework of resolution. In Frontiers in Artificial Intelligence and Applications Vol. 110 (pp. 348-352).

    Reducing SHIQ- Description Logic to Disjunctive Datalog Programs (Conference Paper)

    Hustadt, U., Motik, B., & Sattler, U. (2004). Reducing SHIQ- Description Logic to Disjunctive Datalog Programs. In D. Dubois, C. Welty, & M. -A. Williams (Eds.), 9th International Conference on Knowledge Representation and Reasoning (pp. 152-162). Whistler, Canada: AAAI Press.

    SCAN Is Complete for All Sahlqvist Formulae (Journal article)

    Goranko, V., Hustadt, U., Schmidt, R. A., & Vakarelov, D. (2004). SCAN Is Complete for All Sahlqvist Formulae. Unknown Journal, 149-162. doi:10.1007/978-3-540-24771-5_13

    DOI: 10.1007/978-3-540-24771-5_13

    TeMP: A temporal monodic prover (Conference Paper)

    Hustadt, U., Konev, B., Riazanov, A., & Voronkov, A. (2004). TeMP: A temporal monodic prover. In AUTOMATED REASONING, PROCEEDINGS Vol. 3097 (pp. 326-330). Retrieved from http://gateway.webofknowledge.com/

    Two proof systems for Peirce algebras (Journal article)

    Schmidt, R. A., Orlowska, E., & Hustadt, U. (2003). Two proof systems for Peirce algebras. RELATIONAL AND KLEENE-ALGEBRAIC METHODS IN COMPUTER SCIENCE, 3051, 238-251. Retrieved from http://gateway.webofknowledge.com/

    2003

    A principle for incorporating axioms into the first-order translation of modal formulae (Conference Paper)

    Schmidt, R. A., & Hustadt, U. (2003). A principle for incorporating axioms into the first-order translation of modal formulae. In AUTOMATED DEDUCTION - CADE-19, PROCEEDINGS Vol. 2741 (pp. 412-426). Retrieved from http://gateway.webofknowledge.com/

    Hyperresolution for guarded formulae (Journal article)

    Georgieva, L., Hustadt, U., & Schmidt, R. A. (2003). Hyperresolution for guarded formulae. Journal of Symbolic Computation, 36(1-2), 163-192. doi:10.1016/s0747-7171(03)00034-8

    DOI: 10.1016/s0747-7171(03)00034-8

    Hyperresolution for guarded formulae (Journal article)

    Georgieva, L., Hustadt, U., & Schmidt, R. A. (2003). Hyperresolution for guarded formulae. JOURNAL OF SYMBOLIC COMPUTATION, 36(1-2), 163-192. doi:10.1016/S0747-7171(03)00034-8

    DOI: 10.1016/S0747-7171(03)00034-8

    TRP++2.0: A temporal resolution prover (Conference Paper)

    Hustadt, U., & Konev, B. (2003). TRP++2.0: A temporal resolution prover. In AUTOMATED DEDUCTION - CADE-19, PROCEEDINGS Vol. 2741 (pp. 274-278). Retrieved from http://gateway.webofknowledge.com/

    Towards the implementation of first-order temporal resolution: the expanding domain case (Conference Paper)

    Konev, B., Degtyarev, A., Dixon, C., Fisher, M., & Hustadt, U. (2003). Towards the implementation of first-order temporal resolution: the expanding domain case. In TIME-ICTL 2003: 10TH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING AND FOURTH INTERNATIONAL CONFERENCE ON TEMPORAL LOGIC, PROCEEDINGS (pp. 72-82). Retrieved from http://gateway.webofknowledge.com/

    2002

    (Journal article)

    Hustadt, U., & Schmidt, R. A. (2002). Unknown Title. Journal of Automated Reasoning, 28(2), 205-232. doi:10.1023/a:1015067300005

    DOI: 10.1023/a:1015067300005

    A New Clausal Class Decidable by Hyperresolution (Conference Paper)

    Georgieva, L., Hustadt, U., & Schmidt, R. A. (2002). A New Clausal Class Decidable by Hyperresolution. In Unknown Conference (pp. 260-274). Springer Berlin Heidelberg. doi:10.1007/3-540-45620-1_21

    DOI: 10.1007/3-540-45620-1_21

    Combinations of modal logics (Journal article)

    Bennett, B., Dixon, C., Fisher, M., Hustadt, U., Franconi, E., Horrocks, I., & De Rijke, M. (2002). Combinations of modal logics. ARTIFICIAL INTELLIGENCE REVIEW, 17(1), 1-20. doi:10.1023/A:1015057926707

    DOI: 10.1023/A:1015057926707

    Scientific benchmarking with temporal logic decision procedures (Conference Paper)

    Hustadt, U., & Schmidt, R. A. (2002). Scientific benchmarking with temporal logic decision procedures. In D. Fensel, F. Giunchiglia, D. McGuinness, & M. -A. Williams (Eds.), Eighth International Conference on Principles of Knowledge Representation and Reasoning (pp. 533-544). Toulouse, France: Morgan Kaufmann.

    2001

    Reasoning about agents in the KARO framework (Conference Paper)

    Hustadt, U., Dixon, C., Schmidt, R. A., Fisher, M., Meyer, J. J., van der Hoek, W., . . . SOCIETY, I. C. (2001). Reasoning about agents in the KARO framework. In EIGHTH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS (pp. 206-213). doi:10.1109/TIME.2001.930719

    DOI: 10.1109/TIME.2001.930719

    Multi-agent systems research into the 21st century (Conference Paper)

    D'Inverno, M., Luck, M., & Contributors, U. K. M. A. S. . (2001). Multi-agent systems research into the 21st century. In KNOWLEDGE ENGINEERING REVIEW Vol. 16 (pp. 271-275). doi:10.1017/S0269888901000169

    DOI: 10.1017/S0269888901000169

    Computational Space Efficiency and Minimal Model Generation for Guarded Formulae (Conference Paper)

    Georgieva, L., Hustadt, U., & Schmidt, R. A. (2001). Computational Space Efficiency and Minimal Model Generation for Guarded Formulae. In Unknown Conference (pp. 85-99). Springer Berlin Heidelberg. doi:10.1007/3-540-45653-8_6

    DOI: 10.1007/3-540-45653-8_6

    Resolution Decision Procedures (Chapter)

    Fermüller, C. G., Leitsch, A., Hustadt, U., & Tammet, T. (2001). Resolution Decision Procedures. In Handbook of Automated Reasoning (pp. 1791-1849). Elsevier. doi:10.1016/b978-044450813-3/50027-8

    DOI: 10.1016/b978-044450813-3/50027-8

    Verification within the KARO Agent Theory (Conference Paper)

    Hustadt, U., Dixon, C., Schmidt, R. A., Fisher, M., Meyer, J. -J., & van der Hoek, W. (2001). Verification within the KARO Agent Theory. In Unknown Conference (pp. 33-47). Springer Berlin Heidelberg. doi:10.1007/3-540-45484-5_3

    DOI: 10.1007/3-540-45484-5_3

    2000

    MSPASS: Modal reasoning by translation and first-order resolution (Conference Paper)

    Hustadt, U., & Schmidt, R. A. (2000). MSPASS: Modal reasoning by translation and first-order resolution. In AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS Vol. 1847 (pp. 67-71). Retrieved from http://gateway.webofknowledge.com/

    A resolution decision procedure for fluted logic (Conference Paper)

    Schmidt, R. A., & Hustadt, U. (2000). A resolution decision procedure for fluted logic. In AUTOMATED DEDUCTION - CADE-17 Vol. 1831 (pp. 433-448). Retrieved from http://gateway.webofknowledge.com/

    Issues of decidability for description logics in the framework of resolution (Conference Paper)

    Hustadt, U., & Schmidt, R. A. (2000). Issues of decidability for description logics in the framework of resolution. In AUTOMATED DEDUCTION IN CLASSICAL AND NON-CLASSICAL LOGICS Vol. 1761 (pp. 191-205). Retrieved from http://gateway.webofknowledge.com/

    Normal forms and proofs in combined modal and temporal logics (Conference Paper)

    Hustadt, U., Dixon, C., Schmidt, R. A., & Fisher, M. (2000). Normal forms and proofs in combined modal and temporal logics. In FRONTIERS OF COMBINING SYSTEMS Vol. 1794 (pp. 73-87). Retrieved from http://gateway.webofknowledge.com/

    1999

    An empirical analysis of modal theorem provers (Journal article)

    Hustadt, U., & Schmidt, R. A. (1999). An empirical analysis of modal theorem provers. Journal of Applied Non-Classical Logics, 9(4), 479-522. doi:10.1080/11663081.1999.10510981

    DOI: 10.1080/11663081.1999.10510981

    On the relation of resolution and tableaux proof systems for description logics (Conference Paper)

    Hustadt, U., & Schmidt, R. A. (1999). On the relation of resolution and tableaux proof systems for description logics. In IJCAI International Joint Conference on Artificial Intelligence Vol. 1 (pp. 110-115).

    Maslov’s Class K Revisited (Conference Paper)

    Hustadt, U., & Schmidt, R. A. (1999). Maslov’s Class K Revisited. In Unknown Conference (pp. 172-186). Springer Berlin Heidelberg. doi:10.1007/3-540-48660-7_12

    DOI: 10.1007/3-540-48660-7_12

    1998

    Optimised functional translation and resolution (Conference Paper)

    Hustadt, U., Schmidt, R. A., & Weidenbach, C. (1998). Optimised functional translation and resolution. In AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS Vol. 1397 (pp. 36-37). Retrieved from http://gateway.webofknowledge.com/

    Simplification and backjumping in modal tableau (Conference Paper)

    Hustadt, U., & Schmidt, R. A. (1998). Simplification and backjumping in modal tableau. In AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS Vol. 1397 (pp. 187-201). Retrieved from http://gateway.webofknowledge.com/

    1997

    On evaluating decision procedures for modal logic (Conference Paper)

    Hustadt, U., & Schmidt, R. A. (1997). On evaluating decision procedures for modal logic. In IJCAI International Joint Conference on Artificial Intelligence Vol. 1 (pp. 202-207).

    1996

    Translating graded modalities into predicate logics (Conference Paper)

    Ohlbach, H. J., Schmidt, R., & Hustadt, U. (1996). Translating graded modalities into predicate logics. In PROOF THEORY OF MODAL LOGIC Vol. 2 (pp. 253-291). Retrieved from http://gateway.webofknowledge.com/