Ullrich Hustadt

Orcid: 0000-0002-0455-0267

Affiliations:
  • University of Liverpool, UK
  • Max Planck Institute for Informatics, Saarbrücken, Germany (former)


According to our database1, Ullrich Hustadt authored at least 78 papers between 1994 and 2023.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic.
Proceedings of the Automated Deduction - CADE 29, 2023

2022
Correction to: Local is Best: Efficient Reductions to Modal Logic K.
J. Autom. Reason., 2022

Local is Best: Efficient Reductions to Modal Logic K.
J. Autom. Reason., 2022

Local Reductions for the Modal Cube.
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021
Efficient Local Reductions to Basic Modal Logic.
Proceedings of the Automated Deduction - CADE 28, 2021

2020
sf K<sub>n</sub> : Architecture, Refinements, Strategies and Experiments.
J. Autom. Reason., 2020

Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations.
J. Autom. Reason., 2020

Multi-scale verification of distributed synchronisation.
Formal Methods Syst. Des., 2020

2019
Modal Resolution: Proofs, Layers, and Refinements.
ACM Trans. Comput. Log., 2019

2018
The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators.
Proceedings of the Formal Methods and Software Engineering, 2018

Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics.
Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), 2018

2017
Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking.
Proceedings of the Quantitative Evaluation of Systems - 14th International Conference, 2017

KSP: A Resolution-based Prover for Multimodal K, Abridged Report.
Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

CRutoN: Automatic Verification of a Robotic Assistant's Behaviours.
Proceedings of the Critical Systems: Formal Methods and Automated Verification - Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems - and, 2017

Theorem Proving for Metric Temporal Logic over the Naturals.
Proceedings of the Automated Deduction - CADE 26, 2017

2016
Probabilistic Model Checking of Ant-Based Positionless Swarming.
Proceedings of the Towards Autonomous Robotic Systems - 17th Annual Conference, 2016

: A Resolution-Based Prover for Multimodal K.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015
A Modal-Layered Resolution Calculus for K.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2015

Ordered Resolution for Coalition Logic.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2015

2014
A resolution calculus for the branching-time temporal logic CTL.
ACM Trans. Comput. Log., 2014

A resolution-based calculus for Coalition Logic.
J. Log. Comput., 2014

A Resolution Prover for Coalition Logic.
Proceedings of the Proceedings 2nd International Workshop on Strategic Reasoning, 2014

2013
First-Order Resolution Methods for Modal Logics.
Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2010
CTL-RP: A computation tree logic resolution prover.
AI Commun., 2010

Implementing a fair monodic temporal logic prover.
AI Commun., 2010

A Comparison of Solvers for Propositional Dynamic Logic.
Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, 2010

2009
Preface.
Ann. Math. Artif. Intell., 2009

Resolution-Based Model Construction for PLTL.
Proceedings of the TIME 2009, 2009

Redundancy Elimination in Monodic Temporal Reasoning.
Proceedings of the 7th International Workshop on First-Order Theorem Proving, 2009

A Refined Resolution Calculus for CTL.
Proceedings of the Automated Deduction, 2009

Fair Derivations in Monodic Temporal Reasoning.
Proceedings of the Automated Deduction, 2009

2008
Deciding expressive description logics in the framework of resolution.
Inf. Comput., 2008

2007
The axiomatic translation principle for modal logic.
ACM Trans. Comput. Log., 2007

Reasoning in Description Logics by a Reduction to Disjunctive Datalog.
J. Autom. Reason., 2007

Computational modal logic.
Proceedings of the Handbook of Modal Logic., 2007

2006
Automated Reasoning About Metric and Topology.
Proceedings of the Logics in Artificial Intelligence, 10th European Conference, 2006

2005
First-Order Temporal Verification in Practice.
J. Autom. Reason., 2005

Mechanising first-order temporal resolution.
Inf. Comput., 2005

Data Complexity of Reasoning in Very Expressive Description Logics.
Proceedings of the IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30, 2005

Description Logics and Disjunctive Datalog - The Story so Far.
Proceedings of the 2005 International Workshop on Description Logics (DL2005), 2005

Deciding Monodic Fragments by Temporal Resolution.
Proceedings of the Automated Deduction, 2005

2004
Interactions between Knowledge, Action and Commitment within Agent Dynamic Logic.
Stud Logica, 2004

A Decomposition Rule for Decision Procedures by Resolution-Based Calculi.
Proceedings of the Logic for Programming, 2004

Reducing SHIQ-Description Logic to Disjunctive Datalog Programs.
Proceedings of the Principles of Knowledge Representation and Reasoning: Proceedings of the Ninth International Conference (KR2004), 2004

Reasoning in Description Logics with a Concrete Domain in the Framework of Resolution.
Proceedings of the 16th Eureopean Conference on Artificial Intelligence, 2004

TeMP: A Temporal Monodic Prover.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003
Hyperresolution for guarded formulae.
J. Symb. Comput., 2003

Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case.
Proceedings of the 10th International Symposium on Temporal Representation and Reasoning / 4th International Conference on Temporal Logic (TIME-ICTL 2003), 2003

A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae.
Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

TRP++2.0: A Temporal Resolution Prover.
Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

Two Proof Systems for Peirce Algebras.
Proceedings of the Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, 2003

Mechanised Reasoning and Model Generation for Extended Modal Logics.
Proceedings of the Theory and Applications of Relational Structures as Knowledge Instruments, 2003

SCAN Is Complete for All Sahlqvist Formulae.
Proceedings of the Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, 2003

2002
Using Resolution for Testing Modal Satisfiability and Building Models.
J. Autom. Reason., 2002

Combinations of Modal Logics.
Artif. Intell. Rev., 2002

Scientific Benchmarking with Temporal Logic Decision Procedures.
Proceedings of the Eights International Conference on Principles and Knowledge Representation and Reasoning (KR-02), 2002

On the relationship between decidable fragments, non-classical logics, and description logics.
Proceedings of the 2002 International Workshop on Description Logics (DL2002), 2002

A New Clausal Class Decidable by Hyperresolution.
Proceedings of the Automated Deduction, 2002

2001
Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 2, Dov M. Gabbay, Mark A. Reynolds, and Marcelo Finger.
J. Log. Lang. Inf., 2001

Reasoning about agents in the KARO framework.
Proceedings of the Eigth International Symposium on Temporal Representation and Reasoning, 2001

Computational Space Efficiency and Minimal Model Generation for Guarded Formulae.
Proceedings of the Logic for Programming, 2001

Resolution Decision Procedures.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000
Resolution-Based Methods for Modal Logics.
Log. J. IGPL, 2000

MSPASS: Modal Reasoning by Translation and First-Order Resolution.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2000

Normal Forms and Proofs in Combined Modal and Temporal Logics.
Proceedings of the Frontiers of Combining Systems, 2000

Verification within the KARO Agent Theory.
Proceedings of the Formal Approaches to Agent-Based Systems, First International Workshop, 2000

A Resolution Decision Procedure for Fluted Logic.
Proceedings of the Automated Deduction, 2000

Practical Proof Methods for Combined Modal and Temporal Logics.
Proceedings of the Seventh Workshop on Automated Reasoning, 2000

1999
Resolution based decision procedures for subclasses of first-order logic.
PhD thesis, 1999

An empirical analysis of modal theorem provers.
J. Appl. Non Class. Logics, 1999

On the Relation of Resolution and Tableaux Proof Systems for Description Logics.
Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, 1999

MSPASS: Subsumption Testing with SPASS.
Proceedings of the 1999 International Workshop on Description Logics (DL'99), Linköping, Sweden, July 30, 1999

Maslov's Class K Revisited.
Proceedings of the Automated Deduction, 1999

1998
Simplification and Backjumping in Modal Tableau.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1998

Issues of Decidability for Description Logics in the Framework of Resolution.
Proceedings of the Automated Deduction in Classical and Non-Classical Logics, 1998

A Resolution-Based Decision Procedure for Extensions of K4.
Proceedings of the Advances in Modal Logic 2, 1998

1997
On Evaluating Decision Procedures for Modal Logic.
Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, 1997

1994
Do we need the closed world assumption in knowledge representation?
Proceedings of the Reasoning about Structured Objects: Knowledge Representation Meets Databases, 1994


  Loading...