Publications

Filter publications

What type of publication do you want to show?

All

Journals

Conference papers

Chapters

Books

Other

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

DOI: 10.1007/978-3-031-63501-4_1
: Chapter

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

DOI: 10.1007/978-3-031-38499-8_22
: Chapter

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

DOI: 10.1007/s10817-022-09630-6
: Journal article

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

DOI: 10.1007/s10817-022-09633-3
: Journal article

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

DOI: 10.1007/978-3-031-10769-6_29
: Conference Paper

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

: Chapter

2020

Multi-Scale Verification of Distributed Synchronisation

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
: Journal article

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

DOI: 10.1007/s10817-018-09503-x
: Journal article

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

DOI: 10.1007/s10817-018-09503-x
: Journal article

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

DOI: 10.1007/s10817-020-09541-4
: Journal article

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

: Journal article

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.

: Journal article

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

DOI: 10.1145/3331448
: Journal article

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

: Journal article

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

: Conference Paper

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

: Journal article

Multi-Scale Verification of Distributed Synchronisation

DOI: 10.48550/arxiv.1809.10655
: Preprint

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).

: Conference Paper

2017

The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators

DOI: 10.48550/arxiv.1709.04385
: Preprint

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

: Conference Paper

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).

: Conference Paper

KSP: A Resolution-based Prover for Multimodal K Abridged Report

Nalon, C., Hustadt, U., & Dixon, C. (2017). KSP: 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/

: Conference Paper

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

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

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

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

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).

: Conference Paper

: 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

: Conference Paper

KSP: A Resolution-Based Prover for Multimodal K

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
: Conference Paper

Preface

Larsen, K. G., Potapov, I., & Srba, J. (2016). Preface (Vol. 9899 LNCS).

: Book

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

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

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

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

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

DOI: 10.1093/logcom/ext074
: Journal article

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

: Conference Paper

A Resolution Prover for Coalition Logic

DOI: 10.48550/arxiv.1404.0841
: Preprint

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

DOI: 10.1145/2529993
: Journal article

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

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

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

DOI: 10.3233/AIC-2010-0463
: Journal article

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

DOI: 10.3233/aic-2010-0457
: Journal article

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.

: Conference Paper

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).

: Conference Paper

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

DOI: 10.1109/TIME.2009.11
: Conference Paper

Preface

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

DOI: 10.1007/s10472-009-9149-2
: Book

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/

: Conference Paper

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/

: Conference Paper

Implementing a Fair Monodic Temporal Logic Prover

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

: Journal article

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

DOI: 10.1016/j.ic.2007.11.006
: Journal article

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

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

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

DOI: 10.1007/s10817-007-9080-3
: Journal article

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

DOI: 10.1145/1276920.1276921
: Journal article

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/

: Chapter

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

DOI: 10.1007/11853886_44
: Conference Paper

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

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

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).

: Conference Paper

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.

: Conference Paper

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

DOI: 10.1016/j.ic.2004.10.005
: Journal article

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

DOI: 10.1007/s10817-005-7354-1
: Journal article

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/

: Conference Paper

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

DOI: 10.1007/11532231_15
: Conference Paper

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/

: Conference Paper

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

DOI: 10.1007/s11225-004-6042-1
: Journal article

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/

: Journal article

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.

: Conference Paper

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).

: Conference Paper

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).

: Conference Paper

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

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

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/

: Conference Paper

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/

: Journal article

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/

: Conference Paper

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

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

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

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

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/

: Conference Paper

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/

: Conference Paper

2002

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
: Journal article

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

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

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

DOI: 10.1023/A:1015057926707
: Journal article

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.

: Conference Paper

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

DOI: 10.1109/TIME.2001.930719
: Conference Paper

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

DOI: 10.1017/S0269888901000169
: Conference Paper

Hustadt, U. (2001). Unknown Title. Journal of Logic, Language and Information, 10(3), 406-410. doi:10.1023/a:1011212908144

DOI: 10.1023/a:1011212908144
: Journal article

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

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

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

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

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

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

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

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

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/

: Conference Paper

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

DOI: 10.1093/jigpal/8.3.265
: Journal article

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/

: Conference Paper

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/

: Conference Paper

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/

: Conference Paper

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

DOI: 10.1080/11663081.1999.10510981
: Journal article

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).

: Conference Paper

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

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

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/

: Conference Paper

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/

: Conference Paper

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).

: Conference Paper

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/

: Conference Paper

Publications

2024

Model Construction for Modal Clauses

2023

Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic

2022

2021

2020

Multi-Scale Verification of Distributed Synchronisation

A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments

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

2019

2018

The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators.

Multi-Scale Verification of Distributed Synchronisation

2017

The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators

2016

Probabilistic Model Checking of Ant-Based Positionless Swarming

: A Resolution-Based Prover for Multimodal K.

Preface

2015

A Modal-Layered Resolution Calculus for K

Ordered Resolution for Coalition Logic

2014

A Resolution Prover for Coalition Logic

2013

First-Order Resolution Methods for Modal Logics

2010

CTL-RP: A computation tree logic resolution prover

Implementing a fair monodic temporal logic prover

A Comparison of Solvers for Propositional Dynamic Logic

2009

Redundancy elimination in monodic temporal reasoning

Resolution-Based Model Construction for PLTL

Preface

A Refined Resolution Calculus for CTL

Fair Derivations in Monodic Temporal Reasoning

Implementing a Fair Monodic Temporal Logic Prover

2008

Deciding expressive description logics in the framework of resolution

2007

4 Computational modal logic

Reasoning in description logics by a reduction to disjunctive datalog

The axiomatic translation principle for modal logic

COMPUTATIONAL MODAL LOGIC

2006

Automated reasoning about metric and topology

Verification Within the KARO Agent Theory

2005

Data complexity of reasoning in very expressive description logics

Description logics and disjunctive datalog : The story so far

Mechanising first-order temporal resolution

First-order temporal verification in practice

A decomposition rule for decision procedures by resolution-based calculi

Deciding Monodic Fragments by Temporal Resolution

Deciding monodic fragments by temporal resolution

2004

Interactions between Knowledge, Action and Commitment within Agent Dynamic Logic

Mechanised reasoning and model generation for extended modal logics

Reasoning in Description Logics with a Concrete Domain in the Framework of Resolution

Reasoning in description logics with a concrete domain in the framework of resolution

Reducing SHIQ<sup>−</sup> Description Logic to Disjunctive Datalog Programs

SCAN Is Complete for All Sahlqvist Formulae

TeMP: A temporal monodic prover

Two proof systems for Peirce algebras

2003

A principle for incorporating axioms into the first-order translation of modal formulae

Hyperresolution for guarded formulae

Hyperresolution for guarded formulae

TRP++2.0: A temporal resolution prover

Towards the implementation of first-order temporal resolution: the expanding domain case

2002

A New Clausal Class Decidable by Hyperresolution

Combinations of modal logics

Scientific benchmarking with temporal logic decision procedures

2001

Reasoning about agents in the KARO framework

Multi-agent systems research into the 21st century

Chapter 25 Resolution Decision Procedures