Research outputs
2024
Model Construction for Modal Clauses
Hustadt, U., Papacchini, F., Nalon, C., & Dixon, C. (2024). Model Construction for Modal Clauses. In Lecture Notes in Computer Science (pp. 3-23). Springer Nature Switzerland. doi:10.1007/978-3-031-63501-4_1
2023
Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
Nalon, C., Hustadt, U., Papacchini, F., & Dixon, C. (2023). Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic. In Lecture Notes in Computer Science (pp. 382-400). Springer Nature Switzerland. doi:10.1007/978-3-031-38499-8_22
2022
Local is Best: Efficient Reductions to Modal Logic K
Papacchini, F., Nalon, C., Hustadt, U., & Dixon, C. (2022). Local is Best: Efficient Reductions to Modal Logic K. JOURNAL OF AUTOMATED REASONING, 66(4), 639-666. doi:10.1007/s10817-022-09630-6
Local is Best: Efficient Reductions to Modal Logic K (Sep, 2022, 10.1007/s10817-022-09630-6)
Papacchini, F., Nalon, C., Hustadt, U., & Dixon, C. (2022). Local is Best: Efficient Reductions to Modal Logic K (Sep, 2022, 10.1007/s10817-022-09630-6). JOURNAL OF AUTOMATED REASONING, 66(4), 1099. doi:10.1007/s10817-022-09633-3
Local Reductions for the Modal Cube
Nalon, C., Hustadt, U., Papacchini, F., & Dixon, C. (2022). Local Reductions for the Modal Cube. In AUTOMATED REASONING, IJCAR 2022 Vol. 13385 (pp. 486-505). doi:10.1007/978-3-031-10769-6_29
2021
Efficient Local Reductions to Basic Modal Logic.
Papacchini, F., Nalon, C., Hustadt, U., & Dixon, C. (2021). Efficient Local Reductions to Basic Modal Logic. In Unknown Book (Vol. 12699, pp. 76-92). doi:10.1007/978-3-030-79876-5_5
2020
Multi-Scale Verification of Distributed Synchronisation
Gainer, P., Linker, S., Dixon, C., Hustadt, U., & Fisher, M. (2020). Multi-Scale Verification of Distributed Synchronisation. Formal Methods in System Design. doi:10.1007/s10703-020-00347-z
A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments
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
KSP A Resolution-Based Theorem Prover for K_n : Architecture, Refinements, Strategies and Experiments
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
Theorem Proving for Pointwise Metric Temporal Logic Overthe Naturals via Translations
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
sf Kn : Architecture, Refinements, Strategies and Experiments.
Nalon, C., Hustadt, U., & Dixon, C. (2020). sf Kn : Architecture, Refinements, Strategies and Experiments.. J. Autom. Reason., 64, 461-484. doi:10.1007/s10817-018-09503-x
2019
Modal Resolution: Proofs, Layers, and Refinements.
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
Nalon, C., Dixon, C., & Hustadt, U. (2019). Modal Resolution: Proofs, Layers and Refinements. ACM Transactions on Computational Logic, 20(4). doi:10.1145/3331448
2018
The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators
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
The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators.
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
Multi-Scale Verification of Distributed Synchronisation
Gainer, P., Linker, S., Dixon, C., Hustadt, U., & Fisher, M. (2018). Multi-Scale Verification of Distributed Synchronisation. Retrieved from http://arxiv.org/abs/1809.10655v1
Multi-Scale Verification of Distributed Synchronisation
Evaluating pre-processing techniques for the separated normal form for temporal logics
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).
2017
The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators
CRutoN: Automatic Verification of a Robotic Assistant's Behaviours
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
K<inf>S</inf>P: A resolution-based prover for multimodal K abridged report
Nalon, C., Hustadt, U., & Dixon, C. (2017). K<inf>S</inf>P: A resolution-based prover for multimodal K abridged report. In IJCAI International Joint Conference on Artificial Intelligence (pp. 4919-4923).
K<sub>S</sub>P: A Resolution-based Prover for Multimodal K Abridged Report
Nalon, C., Hustadt, U., & Dixon, C. (2017). K<sub>S</sub>P: A Resolution-based Prover for Multimodal K Abridged Report. In PROCEEDINGS OF THE TWENTY-SIXTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (pp. 4919-4923). Retrieved from https://www.webofscience.com/
Theorem Proving for Metric Temporal Logic over the Naturals
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
Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking
Gainer, P., Linker, S., Dixon, C., Hustadt, U., & Fisher, M. (2017). Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking. In QUANTITATIVE EVALUATION OF SYSTEMS (QEST 2017) Vol. 10503 (pp. 224-239). doi:10.1007/978-3-319-66335-7_14
2016
Probabilistic Model Checking of Ant-Based Positionless Swarming
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.
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
K<sub>S</sub>P: A Resolution-Based Prover for Multimodal K
Nalon, C., Hustadt, U., & Dixon, C. (2016). K<sub>S</sub>P: 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
Preface
Larsen, K. G., Potapov, I., & Srba, J. (2016). Preface (Vol. 9899 LNCS).
2015
A Modal-Layered Resolution Calculus for K
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
Ordered Resolution for Coalition Logic
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
2014
A resolution-based calculus for Coalition Logic
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
A Resolution Prover for Coalition Logic
Nalon, C., Zhang, L., Dixon, C., & Hustadt, U. (2014). A Resolution Prover for Coalition Logic. In EPTCS 146, 2014, pp. 65-73. Retrieved from http://dx.doi.org/10.4204/EPTCS.146.9
A Resolution Prover for Coalition Logic
A Resolution Calculus for the Branching-Time Temporal Logic CTL
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
2013
First-Order Resolution Methods for Modal Logics
Schmidt, R. A., & Hustadt, U. (2013). First-Order Resolution Methods for Modal Logics. In Lecture Notes in Computer Science (pp. 345-391). Springer Berlin Heidelberg. doi:10.1007/978-3-642-37651-1_15
2010
CTL-RP: A computation tree logic resolution prover
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
Implementing a fair monodic temporal logic prover
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
A Comparison of Solvers for Propositional Dynamic Logic
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
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
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
Preface
Ranise, S., & Hustadt, U. (2009). Preface (Vol. 55). doi:10.1007/s10472-009-9149-2
A Refined Resolution Calculus for CTL
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 https://www.webofscience.com/
Fair Derivations in Monodic Temporal Reasoning
Ludwig, M., & Hustadt, U. (2009). Fair Derivations in Monodic Temporal Reasoning. In AUTOMATED DEDUCTION - CADE-22 Vol. 5663 (pp. 261-276). Retrieved from https://www.webofscience.com/
Implementing a Fair Monodic Temporal Logic Prover
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
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
2007
4 Computational modal logic
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
Reasoning in description logics by a reduction to disjunctive datalog
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
The axiomatic translation principle for modal logic
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
COMPUTATIONAL MODAL LOGIC
Horrocks, I., Hustadt, U., Sattler, U., & Schmidt, R. (2007). COMPUTATIONAL MODAL LOGIC. In HANDBOOK OF MODAL LOGIC (Vol. 3, pp. 181-245). Retrieved from https://www.webofscience.com/
2006
Automated reasoning about metric and topology
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
Verification Within the KARO Agent Theory
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
2005
Data complexity of reasoning in very expressive description logics
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
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
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
First-order temporal verification in practice
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
A decomposition rule for decision procedures by resolution-based calculi
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 https://www.webofscience.com/
Deciding Monodic Fragments by Temporal Resolution
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
Deciding monodic fragments by temporal resolution
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 https://www.webofscience.com/
2004
Interactions between Knowledge, Action and Commitment within Agent Dynamic Logic
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
Mechanised reasoning and model generation for extended modal logics
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 https://www.webofscience.com/
Reasoning in Description Logics with a Concrete Domain in the Framework of Resolution
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
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
Hustadt, U., Motik, B., & Sattler, U. (2004). Reducing SHIQ− Description Logic to Disjunctive Datalog Programs. In Principles of Knowledge Representation and Reasoning Proceedings of the 9th International Conference Kr 2004 (pp. 152-162).
SCAN Is Complete for All Sahlqvist Formulae
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
TeMP: A temporal monodic prover
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 https://www.webofscience.com/
Two proof systems for Peirce algebras
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 https://www.webofscience.com/
2003
A principle for incorporating axioms into the first-order translation of modal formulae
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 https://www.webofscience.com/
Hyperresolution for guarded formulae
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
Hyperresolution for guarded formulae
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
TRP++2.0: A temporal resolution prover
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 https://www.webofscience.com/
Towards the implementation of first-order temporal resolution: the expanding domain case
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 https://www.webofscience.com/
2002
Using Resolution for Testing Modal Satisfiability and Building Models
Hustadt, U., & Schmidt, R. A. (2002). Using Resolution for Testing Modal Satisfiability and Building Models. Journal of Automated Reasoning, 28(2), 205-232. doi:10.1023/a:1015067300005
A New Clausal Class Decidable by Hyperresolution
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
Combinations of modal logics
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
Scientific benchmarking with temporal logic decision procedures
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
Hustadt, U., Dixon, C., Schmidt, R. A., Fisher, M., Meyer, J. J., & van der Hoek, W. (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
Multi-agent systems research into the 21st century
D'Inverno, M., & Luck, M. (2001). Multi-agent systems research into the 21st century. In KNOWLEDGE ENGINEERING REVIEW Vol. 16 (pp. 271-275). doi:10.1017/S0269888901000169
Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 2, Dov M. Gabbay, Mark A. Reynolds, and Marcelo Finger
Hustadt, U. (2001). Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 2, Dov M. Gabbay, Mark A. Reynolds, and Marcelo Finger. Journal of Logic, Language and Information, 10(3), 406-410. doi:10.1023/a:1011212908144
Chapter 25 Resolution Decision Procedures
Fermüller, C. G., Leitsch, A., Hustadt, U., & Tammet, T. (2001). Chapter 25 Resolution Decision Procedures. In Handbook of Automated Reasoning (pp. 1791-1849). Elsevier. doi:10.1016/b978-044450813-3/50027-8
Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
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
Resolution Decision Procedures
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
Verification within the KARO Agent Theory
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
2000
MSPASS: Modal reasoning by translation and first-order resolution
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 https://www.webofscience.com/
Resolution-based methods for modal logics
de Nivelle, H. (2000). Resolution-based methods for modal logics. Logic Journal of IGPL, 8(3), 265-292. doi:10.1093/jigpal/8.3.265
A resolution decision procedure for fluted logic
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 https://www.webofscience.com/
Issues of decidability for description logics in the framework of resolution
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 https://www.webofscience.com/
Normal forms and proofs in combined modal and temporal logics
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 https://www.webofscience.com/
1999
An empirical analysis of modal theorem provers
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
On the relation of resolution and tableaux proof systems for description logics
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
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
1998
Optimised functional translation and resolution
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 https://www.webofscience.com/
Simplification and backjumping in modal tableau
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 https://www.webofscience.com/
1997
On evaluating decision procedures for modal logic
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
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 https://www.webofscience.com/