Ullrich Hustadt

82 papers A* 5A 15B 8C 4Journal 25Unranked 21

Year	Rank	Type	Title / Venue / Authors
2024	—	`conf`	Model Construction for Modal Clauses. IJCAR (2) Ullrich Hustadt, Fabio Papacchini, Cláudia Nalon, Clare Dixon
2023	A	`conf`	Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic. CADE Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon
2022	J	`jnl`	Correction to: Local is Best: Efficient Reductions to Modal Logic K. J. Autom. Reason. Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon
2022	A	`conf`	Local Reductions for the Modal Cube. IJCAR Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon
2022	J	`jnl`	Local is Best: Efficient Reductions to Modal Logic K. J. Autom. Reason. Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon
2021	A	`conf`	Efficient Local Reductions to Basic Modal Logic. CADE Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon
2020	J	`jnl`	Multi-scale verification of distributed synchronisation. Formal Methods Syst. Des. Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fisher
2020	J	`jnl`	Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations. J. Autom. Reason. Ullrich Hustadt, Ana Ozaki, Clare Dixon
2020	J	`jnl`	sf K J. Autom. Reason. Cláudia Nalon, Ullrich Hustadt, Clare Dixon
2019	J	`jnl`	Modal Resolution: Proofs, Layers, and Refinements. ACM Trans. Comput. Log. Cláudia Nalon, Clare Dixon, Ullrich Hustadt
2018	—	`conf`	Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics. PAAR@FLoC Ullrich Hustadt, Cláudia Nalon, Clare Dixon
2018	J	`jnl`	Multi-Scale Verification of Distributed Synchronisation. CoRR Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fisher
2018	C	`conf`	The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators. ICFEM Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fisher
2017	—	`conf`	CRutoN: Automatic Verification of a Robotic Assistant's Behaviours. FMICS-AVoCS Paul Gainer, Clare Dixon, Kerstin Dautenhahn, Michael Fisher, Ullrich Hustadt, Joe Saunders, Matt Webster
2017	—	`conf`	Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking. QEST Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fisher
2017	A*	`conf`	KSP: A Resolution-based Prover for Multimodal K, Abridged Report. IJCAI Cláudia Nalon, Ullrich Hustadt, Clare Dixon
2017	J	`jnl`	The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators. CoRR Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fisher
2017	A	`conf`	Theorem Proving for Metric Temporal Logic over the Naturals. CADE Ullrich Hustadt, Ana Ozaki, Clare Dixon
2016	A	`conf`	: A Resolution-Based Prover for Multimodal K. IJCAR Cláudia Nalon, Ullrich Hustadt, Clare Dixon
2016	—	`conf`	Probabilistic Model Checking of Ant-Based Positionless Swarming. TAROS Paul Gainer, Clare Dixon, Ullrich Hustadt
2015	B	`conf`	A Modal-Layered Resolution Calculus for K. TABLEAUX Cláudia Nalon, Ullrich Hustadt, Clare Dixon
2015	B	`conf`	Ordered Resolution for Coalition Logic. TABLEAUX Ullrich Hustadt, Paul Gainer, Clare Dixon, Cláudia Nalon, Lan Zhang
2014	—	`conf`	A Resolution Prover for Coalition Logic. SR Cláudia Nalon, Lan Zhang, Clare Dixon, Ullrich Hustadt
2014	J	`jnl`	A resolution calculus for the branching-time temporal logic CTL. ACM Trans. Comput. Log. Lan Zhang, Ullrich Hustadt, Clare Dixon
2014	J	`jnl`	A resolution-based calculus for Coalition Logic. J. Log. Comput. Cláudia Nalon, Lan Zhang, Clare Dixon, Ullrich Hustadt
2013	—	`conf`	First-Order Resolution Methods for Modal Logics. Programming Logics Renate A. Schmidt, Ullrich Hustadt
2010	—	`conf`	A Comparison of Solvers for Propositional Dynamic Logic. PAAR@IJCAR Ullrich Hustadt, Renate A. Schmidt
2010	J	`jnl`	CTL-RP: A computation tree logic resolution prover. AI Commun. Lan Zhang, Ullrich Hustadt, Clare Dixon
2010	J	`jnl`	Implementing a fair monodic temporal logic prover. AI Commun. Michel Ludwig, Ullrich Hustadt
2009	A	`conf`	A Refined Resolution Calculus for CTL. CADE Lan Zhang, Ullrich Hustadt, Clare Dixon
2009	A	`conf`	Fair Derivations in Monodic Temporal Reasoning. CADE Michel Ludwig, Ullrich Hustadt
2009	J	`jnl`	Preface. Ann. Math. Artif. Intell. Silvio Ranise, Ullrich Hustadt
2009	—	`conf`	Redundancy Elimination in Monodic Temporal Reasoning. FTP Michel Ludwig, Ullrich Hustadt
2009	C	`conf`	Resolution-Based Model Construction for PLTL. TIME Michel Ludwig, Ullrich Hustadt
2008	J	`jnl`	Deciding expressive description logics in the framework of resolution. Inf. Comput. Ullrich Hustadt, Boris Motik, Ulrike Sattler
2007	—	`ch.`	Computational modal logic. Handbook of Modal Logic Ian Horrocks, Ullrich Hustadt, Ulrike Sattler, Renate A. Schmidt
2007	J	`jnl`	Reasoning in Description Logics by a Reduction to Disjunctive Datalog. J. Autom. Reason. Ullrich Hustadt, Boris Motik, Ulrike Sattler
2007	J	`jnl`	The axiomatic translation principle for modal logic. ACM Trans. Comput. Log. Renate A. Schmidt, Ullrich Hustadt
2006	B	`conf`	Automated Reasoning About Metric and Topology. JELIA Ullrich Hustadt, Dmitry Tishkovsky, Frank Wolter, Michael Zakharyaschev
2005	A*	`conf`	Data Complexity of Reasoning in Very Expressive Description Logics. IJCAI Ullrich Hustadt, Boris Motik, Ulrike Sattler
2005	A	`conf`	Deciding Monodic Fragments by Temporal Resolution. CADE Ullrich Hustadt, Boris Konev, Renate A. Schmidt
2005	—	`conf`	Description Logics and Disjunctive Datalog - The Story so Far. Description Logics Ullrich Hustadt, Boris Motik
2005	J	`jnl`	First-Order Temporal Verification in Practice. J. Autom. Reason. M. Carmen Fernández Gago, Ullrich Hustadt, Clare Dixon, Michael Fisher, Boris Konev
2005	J	`jnl`	Mechanising first-order temporal resolution. Inf. Comput. Boris Konev, Anatoli Degtyarev, Clare Dixon, Michael Fisher, Ullrich Hustadt
2004	B	`conf`	A Decomposition Rule for Decision Procedures by Resolution-Based Calculi. LPAR Ullrich Hustadt, Boris Motik, Ulrike Sattler
2004	J	`jnl`	Interactions between Knowledge, Action and Commitment within Agent Dynamic Logic. Stud Logica Renate A. Schmidt, Dmitry Tishkovsky, Ullrich Hustadt
2004	A	`conf`	Reasoning in Description Logics with a Concrete Domain in the Framework of Resolution. ECAI Ullrich Hustadt, Boris Motik, Ulrike Sattler
2004	A*	`conf`	Reducing SHIQ-Description Logic to Disjunctive Datalog Programs. KR Ullrich Hustadt, Boris Motik, Ulrike Sattler
2004	A	`conf`	TeMP: A Temporal Monodic Prover. IJCAR Ullrich Hustadt, Boris Konev, Alexandre Riazanov, Andrei Voronkov
2003	A	`conf`	A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. CADE Renate A. Schmidt, Ullrich Hustadt
2003	J	`jnl`	Hyperresolution for guarded formulae. J. Symb. Comput. Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt
2003	—	`ch.`	Mechanised Reasoning and Model Generation for Extended Modal Logics. Theory and Applications of Relational Structures as Knowledge Instruments Renate A. Schmidt, Ullrich Hustadt
2003	—	`conf`	SCAN Is Complete for All Sahlqvist Formulae. RelMiCS Valentin Goranko, Ullrich Hustadt, Renate A. Schmidt, Dimiter Vakarelov
2003	A	`conf`	TRP++2.0: A Temporal Resolution Prover. CADE Ullrich Hustadt, Boris Konev
2003	C	`conf`	Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case. TIME Boris Konev, Anatoli Degtyarev, Clare Dixon, Michael Fisher, Ullrich Hustadt
2003	—	`conf`	Two Proof Systems for Peirce Algebras. RelMiCS Renate A. Schmidt, Ewa Orlowska, Ullrich Hustadt
2002	A	`conf`	A New Clausal Class Decidable by Hyperresolution. CADE Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt
2002	J	`jnl`	Combinations of Modal Logics. Artif. Intell. Rev. Brandon Bennett, Clare Dixon, Michael Fisher, Ullrich Hustadt, Enrico Franconi, Ian Horrocks, Maarten de Rijke
2002	—	`conf`	On the relationship between decidable fragments, non-classical logics, and description logics. Description Logics Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt
2002	A*	`conf`	Scientific Benchmarking with Temporal Logic Decision Procedures. KR Ullrich Hustadt, Renate A. Schmidt
2002	J	`jnl`	Using Resolution for Testing Modal Satisfiability and Building Models. J. Autom. Reason. Ullrich Hustadt, Renate A. Schmidt
2001	B	`conf`	Computational Space Efficiency and Minimal Model Generation for Guarded Formulae. LPAR Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt
2001	C	`conf`	Reasoning about agents in the KARO framework. TIME Ullrich Hustadt, Clare Dixon, Renate A. Schmidt, Michael Fisher, John-Jules Ch. Meyer, Wiebe van der Hoek
2001	—	`ch.`	Resolution Decision Procedures. Handbook of Automated Reasoning Christian G. Fermüller, Alexander Leitsch, Ullrich Hustadt, Tanel Tammet
2001	J	`jnl`	Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 2, Dov M. Gabbay, Mark A. Reynolds, and Marcelo Finger. J. Log. Lang. Inf. Ullrich Hustadt
2000	A	`conf`	A Resolution Decision Procedure for Fluted Logic. CADE Renate A. Schmidt, Ullrich Hustadt
2000	—	`conf`	Hyperresolution for Guarded Formulae. ARW Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt
2000	B	`conf`	MSPASS: Modal Reasoning by Translation and First-Order Resolution. TABLEAUX Ullrich Hustadt, Renate A. Schmidt
2000	—	`conf`	Normal Forms and Proofs in Combined Modal and Temporal Logics. FroCoS Ullrich Hustadt, Clare Dixon, Renate A. Schmidt, Michael Fisher
2000	—	`conf`	Practical Proof Methods for Combined Modal and Temporal Logics. ARW Ullrich Hustadt
2000	J	`jnl`	Resolution-Based Methods for Modal Logics. Log. J. IGPL Ullrich Hustadt, Hans de Nivelle, Renate A. Schmidt
2000	—	`conf`	Verification within the KARO Agent Theory. FAABS Ullrich Hustadt, Clare Dixon, Renate A. Schmidt, Michael Fisher, John-Jules Ch. Meyer, Wiebe van der Hoek
1999	J	`jnl`	An empirical analysis of modal theorem provers. J. Appl. Non Class. Logics Ullrich Hustadt, Renate A. Schmidt
1999	—	`conf`	MSPASS: Subsumption Testing with SPASS. Description Logics Ullrich Hustadt, Renate A. Schmidt, Christoph Weidenbach
1999	A	`conf`	Maslov's Class K Revisited. CADE Ullrich Hustadt, Renate A. Schmidt
1999	A*	`conf`	On the Relation of Resolution and Tableaux Proof Systems for Description Logics. IJCAI Ullrich Hustadt, Renate A. Schmidt
1999	—	`—`	Resolution based decision procedures for subclasses of first-order logic. Ullrich Hustadt
1998	B	`conf`	A Resolution-Based Decision Procedure for Extensions of K4. Advances in Modal Logic Harald Ganzinger, Ullrich Hustadt, Christoph Meyer, Renate A. Schmidt
1998	—	`conf`	Issues of Decidability for Description Logics in the Framework of Resolution. FTP (LNCS Selection) Ullrich Hustadt, Renate A. Schmidt
1998	B	`conf`	Simplification and Backjumping in Modal Tableau. TABLEAUX Ullrich Hustadt, Renate A. Schmidt
1997	—	`conf`	On Evaluating Decision Procedures for Modal Logic. IJCAI (1) Ullrich Hustadt, Renate A. Schmidt
1994	—	`conf`	Do we need the closed world assumption in knowledge representation? KRDB Ullrich Hustadt