Travelled to:1 × Denmark
1 × Estonia
1 × France
1 × Ireland
1 × Italy
2 × Canada
2 × USA
Collaborated with:R.A.Schmidt B.Konev C.Dixon M.Ludwig L.Zhang B.Motik U.Sattler L.Georgieva C.Nalon A.Ozaki A.Riazanov A.Voronkov
Talks about:tempor (6) resolut (5) logic (4) prover (3) monod (3) procedur (2) decis (2) decid (2) class (2) hyperresolut (1)
Person: Ullrich Hustadt
DBLP: Hustadt:Ullrich
Contributed to:
20092005
2004
20042003200220022000199920162017Wrote 13 papers:
- CADE-2009-LudwigH #reasoning
- Fair Derivations in Monodic Temporal Reasoning (ML, UH), pp. 261–276.
- CADE-2009-ZhangHD #calculus
- A Refined Resolution Calculus for CTL (LZ, UH, CD), pp. 245–260.
- CADE-2005-HustadtKS
- Deciding Monodic Fragments by Temporal Resolution (UH, BK, RAS), pp. 204–218.
- IJCAR-2004-HustadtKRV #named #proving
- TeMP: A Temporal Monodic Prover (UH, BK, AR, AV), pp. 326–330.
- KR-2004-HustadtMS #datalog #logic #source code
- Reducing SHIQ-Description Logic to Disjunctive Datalog Programs (UH, BM, US), pp. 152–162.
- CADE-2003-HustadtK #proving
- TRP++2.0: A Temporal Resolution Prover (UH, BK), pp. 274–278.
- CADE-2003-SchmidtH #axiom #first-order
- A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae (RAS, UH), pp. 412–426.
- CADE-2002-GeorgievaHS #decidability
- A New Clausal Class Decidable by Hyperresolution (LG, UH, RAS), pp. 260–274.
- KR-2002-HustadtS #benchmark #logic #metric
- Scientific Benchmarking with Temporal Logic Decision Procedures (UH, RAS), pp. 533–546.
- CADE-2000-SchmidtH #logic
- A Resolution Decision Procedure for Fluted Logic (RAS, UH), pp. 433–448.
- CADE-1999-HustadtS #revisited
- Maslov’s Class K Revisited (UH, RAS), pp. 172–186.
- IJCAR-2016-NalonHD #multimodal #proving
- : A Resolution-Based Prover for Multimodal K (CN, UH, CD), pp. 406–415.
- CADE-2017-HustadtOD #logic #metric #proving #theorem proving
- Theorem Proving for Metric Temporal Logic over the Naturals (UH, AO, CD), pp. 326–343.