| 2024 | IJCAR | Model Construction for Modal Clauses. | Ullrich Hustadt, Fabio Papacchini, Cludia Nalon, Clare Dixon |
| 2023 | CADE | Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic. | Cludia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon |
| 2022 | CADE | Local Reductions for the Modal Cube. | Cludia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon |
| 2021 | CADE | Efficient Local Reductions to Basic Modal Logic. | Fabio Papacchini, Cludia Nalon, Ullrich Hustadt, Clare Dixon |
| 2018 | CADE | Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics. | Ullrich Hustadt, Cludia Nalon, Clare Dixon |
| 2018 | ICFEM | The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators. | Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fisher |
| 2017 | CADE | Theorem Proving for Metric Temporal Logic over the Naturals. | Ullrich Hustadt, Ana Ozaki, Clare Dixon |
| 2017 | FMICS | CRutoN: Automatic Verification of a Robotic Assistant's Behaviours. | Paul Gainer, Clare Dixon, Kerstin Dautenhahn, Michael Fisher, Ullrich Hustadt, Joe Saunders, Matt Webster |
| 2017 | IJCAI | KSP: A Resolution-based Prover for Multimodal K, Abridged Report. | Cludia Nalon, Ullrich Hustadt, Clare Dixon |
| 2016 | CADE | : A Resolution-Based Prover for Multimodal K. | Cludia Nalon, Ullrich Hustadt, Clare Dixon |
| 2015 | TABLEAUX | Ordered Resolution for Coalition Logic. | Ullrich Hustadt, Paul Gainer, Clare Dixon, Cludia Nalon, Lan Zhang |
| 2015 | TABLEAUX | A Modal-Layered Resolution Calculus for K. | Cludia Nalon, Ullrich Hustadt, Clare Dixon |
| 2010 | CADE | A Comparison of Solvers for Propositional Dynamic Logic. | Ullrich Hustadt, Renate A. Schmidt |
| 2009 | CADE | Fair Derivations in Monodic Temporal Reasoning. | Michel Ludwig, Ullrich Hustadt |
| 2009 | CADE | A Refined Resolution Calculus for CTL. | Lan Zhang, Ullrich Hustadt, Clare Dixon |
| 2009 | TIME | Resolution-Based Model Construction for PLTL. | Michel Ludwig, Ullrich Hustadt |
| 2006 | JELIA | Automated Reasoning About Metric and Topology. | Ullrich Hustadt, Dmitry Tishkovsky, Frank Wolter, Michael Zakharyaschev |
| 2005 | CADE | Deciding Monodic Fragments by Temporal Resolution. | Ullrich Hustadt, Boris Konev, Renate A. Schmidt |
| 2005 | IJCAI | Data Complexity of Reasoning in Very Expressive Description Logics. | Ullrich Hustadt, Boris Motik, Ulrike Sattler |
| 2004 | CADE | TeMP: A Temporal Monodic Prover. | Ullrich Hustadt, Boris Konev, Alexandre Riazanov, Andrei Voronkov |
| 2004 | ECAI | Reasoning in Description Logics with a Concrete Domain in the Framework of Resolution. | Ullrich Hustadt, Boris Motik, Ulrike Sattler |
| 2004 | KR | Reducing SHIQ-Description Logic to Disjunctive Datalog Programs. | Ullrich Hustadt, Boris Motik, Ulrike Sattler |
| 2004 | LPAR | A Decomposition Rule for Decision Procedures by Resolution-Based Calculi. | Ullrich Hustadt, Boris Motik, Ulrike Sattler |
| 2003 | CADE | TRP++2.0: A Temporal Resolution Prover. | Ullrich Hustadt, Boris Konev |
| 2003 | CADE | A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. | Renate A. Schmidt, Ullrich Hustadt |
| 2003 | TIME | Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case. | Boris Konev, Anatoli Degtyarev, Clare Dixon, Michael Fisher, Ullrich Hustadt |
| 2002 | CADE | A New Clausal Class Decidable by Hyperresolution. | Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt |
| 2002 | KR | Scientific Benchmarking with Temporal Logic Decision Procedures. | Ullrich Hustadt, Renate A. Schmidt |
| 2001 | LPAR | Computational Space Efficiency and Minimal Model Generation for Guarded Formulae. | Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt |
| 2001 | TIME | Reasoning about agents in the KARO framework. | Ullrich Hustadt, Clare Dixon, Renate A. Schmidt, Michael Fisher, John-Jules Ch. Meyer, Wiebe van der Hoek |
| 2000 | CADE | A Resolution Decision Procedure for Fluted Logic. | Renate A. Schmidt, Ullrich Hustadt |
| 2000 | TABLEAUX | MSPASS: Modal Reasoning by Translation and First-Order Resolution. | Ullrich Hustadt, Renate A. Schmidt |
| 1999 | CADE | Maslov's Class K Revisited. | Ullrich Hustadt, Renate A. Schmidt |
| 1999 | IJCAI | On the Relation of Resolution and Tableaux Proof Systems for Description Logics. | Ullrich Hustadt, Renate A. Schmidt |
| 1998 | AiML | A Resolution-Based Decision Procedure for Extensions of K4. | Harald Ganzinger, Ullrich Hustadt, Christoph Meyer, Renate A. Schmidt |
| 1998 | TABLEAUX | Simplification and Backjumping in Modal Tableau. | Ullrich Hustadt, Renate A. Schmidt |
| 1997 | IJCAI | On Evaluating Decision Procedures for Modal Logic. | Ullrich Hustadt, Renate A. Schmidt |