Research outputs
2024
Model Construction for Modal Clauses
Hustadt, U., Papacchini, F., Nalon, C., & Dixon, C. (2024). Model Construction for Modal Clauses. In Unknown Book (Vol. 14740, pp. 3-23). 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 Unknown Book (Vol. 14132, pp. 382-400). 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 Lecture Notes in Computer Science Vol. 11232 (pp. 160-176). Springer Nature. doi:10.1007/978-3-030-02450-5_10
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 https://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
A resolution prover for coalition logic
Nalon, C., Zhang, L., Dixon, C., & Hustadt, U. (2014). A resolution prover for coalition logic. In Electronic Proceedings in Theoretical Computer Science Eptcs Vol. 146 (pp. 65-73). doi:10.4204/EPTCS.146.9
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), 38 pages. 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 Unknown Book (Vol. 7797 LNCS, pp. 345-391). doi:10.1007/978-3-642-37651-1_15
2012
A Comparison of Solvers for Propositional Dynamic Logic
Hustadt, U., & Schmidt, R. A. (2012). A Comparison of Solvers for Propositional Dynamic Logic. In EPiC series in computing Vol. 9 (pp. 63-51). EasyChair. doi:10.29007/63hq
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. Studies in Logic and Practical Reasoning, 3, 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), 55 pages. 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 Agent Technology from a Formal Perspective (pp. 193-225). Springer Nature. 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. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 3051, 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 Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 2392 (pp. 260-274). 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 Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 2250 (pp. 85-99). 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 Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 1871 (pp. 33-47). 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., Schmidt, R., & Hustadt, U. (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 Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 1632 (pp. 172-186). 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/