@inproceedings{DBLP:conf/ijcar/HustadtPND24,
  author       = {Ullrich Hustadt and
                  Fabio Papacchini and
                  Cl{\'{a}}udia Nalon and
                  Clare Dixon},
  editor       = {Christoph Benzm{\"{u}}ller and
                  Marijn J. H. Heule and
                  Renate A. Schmidt},
  title        = {Model Construction for Modal Clauses},
  booktitle    = {Automated Reasoning - 12th International Joint Conference, {IJCAR}
                  2024, Nancy, France, July 3-6, 2024, Proceedings, Part {II}},
  series       = {Lecture Notes in Computer Science},
  volume       = {14740},
  pages        = {3--23},
  publisher    = {Springer},
  year         = {2024},
  url          = {https://doi.org/10.1007/978-3-031-63501-4\_1},
  doi          = {10.1007/978-3-031-63501-4\_1},
  timestamp    = {Thu, 22 Aug 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/ijcar/HustadtPND24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/NalonHPD23,
  author       = {Cl{\'{a}}udia Nalon and
                  Ullrich Hustadt and
                  Fabio Papacchini and
                  Clare Dixon},
  editor       = {Brigitte Pientka and
                  Cesare Tinelli},
  title        = {Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic},
  booktitle    = {Automated Deduction - {CADE} 29 - 29th International Conference on
                  Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14132},
  pages        = {382--400},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-38499-8\_22},
  doi          = {10.1007/978-3-031-38499-8\_22},
  timestamp    = {Sun, 24 Sep 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/NalonHPD23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jar/PapacchiniNHD22,
  author       = {Fabio Papacchini and
                  Cl{\'{a}}udia Nalon and
                  Ullrich Hustadt and
                  Clare Dixon},
  title        = {Local is Best: Efficient Reductions to Modal Logic {K}},
  journal      = {J. Autom. Reason.},
  volume       = {66},
  number       = {4},
  pages        = {639--666},
  year         = {2022},
  url          = {https://doi.org/10.1007/s10817-022-09630-6},
  doi          = {10.1007/S10817-022-09630-6},
  timestamp    = {Sun, 25 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/jar/PapacchiniNHD22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jar/PapacchiniNHD22a,
  author       = {Fabio Papacchini and
                  Cl{\'{a}}udia Nalon and
                  Ullrich Hustadt and
                  Clare Dixon},
  title        = {Correction to: Local is Best: Efficient Reductions to Modal Logic
                  {K}},
  journal      = {J. Autom. Reason.},
  volume       = {66},
  number       = {4},
  pages        = {1099},
  year         = {2022},
  url          = {https://doi.org/10.1007/s10817-022-09633-3},
  doi          = {10.1007/S10817-022-09633-3},
  timestamp    = {Sun, 25 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/jar/PapacchiniNHD22a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/NalonHPD22,
  author       = {Cl{\'{a}}udia Nalon and
                  Ullrich Hustadt and
                  Fabio Papacchini and
                  Clare Dixon},
  editor       = {Jasmin Blanchette and
                  Laura Kov{\'{a}}cs and
                  Dirk Pattinson},
  title        = {Local Reductions for the Modal Cube},
  booktitle    = {Automated Reasoning - 11th International Joint Conference, {IJCAR}
                  2022, Haifa, Israel, August 8-10, 2022, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {13385},
  pages        = {486--505},
  publisher    = {Springer},
  year         = {2022},
  url          = {https://doi.org/10.1007/978-3-031-10769-6\_29},
  doi          = {10.1007/978-3-031-10769-6\_29},
  timestamp    = {Mon, 24 Oct 2022 16:36:35 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/NalonHPD22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/PapacchiniNHD21,
  author       = {Fabio Papacchini and
                  Cl{\'{a}}udia Nalon and
                  Ullrich Hustadt and
                  Clare Dixon},
  editor       = {Andr{\'{e}} Platzer and
                  Geoff Sutcliffe},
  title        = {Efficient Local Reductions to Basic Modal Logic},
  booktitle    = {Automated Deduction - {CADE} 28 - 28th International Conference on
                  Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12699},
  pages        = {76--92},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-79876-5\_5},
  doi          = {10.1007/978-3-030-79876-5\_5},
  timestamp    = {Thu, 29 Jul 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/PapacchiniNHD21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/fmsd/GainerLDHF20,
  author       = {Paul Gainer and
                  Sven Linker and
                  Clare Dixon and
                  Ullrich Hustadt and
                  Michael Fisher},
  title        = {Multi-scale verification of distributed synchronisation},
  journal      = {Formal Methods Syst. Des.},
  volume       = {55},
  number       = {3},
  pages        = {171--221},
  year         = {2020},
  url          = {https://doi.org/10.1007/s10703-020-00347-z},
  doi          = {10.1007/S10703-020-00347-Z},
  timestamp    = {Fri, 14 May 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/fmsd/GainerLDHF20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jar/NalonHD20,
  author       = {Cl{\'{a}}udia Nalon and
                  Ullrich Hustadt and
                  Clare Dixon},
  title        = {KSP: Architecture, Refinements, Strategies and
                  Experiments},
  journal      = {J. Autom. Reason.},
  volume       = {64},
  number       = {3},
  pages        = {461--484},
  year         = {2020},
  url          = {https://doi.org/10.1007/s10817-018-09503-x},
  doi          = {10.1007/S10817-018-09503-X},
  timestamp    = {Fri, 14 May 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/jar/NalonHD20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jar/HustadtOD20,
  author       = {Ullrich Hustadt and
                  Ana Ozaki and
                  Clare Dixon},
  title        = {Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals
                  via Translations},
  journal      = {J. Autom. Reason.},
  volume       = {64},
  number       = {8},
  pages        = {1553--1610},
  year         = {2020},
  url          = {https://doi.org/10.1007/s10817-020-09541-4},
  doi          = {10.1007/S10817-020-09541-4},
  timestamp    = {Fri, 14 May 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/jar/HustadtOD20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/tocl/NalonDH19,
  author       = {Cl{\'{a}}udia Nalon and
                  Clare Dixon and
                  Ullrich Hustadt},
  title        = {Modal Resolution: Proofs, Layers, and Refinements},
  journal      = {{ACM} Trans. Comput. Log.},
  volume       = {20},
  number       = {4},
  pages        = {23:1--23:38},
  year         = {2019},
  url          = {https://doi.org/10.1145/3331448},
  doi          = {10.1145/3331448},
  timestamp    = {Mon, 28 Aug 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/tocl/NalonDH19.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/HustadtND18,
  author       = {Ullrich Hustadt and
                  Cl{\'{a}}udia Nalon and
                  Clare Dixon},
  editor       = {Boris Konev and
                  Josef Urban and
                  Philipp R{\"{u}}mmer},
  title        = {Evaluating Pre-Processing Techniques for the Separated Normal Form
                  for Temporal Logics},
  booktitle    = {Proceedings of the 6th Workshop on Practical Aspects of Automated
                  Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018),
                  Oxford, UK, July 19th, 2018},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {2162},
  pages        = {34--48},
  publisher    = {CEUR-WS.org},
  year         = {2018},
  url          = {https://ceur-ws.org/Vol-2162/paper-04.pdf},
  timestamp    = {Fri, 10 Mar 2023 16:23:14 +0100},
  biburl       = {https://dblp.org/rec/conf/cade/HustadtND18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/icfem/GainerLDH018,
  author       = {Paul Gainer and
                  Sven Linker and
                  Clare Dixon and
                  Ullrich Hustadt and
                  Michael Fisher},
  editor       = {Jing Sun and
                  Meng Sun},
  title        = {The Power of Synchronisation: Formal Analysis of Power Consumption
                  in Networks of Pulse-Coupled Oscillators},
  booktitle    = {Formal Methods and Software Engineering - 20th International Conference
                  on Formal Engineering Methods, {ICFEM} 2018, Gold Coast, QLD, Australia,
                  November 12-16, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {11232},
  pages        = {160--176},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-030-02450-5\_10},
  doi          = {10.1007/978-3-030-02450-5\_10},
  timestamp    = {Fri, 25 Dec 2020 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/icfem/GainerLDH018.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/abs-1809-10655,
  author       = {Paul Gainer and
                  Sven Linker and
                  Clare Dixon and
                  Ullrich Hustadt and
                  Michael Fisher},
  title        = {Multi-Scale Verification of Distributed Synchronisation},
  journal      = {CoRR},
  volume       = {abs/1809.10655},
  year         = {2018},
  url          = {http://arxiv.org/abs/1809.10655},
  eprinttype    = {arXiv},
  eprint       = {1809.10655},
  timestamp    = {Fri, 05 Oct 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-1809-10655.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/fmics/GainerDDFHSW17,
  author    = {Paul Gainer and
               Clare Dixon and
               Kerstin Dautenhahn and
               Michael Fisher and
               Ullrich Hustadt and
               Joe Saunders and
               Matt Webster},
  title     = {CRutoN: Automatic Verification of a Robotic Assistant's Behaviours},
  editor    = {Laure Petrucci and
               Cristina Seceleanu and
               Ana Cavalcanti},
  booktitle = {Proceedings of the Joint
               22nd International Workshop on Formal Methods for Industrial Critical
               Systems and 17th International Workshop on Automated Verification
               of Critical Systems (FMICS-AVoCS 2017)},
  caddress  = {Turin, Italy},
  cmonth    = sep # {~18--20},
  pages     = {119--133},
  year      = {2017},
  url       = {https://doi.org/10.1007/978-3-319-67113-0_8},
  doi       = {10.1007/978-3-319-67113-0_8},
  series    = {Lecture Notes in Computer Science},
  volume    = {10471},
  publisher = {Springer},
  year      = {2017},
}

@article{Gainer+Linker+Dixon+Hustadt+Fisher@arXiv2017,
  author    = {Paul Gainer and
               Sven Linker and
               Clare Dixon and
               Ullrich Hustadt and
               Michael Fisher},
  title     = {The Power of Synchronisation: Formal Analysis of Power Consumption
               in Networks of Pulse-Coupled Oscillators},
  journal   = {arXiv},
  volume    = {abs/1709.04385},
  year      = {2017},
  url       = {http://arxiv.org/abs/1709.04385},
  abstract  = {We assess the power consumption of network synchronisation protocols,
  particularly the energy required to synchronise all nodes across a
  network. We use the widely adopted approach of bio-inspired,
  pulse-coupled oscillators to achieve network-wide synchronisation and
  provide an extended formal model of just such a protocol, enhanced
  with structures for recording energy usage. Exhaustive analysis is
  then carried out through formal verification, utilising the PRISM
  model checker to calculate the resources consumed on each possible
  system execution. This allows us to assess a range of parameter
  instantiations and to explore trade-offs between power consumption and
  time to synchronise. This provides a principled basis for the formal
  analysis of a much broader range of large-scale network protocols.}
}

We assess the power consumption of network synchronisation protocols, particularly the energy required to synchronise all nodes across a network. We use the widely adopted approach of bio-inspired, pulse-coupled oscillators to achieve network-wide synchronisation and provide an extended formal model of just such a protocol, enhanced with structures for recording energy usage. Exhaustive analysis is then carried out through formal verification, utilising the PRISM model checker to calculate the resources consumed on each possible system execution. This allows us to assess a range of parameter instantiations and to explore trade-offs between power consumption and time to synchronise. This provides a principled basis for the formal analysis of a much broader range of large-scale network protocols.

@inproceedings{Hustadt+Ozaki+Dixon@CADE2017,
  author    = {Ullrich Hustadt and
               Ana Ozaki and
               Clare Dixon},
  title     = {Theorem Proving for Metric Temporal Logic over the Naturals},
  editor    = {Leonardo de Moura},
  booktitle = {Proceedings of the 26th International Conference on
               Automated Deduction (CADE-26)},
  caddress  = {Gothenburg, Sweden}, 
  cmonth    = aug # {~6-11},
  cyear     = {2017},
  pages     = {326--343},
  year      = {2017},
  series    = {Lecture Notes in Computer Science},
  volume    = {10395},
  publisher = {Springer},
  url       = {https://doi.org/10.1007/978-3-319-63046-5_20},
  doi       = {10.1007/978-3-319-63046-5_20},
}

@inproceedings{DBLP:conf/ijcai/NalonHD17,
  author    = {Cl{\'{a}}udia Nalon and
               Ullrich Hustadt and
               Clare Dixon},
  title     = {{KSP:} {A} Resolution-based Prover for Multimodal K, Abridged Report},
  editor    = {Carles Sierra},
  booktitle = {Proceedings of the Twenty-Sixth International Joint Conference on
               Artificial Intelligence (IJCAI 2017)},
  caddress  = {Melbourne, Australia},
  cmonth    = aug # {~19--25},
  cyear     = {2017},
  pages     = {4919--4923},
  year      = {2017},
  crossref  = {DBLP:conf/ijcai/2017},
  url       = {https://doi.org/10.24963/ijcai.2017/694},
  doi       = {10.24963/ijcai.2017/694},
  timestamp = {Tue, 15 Aug 2017 14:48:05 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/ijcai/NalonHD17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/HustadtOD17,
  author       = {Ullrich Hustadt and
                  Ana Ozaki and
                  Clare Dixon},
  editor       = {Leonardo de Moura},
  title        = {Theorem Proving for Metric Temporal Logic over the Naturals},
  booktitle    = {Automated Deduction - {CADE} 26 - 26th International Conference on
                  Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10395},
  pages        = {326--343},
  publisher    = {Springer},
  year         = {2017},
  url          = {https://doi.org/10.1007/978-3-319-63046-5\_20},
  doi          = {10.1007/978-3-319-63046-5\_20},
  timestamp    = {Thu, 29 Sep 2022 08:36:56 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/HustadtOD17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/fmics/GainerDDFHSW17,
  author       = {Paul Gainer and
                  Clare Dixon and
                  Kerstin Dautenhahn and
                  Michael Fisher and
                  Ullrich Hustadt and
                  Joe Saunders and
                  Matt Webster},
  editor       = {Laure Petrucci and
                  Cristina Seceleanu and
                  Ana Cavalcanti},
  title        = {CRutoN: Automatic Verification of a Robotic Assistant's Behaviours},
  booktitle    = {Critical Systems: Formal Methods and Automated Verification - Joint
                  22nd International Workshop on Formal Methods for Industrial Critical
                  Systems - and - 17th International Workshop on Automated Verification
                  of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18-20,
                  2017, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10471},
  pages        = {119--133},
  publisher    = {Springer},
  year         = {2017},
  url          = {https://doi.org/10.1007/978-3-319-67113-0\_8},
  doi          = {10.1007/978-3-319-67113-0\_8},
  timestamp    = {Mon, 21 Feb 2022 14:40:51 +0100},
  biburl       = {https://dblp.org/rec/conf/fmics/GainerDDFHSW17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/ijcai/NalonHD17,
  author       = {Cl{\'{a}}udia Nalon and
                  Ullrich Hustadt and
                  Clare Dixon},
  editor       = {Carles Sierra},
  title        = {{KSP:} {A} Resolution-based Prover for Multimodal K, Abridged Report},
  booktitle    = {Proceedings of the Twenty-Sixth International Joint Conference on
                  Artificial Intelligence, {IJCAI} 2017, Melbourne, Australia, August
                  19-25, 2017},
  pages        = {4919--4923},
  publisher    = {ijcai.org},
  year         = {2017},
  url          = {https://doi.org/10.24963/ijcai.2017/694},
  doi          = {10.24963/IJCAI.2017/694},
  timestamp    = {Tue, 20 Aug 2019 16:16:54 +0200},
  biburl       = {https://dblp.org/rec/conf/ijcai/NalonHD17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/qest/GainerLDHF17,
  author       = {Paul Gainer and
                  Sven Linker and
                  Clare Dixon and
                  Ullrich Hustadt and
                  Michael Fisher},
  editor       = {Nathalie Bertrand and
                  Luca Bortolussi},
  title        = {Investigating Parametric Influence on Discrete Synchronisation Protocols
                  Using Quantitative Model Checking},
  booktitle    = {Quantitative Evaluation of Systems - 14th International Conference,
                  {QEST} 2017, Berlin, Germany, September 5-7, 2017, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10503},
  pages        = {224--239},
  publisher    = {Springer},
  year         = {2017},
  url          = {https://doi.org/10.1007/978-3-319-66335-7\_14},
  doi          = {10.1007/978-3-319-66335-7\_14},
  timestamp    = {Fri, 25 Dec 2020 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/qest/GainerLDHF17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/abs-1709-04385,
  author       = {Paul Gainer and
                  Sven Linker and
                  Clare Dixon and
                  Ullrich Hustadt and
                  Michael Fisher},
  title        = {The Power of Synchronisation: Formal Analysis of Power Consumption
                  in Networks of Pulse-Coupled Oscillators},
  journal      = {CoRR},
  volume       = {abs/1709.04385},
  year         = {2017},
  url          = {http://arxiv.org/abs/1709.04385},
  eprinttype    = {arXiv},
  eprint       = {1709.04385},
  timestamp    = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-1709-04385.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Gainer+Dixon+Hustadt@TAROS2016,
 author    = {Paul Gainer and
              Clare Dixon and
              Ullrich Hustadt},
 title     = {Probabilistic Model Checking of Ant-Based Positionless Swarming},
 editor    = {Lyuba Alboul and
              Dana D. Damian and
              Jonathan M. Aitken},
 booktitle = {Proceedings of the 17th Annual Conference Towards Autonomous Robotic Systems (TAROS 2016)},
 pages     = {127--138},
 series    = {Lecture Notes in Computer Science},
 volume    = {9716},
 publisher = {Springer},
 year      = {2016},
}

@inproceedings{Nalon+Hustadt+Dixon@IJCAR2016,
 author    = {Cl{\'{a}}udia Nalon and
              Ullrich Hustadt and
              Clare Dixon},
 title     = {KSP: {A} Resolution-Based Prover for Multimodal {K}},
 booktitle = {Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016)},
 pages     = {406--415},
 editor    = {Nicola Olivetti and
              Ashish Tiwari},
 series    = {Lecture Notes in Computer Science},
 volume    = {9706},
 year      = {2016},
}

@inproceedings{DBLP:conf/cade/NalonHD16,
  author       = {Cl{\'{a}}udia Nalon and
                  Ullrich Hustadt and
                  Clare Dixon},
  editor       = {Nicola Olivetti and
                  Ashish Tiwari},
  title        = {: {A} Resolution-Based Prover for Multimodal {K}},
  booktitle    = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
                  2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9706},
  pages        = {406--415},
  publisher    = {Springer},
  year         = {2016},
  url          = {https://doi.org/10.1007/978-3-319-40229-1\_28},
  doi          = {10.1007/978-3-319-40229-1\_28},
  timestamp    = {Mon, 26 Jun 2023 20:45:22 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/NalonHD16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/taros/GainerDH16,
  author       = {Paul Gainer and
                  Clare Dixon and
                  Ullrich Hustadt},
  editor       = {Lyuba Alboul and
                  Dana D. Damian and
                  Jonathan M. Aitken},
  title        = {Probabilistic Model Checking of Ant-Based Positionless Swarming},
  booktitle    = {Towards Autonomous Robotic Systems - 17th Annual Conference, {TAROS}
                  2016, Sheffield, UK, June 26 - July 1, 2016, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9716},
  pages        = {127--138},
  publisher    = {Springer},
  year         = {2016},
  url          = {https://doi.org/10.1007/978-3-319-40379-3\_13},
  doi          = {10.1007/978-3-319-40379-3\_13},
  timestamp    = {Mon, 03 Jan 2022 22:19:33 +0100},
  biburl       = {https://dblp.org/rec/conf/taros/GainerDH16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@INPROCEEDINGS{Hustadt+Gainer+Dixon+Nalon+Zhang@TABLEAUX2015,
 AUTHOR        = {Hustadt, Ullrich and Gainer, Paul and Dixon, Clare and Nalon, Cl{\'a}udia and Zhang, Lan},
 TITLE         = {Ordered Resolution for Coalition Logic},
 PAGES         = {165-180},
 BOOKTITLE     = {Proceedings of the International Conference on
 Automated Reasoning with Analytic Tableaux and Related Methods 
 (TABLEAUX 2015) [Wroclaw, Poland, 20--24 September 2015]},
 YEAR          = {2015},
 EDITOR        = {de Nivelle, Hans},
 PUBLISHER     = {Springer International Publishing Switzerland},
 PADDRESS      = {Cham, Switzerland},
 PYEAR         = {2015},
 CADDRESS      = {Wroclaw, Poland},
 CYEAR         = {2015},
 CMONTH        = sep # {20--24},
 SERIES        = {LNAI},
 VOLUME        = {9323},
 URL           = {Hustadt+Gainer+Dixon+Nalon+Zhang@TABLEAUX2015.pdf},
 ABSTRACT      = {In this paper we introduce a calculus based on ordered
 resolution for Coalition Logic (CL), improving our previous approach based
 on unrefined resolution, and discuss the problems associated with imposing
 an ordering refinement in the context of CL. The calculus operates
 on `coalition problems', a normal form for CL where we use coalition
 vectors that can represent choices made by agents explicitly, and the
 inference rules of the calculus provide the basis for a decision procedure
 for the satisfiability problem in CL. We give correctness, termination
 and complexity results for our calculus. We also present experimental
 results for an implementation of the calculus and show that it outperforms
 a tableau-based decision procedure for Alternating-Time Temporal
 Logic (ATL) on two classes of benchmark formulae for CL.}
}

In this paper we introduce a calculus based on ordered resolution for Coalition Logic (CL), improving our previous approach based on unrefined resolution, and discuss the problems associated with imposing an ordering refinement in the context of CL. The calculus operates on `coalition problems', a normal form for CL where we use coalition vectors that can represent choices made by agents explicitly, and the inference rules of the calculus provide the basis for a decision procedure for the satisfiability problem in CL. We give correctness, termination and complexity results for our calculus. We also present experimental results for an implementation of the calculus and show that it outperforms a tableau-based decision procedure for Alternating-Time Temporal Logic (ATL) on two classes of benchmark formulae for CL.

@INPROCEEDINGS{Nalon+Hustadt+Dixon@TABLEAUX2015,
 AUTHOR        = {Nalon, Cl{\'a}udia and Hustadt, Ullrich and Dixon, Clare},
 TITLE         = {A Modal-Layered Resolution Calculus for {K}},
 PAGES         = {181--196},
 BOOKTITLE     = {Proceedings of the International Conference on
 Automated Reasoning with Analytic Tableaux and Related Methods 
 (TABLEAUX 2015) [Wroclaw, Poland, 20--24 September 2015]},
 YEAR          = {2015},
 EDITOR        = {de Nivelle, Hans},
 PUBLISHER     = {Springer International Publishing Switzerland},
 PADDRESS      = {Cham, Switzerland},
 PYEAR         = {2015},
 CADDRESS      = {Wroclaw, Poland},
 CYEAR         = {2015},
 CMONTH        = sep # {20--24},
 SERIES        = {LNAI},
 VOLUME        = {9323},
 URL           = {Nalon+Hustadt+Dixon@TABLEAUX2015.pdf},
 ABSTRACT      = {Resolution-based provers for multimodal normal logics require pruning
 of the search space for a proof in order to deal with the inherent intractability
 of the satisfiability problem for such logics. We present a clausal modal-layered
 hyper-resolution calculus for the basic multimodal logic, which divides the clause
 set according to the modal depth at which clauses occur. We show that the calculus
 is complete for the logics being considered. We also show that the calculus
 can be combined with other strategies. In particular, we discuss the completeness
 of combining modal layering and negative resolution. In addition, we present an
 incompleteness result for modal layering together with ordered resolution.}
}

Resolution-based provers for multimodal normal logics require pruning of the search space for a proof in order to deal with the inherent intractability of the satisfiability problem for such logics. We present a clausal modal-layered hyper-resolution calculus for the basic multimodal logic, which divides the clause set according to the modal depth at which clauses occur. We show that the calculus is complete for the logics being considered. We also show that the calculus can be combined with other strategies. In particular, we discuss the completeness of combining modal layering and negative resolution. In addition, we present an incompleteness result for modal layering together with ordered resolution.

@inproceedings{DBLP:conf/tableaux/HustadtGDNZ15,
  author       = {Ullrich Hustadt and
                  Paul Gainer and
                  Clare Dixon and
                  Cl{\'{a}}udia Nalon and
                  Lan Zhang},
  editor       = {Hans de Nivelle},
  title        = {Ordered Resolution for Coalition Logic},
  booktitle    = {Automated Reasoning with Analytic Tableaux and Related Methods - 24th
                  International Conference, {TABLEAUX} 2015, Wroc{\l}aw, Poland, September
                  21-24, 2015. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9323},
  pages        = {169--184},
  publisher    = {Springer},
  year         = {2015},
  url          = {https://doi.org/10.1007/978-3-319-24312-2\_12},
  doi          = {10.1007/978-3-319-24312-2\_12},
  timestamp    = {Sat, 19 Oct 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/tableaux/HustadtGDNZ15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tableaux/NalonHD15,
  author       = {Cl{\'{a}}udia Nalon and
                  Ullrich Hustadt and
                  Clare Dixon},
  editor       = {Hans de Nivelle},
  title        = {A Modal-Layered Resolution Calculus for {K}},
  booktitle    = {Automated Reasoning with Analytic Tableaux and Related Methods - 24th
                  International Conference, {TABLEAUX} 2015, Wroc{\l}aw, Poland, September
                  21-24, 2015. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9323},
  pages        = {185--200},
  publisher    = {Springer},
  year         = {2015},
  url          = {https://doi.org/10.1007/978-3-319-24312-2\_13},
  doi          = {10.1007/978-3-319-24312-2\_13},
  timestamp    = {Sat, 19 Oct 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/tableaux/NalonHD15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@JOURNAL{Nalon+Zhang+Dixon+Hustadt@JLC2014,
 AUTHOR        = {Cl{\'a}udia Nalon and Lan Zhang and Clare Dixon and Ullrich Hustadt},
 TITLE         = {A resolution-based calculus for Coalition Logic},
 JOURNAL       = {Journal of Logic and Computation},
 VOLUME        = {24},
 NUMBER        = {4},
 PAGES         = {883-917},
 YEAR          = {2014},
 URL           = {http://logcom.oxfordjournals.org/content/24/4/883},
 ABSTRACT      = {We present a resolution-based calculus for the Coalition Logic CL, a
non-normal modal logic used for reasoning about cooperative agency. We present
a normal form and a set of resolution-based inference rules to solve the 
satisfiability problem in CL. We also show that the calculus presented here is sound,
complete, and terminating.}
}

We present a resolution-based calculus for the Coalition Logic CL, a non-normal modal logic used for reasoning about cooperative agency. We present a normal form and a set of resolution-based inference rules to solve the satisfiability problem in CL. We also show that the calculus presented here is sound, complete, and terminating.

@INPROCEEDINGS{Nalon+Zhang+Dixon+Hustadt@SR2014,
 AUTHOR        = {Cl{\'a}udia Nalon and Lan Zhang and Clare Dixon and Ullrich Hustadt},
 TITLE         = {A Resolution Prover for Coalition Logic},
 EDITOR        = {F.~Mogavero and A.~Murano and M.~Y.~Vardi},
 BOOKTITLE     = {Proceedings 2nd International Workshop on Strategic Reasoning (SR 2014)},
 SERIES        = {Electronic Proceedings in Theoretical Computer Science},
 VOLUME        = {146},
 PAGES         = {65-74},
 YEAR          = {2014},
 ABSTRACT      = {We present a prototype tool for automated reasoning for Coalition Logic,
 a non-normal modal logic that can be used for reasoning about cooperative agency. The
 theorem prover CLProver is based on recent work on a resolution-based calculus for
 Coalition Logic that operates on coalition problems, a normal form for Coalition Logic.
 We provide an overview of coalition problems and of the resolution-based calculus for
 Coalition Logic. We then give details of the implementation of CLProver and present the
 results for a comparison with an existing tableau-based solver.}
}

We present a prototype tool for automated reasoning for Coalition Logic, a non-normal modal logic that can be used for reasoning about cooperative agency. The theorem prover CLProver is based on recent work on a resolution-based calculus for Coalition Logic that operates on coalition problems, a normal form for Coalition Logic. We provide an overview of coalition problems and of the resolution-based calculus for Coalition Logic. We then give details of the implementation of CLProver and present the results for a comparison with an existing tableau-based solver.

@article{Zhang+Hustadt+Dixon@ToCL2014,
 author    = {Lan Zhang and Ullrich Hustadt and Clare Dixon},
 title     = {A Resolution Calculus for Branching-Time Temporal Logic {CTL}},
 journal   = {ACM Transactions on Computational Logic},
 year      = {2014},
 month     = feb,
 volume    = {15},
 number    = {1},
 pages     = {10:1-38},
 url       = {http://cgi.csc.liv.ac.uk/~ullrich/publications/Zhang+Hustadt+Dixon@ToCL2014.pdf},
 abstract  = {The branching-time temporal logic CTL is useful for
 specifying systems that change over time and involve quantification
 over possible futures. Here we present a resolution calculus for CTL
 that involves the trans- lation of formulae to a normal form and the
 application of a number of resolution rules. We use indices in the
 normal form to represent particular paths and the application of the
 resolution rules is restricted dependent on an ordering and selection
 function to reduce the search space. We show that the translation
 preserves satisfiability, the calculus is sound, complete and
 terminating and consider the complexity of the calculus.}
}

The branching-time temporal logic CTL is useful for specifying systems that change over time and involve quantification over possible futures. Here we present a resolution calculus for CTL that involves the trans- lation of formulae to a normal form and the application of a number of resolution rules. We use indices in the normal form to represent particular paths and the application of the resolution rules is restricted dependent on an ordering and selection function to reduce the search space. We show that the translation preserves satisfiability, the calculus is sound, complete and terminating and consider the complexity of the calculus.

@article{DBLP:journals/logcom/NalonZDH14,
  author       = {Cl{\'{a}}udia Nalon and
                  Lan Zhang and
                  Clare Dixon and
                  Ullrich Hustadt},
  title        = {A resolution-based calculus for Coalition Logic},
  journal      = {J. Log. Comput.},
  volume       = {24},
  number       = {4},
  pages        = {883--917},
  year         = {2014},
  url          = {https://doi.org/10.1093/logcom/ext074},
  doi          = {10.1093/LOGCOM/EXT074},
  timestamp    = {Sat, 19 Oct 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/logcom/NalonZDH14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/tocl/ZhangHD14,
  author       = {Lan Zhang and
                  Ullrich Hustadt and
                  Clare Dixon},
  title        = {A resolution calculus for the branching-time temporal logic {CTL}},
  journal      = {{ACM} Trans. Comput. Log.},
  volume       = {15},
  number       = {1},
  pages        = {10:1--10:38},
  year         = {2014},
  url          = {https://doi.org/10.1145/2529993},
  doi          = {10.1145/2529993},
  timestamp    = {Sat, 19 Oct 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/tocl/ZhangHD14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:journals/corr/NalonZDH14,
  author       = {Cl{\'{a}}udia Nalon and
                  Lan Zhang and
                  Clare Dixon and
                  Ullrich Hustadt},
  editor       = {Fabio Mogavero and
                  Aniello Murano and
                  Moshe Y. Vardi},
  title        = {A Resolution Prover for Coalition Logic},
  booktitle    = {Proceedings 2nd International Workshop on Strategic Reasoning, {SR}
                  2014, Grenoble, France, April 5-6, 2014},
  series       = {{EPTCS}},
  volume       = {146},
  pages        = {65--73},
  year         = {2014},
  url          = {https://doi.org/10.4204/EPTCS.146.9},
  doi          = {10.4204/EPTCS.146.9},
  timestamp    = {Sat, 30 Sep 2023 10:08:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/NalonZDH14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@TECHREPORT{Nalon+Zhang+Dixon+Hustadt@ULCSTR2013,
 AUTHOR        = {Cl{\'a}udia Nalon and Lan Zhang and Clare Dixon and Ullrich Hustadt},
 TITLE         = {A resolution-based calculus for Coalition Logic (Extended Version)},
 INSTITUTION   = {Department of Computer Science, University of Liverpool},
 YEAR          = {2013},
 TYPE          = {Technical Report},
 NUMBER        = {ULCS-13-004},
 ADDRESS       = {Liverpool, UK},
 URL           = {http://intranet.csc.liv.ac.uk/research/techreports/tr2013/ulcs-13-004.pdf},
 ABSTRACT      = {We present a resolution-based calculus for the Coalition Logic CL, a
non-normal modal logic used for reasoning about cooperative agency. We present
a normal form and a set of resolution-based inference rules to solve the 
satisfiability problem in CL. We also show that the calculus presented here is sound,
complete, and terminating.}
}

We present a resolution-based calculus for the Coalition Logic CL, a non-normal modal logic used for reasoning about cooperative agency. We present a normal form and a set of resolution-based inference rules to solve the satisfiability problem in CL. We also show that the calculus presented here is sound, complete, and terminating.

@incollection{Schmidt+Hustadt@ProgLog2013,
 author    = {Schmidt, Renate A. and Hustadt, Ullrich},
 title     = {First-Order Resolution Methods for Modal Logics},
 booktitle = {Programming Logics},
 pages     = {345-391},
 editor    = {Voronkov, Andrei and Weidenbach, Christoph},
 year      = {2013},
 isbn      = {978-3-642-37650-4},
 volume    = {7797},
 series    = {Lecture Notes in Computer Science},
 doi       = {10.1007/978-3-642-37651-1_15},
 url       = {http://dx.doi.org/10.1007/978-3-642-37651-1_15},
 publisher = {Springer},
 abstract  = {In this paper we give an overview of results for modal
 logic which can be shown using techniques and methods from first-order
 logic and resolution. Because of the breadth of the area and the many
 applications we focus on the use of first-order resolution methods for
 modal logics. In addition to traditional propositional modal logics we
 consider more expressive PDL-like dynamic modal logics closely related
 to description logics. Without going into too much detail, we survey
 different ways of translating modal logics into first-order logic, we
 explore different ways of using first-order resolution theorem provers
 to solve a range of reasoning problems for modal logics, and we
 discuss a variety of results which have been obtained in the setting
 of first-order resolution.}
}

In this paper we give an overview of results for modal logic which can be shown using techniques and methods from first-order logic and resolution. Because of the breadth of the area and the many applications we focus on the use of first-order resolution methods for modal logics. In addition to traditional propositional modal logics we consider more expressive PDL-like dynamic modal logics closely related to description logics. Without going into too much detail, we survey different ways of translating modal logics into first-order logic, we explore different ways of using first-order resolution theorem provers to solve a range of reasoning problems for modal logics, and we discuss a variety of results which have been obtained in the setting of first-order resolution.

@inproceedings{DBLP:conf/birthday/SchmidtH13,
  author       = {Renate A. Schmidt and
                  Ullrich Hustadt},
  editor       = {Andrei Voronkov and
                  Christoph Weidenbach},
  title        = {First-Order Resolution Methods for Modal Logics},
  booktitle    = {Programming Logics - Essays in Memory of Harald Ganzinger},
  series       = {Lecture Notes in Computer Science},
  volume       = {7797},
  pages        = {345--391},
  publisher    = {Springer},
  year         = {2013},
  url          = {https://doi.org/10.1007/978-3-642-37651-1\_15},
  doi          = {10.1007/978-3-642-37651-1\_15},
  timestamp    = {Wed, 25 Sep 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/birthday/SchmidtH13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@INPROCEEDINGS{Hustadt+Schmidt@PAAR2010,
 AUTHOR        = {Hustadt, Ullrich and Schmidt, Renate, A.},
 TITLE         = {A Comparison of Solvers for Propositional Dynamic Logic},
 BOOKTITLE     = {Proceedings of the Workshop on Practical Aspect of Automated Reasoning (PAAR-2010)
 [Edinburgh, Scotland, 14 July 2010]},
 YEAR          = {2010},
 EDITOR        = {Konev, B. and Schmidt, Renate A. and Schulz, Stephan},
 PAGES         = {},
 CADDRESS      = {Edinburgh, Scotland},
 CYEAR         = {2010},
 CMONTH        = jul # {~14},
 URL           = {Hustadt+Schmidt@PAAR2010.pdf},
 ABSTRACT      = {Calculi for propositional dynamic logics have been investigated since
the introduction of this logic in the late seventies. Only in recent
years have practical procedures been suggested and implemented. In
this paper, we compare three such systems, namely, the
Tableau Workbench by Abate, Goré, and Widmann
(2009), the pdlProver system by Goré and Widmann (2009), and
the MLSolver system by Friedmann and Lange (2009).
<p>
The benchmarking formulae used in this paper are available in
MLSolver and pdlProver syntax:
<ul style="margin-top: -10; margin-left: 0; padding-left: 20px;">
<li>C<sub>PDL</sub><sup>1</sup> (n=5, k=3, p=0.5): 
in <a href="http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/mlsolver-Cpdl1-5-3.zip">MLSolver syntax</a>, 
in <a href="http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/pdlProver-Cpdl1-5-3.zip">pdlProver syntax</a>
</li>
<li>C<sub>PDL</sub><sup>2</sup> (n=5, k=3, p=0.5): 
in <a href="http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/mlsolver-Cpdl2-5-3.zip">MLSolver syntax</a>, 
in <a href="http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/pdlProver-Cpdl2-5-3.zip">pdlProver syntax</a>
</li>
</ul>}
}

Calculi for propositional dynamic logics have been investigated since the introduction of this logic in the late seventies. Only in recent years have practical procedures been suggested and implemented. In this paper, we compare three such systems, namely, the Tableau Workbench by Abate, Goré, and Widmann (2009), the pdlProver system by Goré and Widmann (2009), and the MLSolver system by Friedmann and Lange (2009).

The benchmarking formulae used in this paper are available in MLSolver and pdlProver syntax:

• C_PDL¹ (n=5, k=3, p=0.5): in MLSolver syntax, in pdlProver syntax
• C_PDL² (n=5, k=3, p=0.5): in MLSolver syntax, in pdlProver syntax

@ARTICLE{Ludwig+Hustadt@AIC2010,
 AUTHOR   = {Ludwig, Michel and Hustadt, Ullrich},
 TITLE    = {Implementing a fair monodic temporal logic prover},
 JOURNAL  = {AI Communications},
 VOLUME   = {23},
 NUMBER   = {2--3},
 PAGES    = {69-96},
 YEAR     = {2010},
 URL      = {http://iospress.metapress.com/content/h7262n0780p40027/fulltext.pdf},
 ABSTRACT = {Monodic first-order temporal logic is a fragment of
 first-order temporal logic for which sound and complete calculi have
 been devised. One such calculus is ordered fine-grained resolution
 with selection, which is implemented in the theorem prover
 TeMP. However, the architecture of TeMP cannot guarantee the fairness
 of its derivations. In this paper we present an architecture for a
 resolution-based monodic first-order temporal logic prover that can
 ensure fair derivations and we describe the implementation of this
 fair architecture in the theorem prover TSPASS.}
}

Monodic first-order temporal logic is a fragment of first-order temporal logic for which sound and complete calculi have been devised. One such calculus is ordered fine-grained resolution with selection, which is implemented in the theorem prover TeMP. However, the architecture of TeMP cannot guarantee the fairness of its derivations. In this paper we present an architecture for a resolution-based monodic first-order temporal logic prover that can ensure fair derivations and we describe the implementation of this fair architecture in the theorem prover TSPASS.

@ARTICLE{Zhang+Hustadt+Dixon@AIC2010,
 AUTHOR  = {Zhang, Lan and Hustadt, Ullrich and Dixon, Clare},
 TITLE   = {{CTL-RP}: A computation tree logic resolution prover},
 JOURNAL = {AI Communications},
 VOLUME  = {23},
 NUMBER  = {2--3},
 PAGES   = {111-136},
 YEAR    = {2010},
 URL      = {http://iospress.metapress.com/content/x125544601352537/fulltext.pdf},
 ABSTRACT = {In this paper, we present a resolution-based calculus RCTL<sup>>,S</sup> for Computation Tree Logic (CTL) 
as well as an implementation of that calculus in the theorem prover CTL-RP. The calculus RCTL<sup>>,S</sup> 
requires a transformation of an arbitrary CTL formula to an equi-satisfiable clausal normal form formulated
in an extension of CTL with indexed path formulae. The calculus itself consists of a set of resolution rules 
which can be used for an EXPTIME decision procedure for the satisfiability problem of CTL. We give a formal
semantics for the clausal normal form, provide proof sketches for the soundness and completeness of the 
resolution rules, discuss the complexity of the decision procedure based on RCTL<sup>>,S</sup>, and present 
an approach to implementing the calculus RCTL<sup>>,S</sup> using first-order techniques. Finally, we give 
a comparison between CTL-RP and a tableau theorem prover for CTL.}
}

In this paper, we present a resolution-based calculus RCTL^>,S for Computation Tree Logic (CTL) as well as an implementation of that calculus in the theorem prover CTL-RP. The calculus RCTL^>,S requires a transformation of an arbitrary CTL formula to an equi-satisfiable clausal normal form formulated in an extension of CTL with indexed path formulae. The calculus itself consists of a set of resolution rules which can be used for an EXPTIME decision procedure for the satisfiability problem of CTL. We give a formal semantics for the clausal normal form, provide proof sketches for the soundness and completeness of the resolution rules, discuss the complexity of the decision procedure based on RCTL^>,S, and present an approach to implementing the calculus RCTL^>,S using first-order techniques. Finally, we give a comparison between CTL-RP and a tableau theorem prover for CTL.

@article{DBLP:journals/aicom/LudwigH10,
  author       = {Michel Ludwig and
                  Ullrich Hustadt},
  title        = {Implementing a fair monodic temporal logic prover},
  journal      = {{AI} Commun.},
  volume       = {23},
  number       = {2-3},
  pages        = {69--96},
  year         = {2010},
  url          = {https://doi.org/10.3233/AIC-2010-0457},
  doi          = {10.3233/AIC-2010-0457},
  timestamp    = {Thu, 18 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/aicom/LudwigH10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/aicom/ZhangHD10,
  author       = {Lan Zhang and
                  Ullrich Hustadt and
                  Clare Dixon},
  title        = {{CTL-RP:} {A} computation tree logic resolution prover},
  journal      = {{AI} Commun.},
  volume       = {23},
  number       = {2-3},
  pages        = {111--136},
  year         = {2010},
  url          = {https://doi.org/10.3233/AIC-2010-0463},
  doi          = {10.3233/AIC-2010-0463},
  timestamp    = {Sat, 19 Oct 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/aicom/ZhangHD10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/HustadtS10,
  author       = {Ullrich Hustadt and
                  Renate A. Schmidt},
  editor       = {Renate A. Schmidt and
                  Stephan Schulz and
                  Boris Konev},
  title        = {A Comparison of Solvers for Propositional Dynamic Logic},
  booktitle    = {Proceedings of the 2nd Workshop on Practical Aspects of Automated
                  Reasoning, PAAR-2010, Edinburgh, Scotland, UK, July 14, 2010},
  series       = {EPiC Series in Computing},
  volume       = {9},
  pages        = {63--73},
  publisher    = {EasyChair},
  year         = {2010},
  url          = {https://doi.org/10.29007/63hq},
  doi          = {10.29007/63HQ},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/HustadtS10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Ludwig+Hustadt@CADE2009,
 author    = {Michel Ludwig and Ullrich Hustadt},
 title     = {Fair Derivations in Monodic Temporal Reasoning},
 year      = {2009},
 pages     = {261-276},
 editor    = {Renate A. Schmidt},
 booktitle = {Proceedings of the 22nd International Conference
              on Automated Deduction (CADE-22),
	      [Montreal, Canada, 2-7 August 2009]},
 publisher = {Springer},
 series    = {Lecture Notes in Computer Science},
 volume    = {5663},
 year      = {2009},
 isbn      = {978-3-642-02958-5},
 bibsource = {DBLP, http://dblp.uni-trier.de},
 url       = {http://dx.doi.org/10.1007/978-3-642-02959-2_21},
 abstract  = {Ordered fine-grained resolution with selection is a
 sound and complete resolution-based calculus for monodic first-order
 temporal logic. The inference rules of the calculus are based on
 standard resolution between different types of temporal clauses on one
 hand and inference rules with semi-decidable applicability conditions
 that handle eventualities on the other hand. In this paper we
 illustrate how the combination of these two different types of
 inference rules can lead to unfair derivations in practice. We also
 present an inference procedure that allows us to construct fair
 derivations and prove its refutational completeness. We conclude with
 some experimental results obtained with the implementation of the new
 procedure in the theorem prover TSPASS.}
}

Ordered fine-grained resolution with selection is a sound and complete resolution-based calculus for monodic first-order temporal logic. The inference rules of the calculus are based on standard resolution between different types of temporal clauses on one hand and inference rules with semi-decidable applicability conditions that handle eventualities on the other hand. In this paper we illustrate how the combination of these two different types of inference rules can lead to unfair derivations in practice. We also present an inference procedure that allows us to construct fair derivations and prove its refutational completeness. We conclude with some experimental results obtained with the implementation of the new procedure in the theorem prover TSPASS.

@INPROCEEDINGS{Ludwig+Hustadt@FTP2009,
 AUTHOR        = {Ludwig, Michel and Hustadt, Ullrich},
 TITLE         = {Redundancy Elimination in Monodic Temporal Reasoning},
 BOOKTITLE     = {Proceedings of the 7th International Workshop on First-Order
Theorem Proving (FTP 2009) [Oslo, Norway, 6-7 July 2009]},
 YEAR          = {2009},
 EDITOR        = {Peltier, N. and Sofronie-Stokkermans, V.},
 PAGES         = {},
 CADDRESS      = {Oslo, Norway},
 CYEAR         = {2009},
 CMONTH        = jul # {6-7},
 YEAR          = {2009},
 URL           = {Ludwig+Hustadt@FTP2009.pdf},
 ABSTRACT = {The elimination of redundant clauses is an essential part
 of resolution-based theorem proving in order to reduce the size of
 the search space. In this paper we focus on ordered fine-grained
 resolution with selection, a sound and complete resolution-based
 calculus for monodic first-order temporal logic. The inference rules
 of the calculus are based on standard resolution between different
 types of temporal clauses on one hand and inference rules with
 semi-decidable applicability conditions that handle eventualities on
 the other hand. We define a subsumption relation on temporal clauses
 and show how the calculus can be extended with reduction rules that
 eliminate redundant clauses. We also illustrate how the subsumption
 relation can be used to simplify the loop search process for
 eventualities.}
}

The elimination of redundant clauses is an essential part of resolution-based theorem proving in order to reduce the size of the search space. In this paper we focus on ordered fine-grained resolution with selection, a sound and complete resolution-based calculus for monodic first-order temporal logic. The inference rules of the calculus are based on standard resolution between different types of temporal clauses on one hand and inference rules with semi-decidable applicability conditions that handle eventualities on the other hand. We define a subsumption relation on temporal clauses and show how the calculus can be extended with reduction rules that eliminate redundant clauses. We also illustrate how the subsumption relation can be used to simplify the loop search process for eventualities.

@INPROCEEDINGS{Ludwig+Hustadt@TIME2009,
 AUTHOR        = {Ludwig, Michel and Hustadt, Ullrich},
 TITLE         = {Resolution-Based Model Construction for {PLTL}},
 BOOKTITLE     = {Proceedings of the 16th International Symposium on
 Temporal Representation and Reasoning (TIME-2009)
 [Brixen-Bressanone, Italy, 23-25 July 2009]},
 YEAR          = {2009},
 EDITOR        = {Lutz, Carsten and Raskin, Jean-Francois},
 PAGES         = {73-80},
 PUBLISHER     = {IEEE Computer Society},
 CADDRESS      = {Brixen-Bressanone, Italy},
 CYEAR         = {2009},
 CMONTH        = jul # {23--25},
 YEAR          = {2009},
 URL           = {Ludwig+Hustadt@TIME2009.pdf},
 ABSTRACT = {The elimination of redundant clauses is an essential part
 of resolution-based theorem proving in order to reduce the size of
 the search space. In this paper we focus on ordered fine-grained
 resolution with selection, a sound and complete resolution-based
 calculus for monodic first-order temporal logic. The inference rules
 of the calculus are based on standard resolution between different
 types of temporal clauses on one hand and inference rules with
 semi-decidable applicability conditions that handle eventualities on
 the other hand. We define a subsumption relation on temporal clauses
 and show how the calculus can be extended with reduction rules that
 eliminate redundant clauses. We also illustrate how the subsumption
 relation can be used to simplify the loop search process for
 eventualities.}
}

The elimination of redundant clauses is an essential part of resolution-based theorem proving in order to reduce the size of the search space. In this paper we focus on ordered fine-grained resolution with selection, a sound and complete resolution-based calculus for monodic first-order temporal logic. The inference rules of the calculus are based on standard resolution between different types of temporal clauses on one hand and inference rules with semi-decidable applicability conditions that handle eventualities on the other hand. We define a subsumption relation on temporal clauses and show how the calculus can be extended with reduction rules that eliminate redundant clauses. We also illustrate how the subsumption relation can be used to simplify the loop search process for eventualities.

@inproceedings{Zhang+Hustadt+Dixon@CADE2009,
 author    = {Lan Zhang and Ullrich Hustadt and Clare Dixon},
 title     = {A Refined Resolution Calculus for {CTL}},
 pages     = {245-260},
 bibsource = {DBLP, http://dblp.uni-trier.de},
 editor    = {Renate A. Schmidt},
 booktitle = {Proceedings of the 22nd International Conference
              on Automated Deduction (CADE-22),
	      Montreal, Canada, August 2-7, 2009},
 publisher = {Springer},
 series    = {Lecture Notes in Computer Science},
 volume    = {5663},
 year      = {2009},
 isbn      = {978-3-642-02958-5},
 url       = {http://dx.doi.org/10.1007/978-3-642-02959-2_20},
 abstract  = {In this paper, we present a refined resolution-based
 calculus for Computation Tree Logic (CTL). The calculus requires a
 polynomial time computable transformation of an arbitrary CTL formula
 to an equi-satisfiable clausal normal form formulated in an extension
 of CTL with indexed existential path quantifiers. The calculus itself
 consists of a set of resolution rules which can be used as the basis
 for an EXPTIME decision procedure for the satisfiability problem of
 CTL. We prove soundness and completeness of the calculus. In addition,
 we introduce CTL-RP, our implementation of the calculus as well as
 some experimental results.} 
}

In this paper, we present a refined resolution-based calculus for Computation Tree Logic (CTL). The calculus requires a polynomial time computable transformation of an arbitrary CTL formula to an equi-satisfiable clausal normal form formulated in an extension of CTL with indexed existential path quantifiers. The calculus itself consists of a set of resolution rules which can be used as the basis for an EXPTIME decision procedure for the satisfiability problem of CTL. We prove soundness and completeness of the calculus. In addition, we introduce CTL-RP, our implementation of the calculus as well as some experimental results.

@article{DBLP:journals/amai/RaniseH09,
  author       = {Silvio Ranise and
                  Ullrich Hustadt},
  title        = {Preface},
  journal      = {Ann. Math. Artif. Intell.},
  volume       = {55},
  number       = {1-2},
  pages        = {1--2},
  year         = {2009},
  url          = {https://doi.org/10.1007/s10472-009-9149-2},
  doi          = {10.1007/S10472-009-9149-2},
  timestamp    = {Wed, 25 Sep 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/amai/RaniseH09.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/ZhangHD09,
  author       = {Lan Zhang and
                  Ullrich Hustadt and
                  Clare Dixon},
  editor       = {Renate A. Schmidt},
  title        = {A Refined Resolution Calculus for {CTL}},
  booktitle    = {Automated Deduction - CADE-22, 22nd International Conference on Automated
                  Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5663},
  pages        = {245--260},
  publisher    = {Springer},
  year         = {2009},
  url          = {https://doi.org/10.1007/978-3-642-02959-2\_20},
  doi          = {10.1007/978-3-642-02959-2\_20},
  timestamp    = {Sat, 19 Oct 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/ZhangHD09.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/LudwigH09,
  author       = {Michel Ludwig and
                  Ullrich Hustadt},
  editor       = {Renate A. Schmidt},
  title        = {Fair Derivations in Monodic Temporal Reasoning},
  booktitle    = {Automated Deduction - CADE-22, 22nd International Conference on Automated
                  Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5663},
  pages        = {261--276},
  publisher    = {Springer},
  year         = {2009},
  url          = {https://doi.org/10.1007/978-3-642-02959-2\_21},
  doi          = {10.1007/978-3-642-02959-2\_21},
  timestamp    = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/LudwigH09.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/ftp/LudwigH09,
  author       = {Michel Ludwig and
                  Ullrich Hustadt},
  editor       = {Nicolas Peltier and
                  Viorica Sofronie{-}Stokkermans},
  title        = {Redundancy Elimination in Monodic Temporal Reasoning},
  booktitle    = {Proceedings of the 7th International Workshop on First-Order Theorem
                  Proving, {FTP} 2009, Oslo, Norway, July 6-7, 2009},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {556},
  publisher    = {CEUR-WS.org},
  year         = {2009},
  url          = {https://ceur-ws.org/Vol-556/paper05.pdf},
  timestamp    = {Fri, 10 Mar 2023 16:23:18 +0100},
  biburl       = {https://dblp.org/rec/conf/ftp/LudwigH09.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/time/LudwigH09,
  author       = {Michel Ludwig and
                  Ullrich Hustadt},
  editor       = {Carsten Lutz and
                  Jean{-}Fran{\c{c}}ois Raskin},
  title        = {Resolution-Based Model Construction for {PLTL}},
  booktitle    = {{TIME} 2009, 16th International Symposium on Temporal Representation
                  and Reasoning, Bressanone-Brixen, Italy, 23-25 July 2009, Proceedings},
  pages        = {73--80},
  publisher    = {{IEEE} Computer Society},
  year         = {2009},
  url          = {https://doi.org/10.1109/TIME.2009.11},
  doi          = {10.1109/TIME.2009.11},
  timestamp    = {Fri, 24 Mar 2023 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/time/LudwigH09.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{Hustadt+Motik+Sattler@InfComputat2008,
 author    = {Ullrich Hustadt and
              Boris Motik and
              Ulrike Sattler},
 title     = {Deciding expressive description logics in the framework
              of resolution},
 journal   = {Information and Computation},
 volume    = {206},
 number    = {5},
 year      = {2008},
 pages     = {579-601},
 bibsource = {DBLP, http://dblp.uni-trier.de},
 url       = {http://dx.doi.org/10.1016/j.ic.2007.11.006},
 abstract  = {We present a decision procedure for the description logic
 SHIQ based on the basic superposition calculus, and show that it runs
 in exponential time for unary coding of numbers. To derive our
 algorithm, we extend basic superposition with a decomposition
 inference rule, which transforms conclusions of certain inferences
 into equivalent, but simpler clauses. This rule can be used for
 general first-order theorem proving with any resolution-based calculus
 compatible with the standard notion of redundancy.}
}

We present a decision procedure for the description logic SHIQ based on the basic superposition calculus, and show that it runs in exponential time for unary coding of numbers. To derive our algorithm, we extend basic superposition with a decomposition inference rule, which transforms conclusions of certain inferences into equivalent, but simpler clauses. This rule can be used for general first-order theorem proving with any resolution-based calculus compatible with the standard notion of redundancy.

@article{DBLP:journals/iandc/HustadtMS08,
  author       = {Ullrich Hustadt and
                  Boris Motik and
                  Ulrike Sattler},
  title        = {Deciding expressive description logics in the framework of resolution},
  journal      = {Inf. Comput.},
  volume       = {206},
  number       = {5},
  pages        = {579--601},
  year         = {2008},
  url          = {https://doi.org/10.1016/j.ic.2007.11.006},
  doi          = {10.1016/J.IC.2007.11.006},
  timestamp    = {Fri, 12 Feb 2021 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/iandc/HustadtMS08.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{Hustadt+Motik+Sattler@JAR2007,
 author    = {Ullrich Hustadt and Boris Motik and Ulrike Sattler},
 title     = {Reasoning in Description Logics by a Reduction to Disjunctive Datalog},
 journal   = {Journal of Automated Reasoning},
 volume    = {39},
 number    = {3},
 year      = {2007},
 pages     = {351-384},
 url       = {http://dx.doi.org/10.1007/s10817-007-9080-3},
 abstract  = {As applications of description logics proliferate,
 efficient reasoning with knowledge bases containing many assertions
 becomes ever more important. For such cases, we developed a novel
 reasoning algorithm that reduces a SHIQ knowledge base to a
 disjunctive datalog program while preserving the set of ground
 consequences. Queries can then be answered in the resulting program
 while reusing existing and practically proven optimization techniques
 of deductive databases, such as join-order optimizations or magic
 sets. Moreover, we use our algorithm to derive precise data complexity
 bounds: we show that SHIQ is data complete for NP, and we identify an
 expressive fragment of SHIQ with polynomial data complexity.} 
}

As applications of description logics proliferate, efficient reasoning with knowledge bases containing many assertions becomes ever more important. For such cases, we developed a novel reasoning algorithm that reduces a SHIQ knowledge base to a disjunctive datalog program while preserving the set of ground consequences. Queries can then be answered in the resulting program while reusing existing and practically proven optimization techniques of deductive databases, such as join-order optimizations or magic sets. Moreover, we use our algorithm to derive precise data complexity bounds: we show that SHIQ is data complete for NP, and we identify an expressive fragment of SHIQ with polynomial data complexity.

@article{Schmidt+Hustadt@ToCL2007,
 author    = {Schmidt, Renate A. and Hustadt, Ullrich},
 title     = {The Axiomatic Translation Principle for Modal Logic},
 journal   = {ACM Transactions on Computational Logic},
 volume    = {8},
 number    = {4},
 year      = {2007},
 pages     = {19/1-55},
 url       = {http://doi.acm.org/10.1145/1276920.1276921},
 abstract = {In this paper we present a translation principle, called
 the axiomatic translation, for reducing propositional modal logics
 with background theories, including triangular properties such as
 transitivity, Euclideanness and functionality, to decidable fragments
 of first-order logic. The goal of the axiomatic translation principle
 is to find simplified theories, which capture the inference problems
 in the original theory, but in a way that can be readily automated
 and is easier to deal with by existing (first-order) theorem provers
 than the standard translation. The principle of the axiomatic
 translation is conceptually very simple and can be almost completely
 automated. Soundness is automatic under reasonable assumptions,
 general decidability results can be stated and termination of ordered
 resolution is easily achieved. The non-trivial part of the approach
 is proving completeness. We prove results of completeness,
 decidability, model generation, the small model property and the
 interpolation property for a number of common and less common modal
 logics. We also present results of experiments with a number of
 first-order logic theorem provers which are very encouraging.}
}

In this paper we present a translation principle, called the axiomatic translation, for reducing propositional modal logics with background theories, including triangular properties such as transitivity, Euclideanness and functionality, to decidable fragments of first-order logic. The goal of the axiomatic translation principle is to find simplified theories, which capture the inference problems in the original theory, but in a way that can be readily automated and is easier to deal with by existing (first-order) theorem provers than the standard translation. The principle of the axiomatic translation is conceptually very simple and can be almost completely automated. Soundness is automatic under reasonable assumptions, general decidability results can be stated and termination of ordered resolution is easily achieved. The non-trivial part of the approach is proving completeness. We prove results of completeness, decidability, model generation, the small model property and the interpolation property for a number of common and less common modal logics. We also present results of experiments with a number of first-order logic theorem provers which are very encouraging.

@article{DBLP:journals/jar/HustadtMS07,
  author       = {Ullrich Hustadt and
                  Boris Motik and
                  Ulrike Sattler},
  title        = {Reasoning in Description Logics by a Reduction to Disjunctive Datalog},
  journal      = {J. Autom. Reason.},
  volume       = {39},
  number       = {3},
  pages        = {351--384},
  year         = {2007},
  url          = {https://doi.org/10.1007/s10817-007-9080-3},
  doi          = {10.1007/S10817-007-9080-3},
  timestamp    = {Wed, 02 Sep 2020 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/jar/HustadtMS07.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/tocl/SchmidtH07,
  author       = {Renate A. Schmidt and
                  Ullrich Hustadt},
  title        = {The axiomatic translation principle for modal logic},
  journal      = {{ACM} Trans. Comput. Log.},
  volume       = {8},
  number       = {4},
  pages        = {19},
  year         = {2007},
  url          = {https://doi.org/10.1145/1276920.1276921},
  doi          = {10.1145/1276920.1276921},
  timestamp    = {Wed, 25 Sep 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/tocl/SchmidtH07.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@incollection{DBLP:books/el/07/HorrocksHSS07,
  author       = {Ian Horrocks and
                  Ullrich Hustadt and
                  Ulrike Sattler and
                  Renate A. Schmidt},
  editor       = {Patrick Blackburn and
                  J. F. A. K. van Benthem and
                  Frank Wolter},
  title        = {Computational modal logic},
  booktitle    = {Handbook of Modal Logic},
  series       = {Studies in logic and practical reasoning},
  volume       = {3},
  pages        = {181--245},
  publisher    = {North-Holland},
  year         = {2007},
  url          = {https://doi.org/10.1016/s1570-2464(07)80007-3},
  doi          = {10.1016/S1570-2464(07)80007-3},
  timestamp    = {Tue, 12 Apr 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/books/el/07/HorrocksHSS07.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@INPROCEEDINGS{Hustadt+Tishkovsky+Wolter+Zakharyaschev@JELIA2006,
 AUTHOR        = {Hustadt, U. and Tishkovsky, D. and Wolter, F. and Zakharyaschev, M.},
 TITLE         = {Automated reasoning about metric and topology},
 BOOKTITLE     = {Proceedings of the 10th European Conference on Logics in Artificial Intelligence (JELIA 2006) [Liverpool, UK, 13-15 September 2006]},
 YEAR          = {2006},
 EDITOR        = {Fisher, M. and van der Hoek, Wiebe and Konev, B. and Lisitsa, A.},
 PAGES         = {490-493},
 PUBLISHER     = {Springer},
 CADDRESS      = {Liverpool, UK},
 CYEAR         = {2006},
 CMONTH        = sep # {~13-15},
 SERIES        = {LNAI},
 VOLUME        = {4160},
 URL           = {http://dx.doi.org/10.1007/11853886_44},
 ABSTRACT = {In this paper we compare two approaches to automated
 reasoning about metric and topology in the framework of the logic MT
 introduced in [10].  MT-formulas are built from set variables
 p1,p2,... (for arbitrary subsets of a metric space) using the Booleans
 conjunction, disjunction, implication, and negation, distance
 operators, and topological interior and closure operators I and C.}
}

In this paper we compare two approaches to automated reasoning about metric and topology in the framework of the logic MT introduced in [10]. MT-formulas are built from set variables p1,p2,... (for arbitrary subsets of a metric space) using the Booleans conjunction, disjunction, implication, and negation, distance operators, and topological interior and closure operators I and C.

@inproceedings{DBLP:conf/jelia/HustadtTWZ06,
  author       = {Ullrich Hustadt and
                  Dmitry Tishkovsky and
                  Frank Wolter and
                  Michael Zakharyaschev},
  editor       = {Michael Fisher and
                  Wiebe van der Hoek and
                  Boris Konev and
                  Alexei Lisitsa},
  title        = {Automated Reasoning About Metric and Topology},
  booktitle    = {Logics in Artificial Intelligence, 10th European Conference, {JELIA}
                  2006, Liverpool, UK, September 13-15, 2006, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {4160},
  pages        = {490--493},
  publisher    = {Springer},
  year         = {2006},
  url          = {https://doi.org/10.1007/11853886\_44},
  doi          = {10.1007/11853886\_44},
  timestamp    = {Sun, 06 Oct 2024 21:10:23 +0200},
  biburl       = {https://dblp.org/rec/conf/jelia/HustadtTWZ06.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@ARTICLE{Fernandez-Gago+Hustadt+Dixon+Fisher+Konev@JAR2005,
 AUTHOR        = {M. C. Fern{\'a}ndez-Gago and U. Hustadt and C. Dixon 
 and M. Fisher and B. Konev},
 TITLE         = {First-Order Temporal Verification in Practice},
 JOURNAL       = {Journal of Automated Reasoning},
 YEAR          = {2005},
 VOLUME        = {34},
 NUMBER        = {3},
 PAGES         = {295-321},
 MONTH         = apr,
 URL           = {http://dx.doi.org/10.1007/s10817-005-7354-1},
 ABSTRACT      = {First-order temporal logic, the extension 
 of first-order logic with operators dealing with time, is a 
 powerful and expressive formalism with many potential 
 applications. This expressive logic can be viewed as a 
 framework in which to investigate problems specified in 
 other logics. The monodic fragment of first-order temporal 
 logic is a useful fragment that possesses good computational 
 properties such as completeness and sometimes even decidability. 
 Temporal logics of knowledge are useful for dealing with situations 
 where the knowledge of agents in a system is involved. In this 
 paper we present a translation from temporal logics of knowledge 
 into the monodic fragment of first-order temporal logic. We can 
 then use a theorem prover for monodic first-order temporal logic 
 to prove properties of the translated formulas. This allows problems 
 specified in temporal logics of knowledge to be verified automatically 
 without needing a specialized theorem prover for temporal logics of 
 knowledge. We present the translation, its correctness, and examples 
 of its use.}
}

First-order temporal logic, the extension of first-order logic with operators dealing with time, is a powerful and expressive formalism with many potential applications. This expressive logic can be viewed as a framework in which to investigate problems specified in other logics. The monodic fragment of first-order temporal logic is a useful fragment that possesses good computational properties such as completeness and sometimes even decidability. Temporal logics of knowledge are useful for dealing with situations where the knowledge of agents in a system is involved. In this paper we present a translation from temporal logics of knowledge into the monodic fragment of first-order temporal logic. We can then use a theorem prover for monodic first-order temporal logic to prove properties of the translated formulas. This allows problems specified in temporal logics of knowledge to be verified automatically without needing a specialized theorem prover for temporal logics of knowledge. We present the translation, its correctness, and examples of its use.

@INPROCEEDINGS{Hustadt+Konev+Schmidt@CADE2005,
 AUTHOR        = {Ullrich Hustadt and Boris Konev and Renate A. Schmidt},
 TITLE         = {Deciding Monodic Fragments by Temporal Resolution},
 BOOKTITLE     = {Proceedings of the 20th International Conference on
 Automated Deduction (CADE-20) [Tallin, Estonia, 22-27 July 2005]},
 YEAR          = {2005},
 EDITOR        = {Robert Nieuwenhuis},
 PAGES         = {204-218},
 PUBLISHER     = {Springer},
 PYEAR         = {2005},
 CADDRESS      = {Tallinn, Estonia},
 CYEAR         = {2005},
 CMONTH        = jul # {~22-27},
 SERIES        = {LNAI},
 VOLUME        = {3632},
 URL           = {http://www.csc.liv.ac.uk/~ullrich/publications/Hustadt+Konev+Schmidt@CADE2005.pdf},
 URL           = {http://dx.doi.org/10.1007/11532231_15},
 ABSTRACT      = {In this paper we study the decidability of various
 fragments of monodic first-order temporal logic by temporal
 resolution. We focus on two resolution calculi, namely, monodic
 temporal resolution and fine-grained temporal resolution.
 For the first, we state a very general decidability result, which is
 independent of the particular decision procedure used to decide the
 first-order part of the logic.
 <p>
 For the second, we introduce refinements using orderings and selection
 functions. This allows us to transfer existing results on decidability by
 resolution for first-order fragments to monodic first-order temporal
 logic and obtain new decision procedures.
 </p>
 The latter is of immediate practical value, due to the
 availability of <a href="http://www.csc.liv.ac.uk/~konev/TeMP/">TeMP</a>, 
 an implementation of fine-grained temporal resolution.}
}

In this paper we study the decidability of various fragments of monodic first-order temporal logic by temporal resolution. We focus on two resolution calculi, namely, monodic temporal resolution and fine-grained temporal resolution. For the first, we state a very general decidability result, which is independent of the particular decision procedure used to decide the first-order part of the logic.

For the second, we introduce refinements using orderings and selection functions. This allows us to transfer existing results on decidability by resolution for first-order fragments to monodic first-order temporal logic and obtain new decision procedures.

The latter is of immediate practical value, due to the availability of TeMP, an implementation of fine-grained temporal resolution.

@INPROCEEDINGS{Hustadt+Motik@DL2005,
 AUTHOR        = {Hustadt, Ullrich and Motik, Boris},
 TITLE         = {Description Logics and Disjunctive Datalog --- The Story so Far},
 BOOKTITLE     = {Proceedings of the 2005 International Workshop on Description Logics (DL2005)
 [Edinburgh, Scotland, 26-28 July 2005]},
 EDITOR        = {Ian Horrocks and Ulrike Sattler and Frank Wolter},
 CADDRESS      = {Edinburgh, Scotland, UK},
 CYEAR         = {2005},
 YEAR          = {2005},
 CMONTH        = jul # {~26--28},
 SERIES        = {CEUR Workshop Proceedings},
 VOLUME        = {189},
 URL           = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-147/31-MotikHustadt.pdf},
 ABSTRACT      = {In this paper we present an overview of our recent work on the relationship
 between description logics and disjunctive datalog. In particular,
 we reduce satisfiability and instance checking in SHIQ to corresponding
 problems in disjunctive datalog. This allows us to apply practically successful
 deductive database optimization techniques, such as magic sets.
 Interestingly, the reduction also allows us to obtain novel theoretical results
 on description logics. In particular, we show that the <em>data complexity</em>
 of reasoning in SHIQ is in NP, and we define a fragment called
 Horn-SHIQ for which the data complexity is in P. Finally, the reduction
 provides a basis for query answering in an extension of SHIQ with
 so-called <em>DL-safe rules</em>.}
}

In this paper we present an overview of our recent work on the relationship between description logics and disjunctive datalog. In particular, we reduce satisfiability and instance checking in SHIQ to corresponding problems in disjunctive datalog. This allows us to apply practically successful deductive database optimization techniques, such as magic sets. Interestingly, the reduction also allows us to obtain novel theoretical results on description logics. In particular, we show that the data complexity of reasoning in SHIQ is in NP, and we define a fragment called Horn-SHIQ for which the data complexity is in P. Finally, the reduction provides a basis for query answering in an extension of SHIQ with so-called DL-safe rules.

@INPROCEEDINGS{Hustadt+Motik+Sattler@IJCAI2005,
 AUTHOR        = {Hustadt, Ullrich and Motik, Boris and Sattler, Ulrike},
 TITLE         = {Data Complexity of Reasoning in Very Expressive 
 Description Logics},
 BOOKTITLE     = {Proceedings of the Nineteenth International 
 Joint Conference on Artificial Intelligence (IJCAI 2005)
 [Edinburg, Scotland, 30 July - 5 August 2005]},
 YEAR          = {2005},
 PAGES         = {466-471},
 PUBLISHER     = {International Joint Conferences on
 Artificial Intelligence},
 CADDRESS      = {Edinburgh, Scotland},
 CYEAR         = {2005},
 CMONTH        = jul # {~30--} # aug # {~5},
 URL           = {http://www.ijcai.org/papers/0326.pdf},
 ABSTRACT      = {<em>Data complexity</em> of reasoning in description logics
 (DLs) estimates the performance of reasoning algorithms
 measured in the size of the ABox only.
 We show that, even for the very expressive DL
 SHIQ, satisfiability checking is data complete for
 NP. For applications with large ABoxes, this can
 be a more accurate estimate than the usually considered
 combined complexity, which is EXPTIMEcomplete.
 Furthermore, we identify an expressive
 fragment, Horn-SHIQ, which is data complete for P, 
 thus being very appealing for practical usage.}
}

Data complexity of reasoning in description logics (DLs) estimates the performance of reasoning algorithms measured in the size of the ABox only. We show that, even for the very expressive DL SHIQ, satisfiability checking is data complete for NP. For applications with large ABoxes, this can be a more accurate estimate than the usually considered combined complexity, which is EXPTIMEcomplete. Furthermore, we identify an expressive fragment, Horn-SHIQ, which is data complete for P, thus being very appealing for practical usage.

@INPROCEEDINGS{Hustadt+Motik+Sattler@LPAR2004,
 AUTHOR        = {Hustadt, U. and Motik, B. and Sattler, U.},
 TITLE         = {A Decomposition Rule for Decision Procedures by Resolution-Based Calculi},
 BOOKTITLE     = {Proceedings of the 11th International Conference on 
 Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2004)
 [Montevideo, Uruguay, 14-18 March 2005)},
 EDITOR        = {Baader, F. and Voronkov, A.},
 PUBLISHER     = {Springer},
 CMONTH        = mar # {~14--18},
 CYEAR         = {2005},
 YEAR          = {2005},
 PAGES         = {21-35},
 URL           = {http://dx.doi.org/10.1007/978-3-540-32275-7_2},
 ABSTRACT      = {Resolution-based calculi are among the most widely used calculi 
 for theorem proving in first-order logic. Numerous refinements 
 of resolution are nowadays available, such as e.g. basic superposition, 
 a calculus highly optimized for theorem proving with equality. However, 
 even such an advanced calculus does not restrict inferences enough to 
 obtain decision procedures for complex logics, such as SHIQ. 
 In this paper, we present a new decomposition inference rule, 
 which can be combined with any resolution-based calculus compatible 
 with the standard notion of redundancy. We combine decomposition with 
 basic superposition to obtain three new decision procedures: 
 (i) for the description logic SHIQ, (ii) for the description logic ALCHIQb, 
 and (iii) for answering conjunctive queries over SHIQ knowledge bases. 
 The first two procedures are worst-case optimal and, based on the 
 vast experience in building efficient theorem provers, we expect them 
 to be suitable for practical usage.}
}

Resolution-based calculi are among the most widely used calculi for theorem proving in first-order logic. Numerous refinements of resolution are nowadays available, such as e.g. basic superposition, a calculus highly optimized for theorem proving with equality. However, even such an advanced calculus does not restrict inferences enough to obtain decision procedures for complex logics, such as SHIQ. In this paper, we present a new decomposition inference rule, which can be combined with any resolution-based calculus compatible with the standard notion of redundancy. We combine decomposition with basic superposition to obtain three new decision procedures: (i) for the description logic SHIQ, (ii) for the description logic ALCHIQb, and (iii) for answering conjunctive queries over SHIQ knowledge bases. The first two procedures are worst-case optimal and, based on the vast experience in building efficient theorem provers, we expect them to be suitable for practical usage.

@ARTICLE{Konev+Degtyarev+Dixon+Fisher+Hustadt@InfComputat2005,
 AUTHOR        = {Boris Konev and Anatoli Degtyarev and Clare Dixon and Michael Fisher and Ullrich Hustadt},
 TITLE         = {Mechanising first-order temporal resolution},
 JOURNAL       = {Information and Computation},
 YEAR          = {2005},
 VOLUME        = {199},
 NUMBER        = {1-2},
 PAGES         = {55-86},
 URL           = {http://dx.doi.org/10.1016/j.ic.2004.10.005},
 ABSTRACT = {First-order temporal logic is a concise and powerful
 notation, with many potential applications in both Computer Science
 and Artificial Intelligence. While the full logic is highly complex,
 recent work on monodic first-order temporal logics has identified
 important enumerable and even decidable fragments. Although a
 complete and correct resolution-style calculus has already been
 suggested for this specific fragment, this calculus involves
 constructions too complex to be of practical value. In this paper, we
 develop a machine-oriented clausal resolution method which features
 radically simplified proof search. We first define a normal form for
 monodic formulae and then introduce a novel resolution calculus that
 can be applied to formulae in this normal form. By careful encoding,
 parts of the calculus can be implemented using classical first-order
 resolution and can, thus, be efficiently implemented. We prove
 correctness and completeness results for the calculus and illustrate
 it on a comprehensive example. An implementation of the method is
 briefly discussed.}
}
  

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. Although a complete and correct resolution-style calculus has already been suggested for this specific fragment, this calculus involves constructions too complex to be of practical value. In this paper, we develop a machine-oriented clausal resolution method which features radically simplified proof search. We first define a normal form for monodic formulae and then introduce a novel resolution calculus that can be applied to formulae in this normal form. By careful encoding, parts of the calculus can be implemented using classical first-order resolution and can, thus, be efficiently implemented. We prove correctness and completeness results for the calculus and illustrate it on a comprehensive example. An implementation of the method is briefly discussed.

@article{DBLP:journals/iandc/KonevDDFH05,
  author       = {Boris Konev and
                  Anatoli Degtyarev and
                  Clare Dixon and
                  Michael Fisher and
                  Ullrich Hustadt},
  title        = {Mechanising first-order temporal resolution},
  journal      = {Inf. Comput.},
  volume       = {199},
  number       = {1-2},
  pages        = {55--86},
  year         = {2005},
  url          = {https://doi.org/10.1016/j.ic.2004.10.005},
  doi          = {10.1016/J.IC.2004.10.005},
  timestamp    = {Sun, 06 Oct 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/iandc/KonevDDFH05.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jar/Fernandez-GagoHDFK05,
  author       = {M. Carmen Fern{\'{a}}ndez Gago and
                  Ullrich Hustadt and
                  Clare Dixon and
                  Michael Fisher and
                  Boris Konev},
  title        = {First-Order Temporal Verification in Practice},
  journal      = {J. Autom. Reason.},
  volume       = {34},
  number       = {3},
  pages        = {295--321},
  year         = {2005},
  url          = {https://doi.org/10.1007/s10817-005-7354-1},
  doi          = {10.1007/S10817-005-7354-1},
  timestamp    = {Sun, 06 Oct 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/jar/Fernandez-GagoHDFK05.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/HustadtKS05,
  author       = {Ullrich Hustadt and
                  Boris Konev and
                  Renate A. Schmidt},
  editor       = {Robert Nieuwenhuis},
  title        = {Deciding Monodic Fragments by Temporal Resolution},
  booktitle    = {Automated Deduction - CADE-20, 20th International Conference on Automated
                  Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {3632},
  pages        = {204--218},
  publisher    = {Springer},
  year         = {2005},
  url          = {https://doi.org/10.1007/11532231\_15},
  doi          = {10.1007/11532231\_15},
  timestamp    = {Sun, 06 Oct 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/HustadtKS05.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/dlog/HustadtM05,
  author       = {Ullrich Hustadt and
                  Boris Motik},
  editor       = {Ian Horrocks and
                  Ulrike Sattler and
                  Frank Wolter},
  title        = {Description Logics and Disjunctive Datalog - The Story so Far},
  booktitle    = {Proceedings of the 2005 International Workshop on Description Logics
                  (DL2005), Edinburgh, Scotland, UK, July 26-28, 2005},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {147},
  publisher    = {CEUR-WS.org},
  year         = {2005},
  url          = {https://ceur-ws.org/Vol-147/31-MotikHustadt.pdf},
  timestamp    = {Fri, 10 Mar 2023 16:23:17 +0100},
  biburl       = {https://dblp.org/rec/conf/dlog/HustadtM05.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/ijcai/HustadtMS05,
  author       = {Ullrich Hustadt and
                  Boris Motik and
                  Ulrike Sattler},
  editor       = {Leslie Pack Kaelbling and
                  Alessandro Saffiotti},
  title        = {Data Complexity of Reasoning in Very Expressive Description Logics},
  booktitle    = {IJCAI-05, Proceedings of the Nineteenth International Joint Conference
                  on Artificial Intelligence, Edinburgh, Scotland, UK, July 30 - August
                  5, 2005},
  pages        = {466--471},
  publisher    = {Professional Book Center},
  year         = {2005},
  url          = {http://ijcai.org/Proceedings/05/Papers/0326.pdf},
  timestamp    = {Tue, 20 Aug 2019 16:16:29 +0200},
  biburl       = {https://dblp.org/rec/conf/ijcai/HustadtMS05.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@INPROCEEDINGS{Goranko+Hustadt+Schmidt+Vakarelov@RSRelMiCSIWAKA2003,
 AUTHOR        = {Goranko, Valentin and Hustadt, Ullrich and 
 Schmidt, Renate and Vakarelov, Dimiter},
 TITLE         = {{SCAN} is complete for all Sahlqvist formulae},
 BOOKTITLE     = {Revised Selected Papers of the 7th International 
 Seminar on Relational Methods in Computer Science and the
 2nd International Workshop on Kleene Algebra
 [Bad Malente, Germany, 12-17 May 2003]},
 EDITOR        = {Berghammer, Rudolf and M{\"o}ller, Bernhard
 and Struth, Georg},
 PAGES         = {149-162},
 PUBLISHER     = {Springer},
 ADDRESS       = {},
 PADDRESS      = {Berlin},
 PYEAR         = {2004},
 YEAR          = {2004},
 CADDRESS      = {Bad Malente, Germany},
 CYEAR         = {2003},
 CMONTH        = may # {~12-17},
 SERIES        = {LNCS},
 VOLUME        = {3051},
 URL           = {Goranko+Hustadt+Schmidt+Vakarelov@RSRelMiCSIWAKA2003.pdf},
 ABSTRACT      = {SCAN is an algorithm for reducing existential
 second-order logic formulae to equivalent simpler formulae, often
 first-order logic formulae.  It is provably impossible for such a
 reduction to first-order logic to be successful for every second-order
 logic formula which has an equivalent first-order formula.  In this
 paper we show that SCAN successfully computes the first-order
 equivalents of all Sahlqvist formulae in the classical (multi-)modal
 language.}
}

SCAN is an algorithm for reducing existential second-order logic formulae to equivalent simpler formulae, often first-order logic formulae. It is provably impossible for such a reduction to first-order logic to be successful for every second-order logic formula which has an equivalent first-order formula. In this paper we show that SCAN successfully computes the first-order equivalents of all Sahlqvist formulae in the classical (multi-)modal language.

@INCOLLECTION{HK2004,
 AUTHOR        = {Hustadt, Ullrich and Konev, Boris},
 TITLE         = {{TRP++}: A temporal resolution prover},
 BOOKTITLE     = {Collegium Logicum},
 PUBLISHER     = {Kurt G{\"o}del Society},
 YEAR          = {2004},
 EDITOR        = {Baaz, Matthias and Makowsky, Johann and Voronkov, Andrei},
 PAGES         = {65-79},
 URL           = {http://www.csc.liv.ac.uk/~ullrich/publications/HK_KGS.pdf},
 ABSTRACT      = {Temporal logics are extensions of classical logic with
 operators that deal with time. They have been used in a wide variety
 of areas within Computer Science and Artificial Intelligence, for
 example robotics, databases, hardware verification and agent-based
 systems. 
 <p>
 In particular, propositional temporal logics have been
 applied to (i) the specification and verification of reactive
 (e.g. distributed or concurrent) systems; (ii) the synthesis of
 programs from temporal specifications;; (iii) the semantics of
 executable temporal logic; (iv) algorithmic verification via
 model-checking; and (v) knowledge representation and reasoning.
 </p>
 <p>
 In developing these techniques, temporal proof is often required, and
 we base our work on practical proof techniques for the clausal
 resolution method for propositional linear-time temporal logic
 PLTL. The method is based on an intuitive clausal form, called SNF,
 comprising three main clause types and a small number of resolution
 rules.
 </p>
 While the approach has been shown to be competitive using
 a prototype implementation of the method, we now aim at an even more
 efficient implementation. This implementation, called TRP++, is the
 focus of this paper.}
}

Temporal logics are extensions of classical logic with operators that deal with time. They have been used in a wide variety of areas within Computer Science and Artificial Intelligence, for example robotics, databases, hardware verification and agent-based systems.

In particular, propositional temporal logics have been applied to (i) the specification and verification of reactive (e.g. distributed or concurrent) systems; (ii) the synthesis of programs from temporal specifications;; (iii) the semantics of executable temporal logic; (iv) algorithmic verification via model-checking; and (v) knowledge representation and reasoning.

In developing these techniques, temporal proof is often required, and we base our work on practical proof techniques for the clausal resolution method for propositional linear-time temporal logic PLTL. The method is based on an intuitive clausal form, called SNF, comprising three main clause types and a small number of resolution rules.

While the approach has been shown to be competitive using a prototype implementation of the method, we now aim at an even more efficient implementation. This implementation, called TRP++, is the focus of this paper.

@INPROCEEDINGS{Hustadt+Konev+Riazanov+Voronkov@IJCAR2004,
 AUTHOR        = {Hustadt, Ullrich and Konev, Boris and Riazanov, Alexandre and Voronkov, Andrei},
 TITLE         = {TeMP: A Temporal Monodic Prover},
 PAGES         = {326-330},
 EDITOR        = {Basin, David A. and Rusinowitch, Micha{\"e}l},
 BOOKTITLE     = {Proceedings of the Second International Joint Conference on Automated Reasoning (IJCAR 2004) [Cork, Ireland, 4-8 July 2004]}, 
 CADDRESS      = {Cork, Ireland},
 CMONTH        = jul # {4--8}, 
 CYEAR         = {2004},
 PUBLISHER     = {Springer},
 SERIES        = {LNAI},
 VOLUME        = {3097},
 YEAR          = {2004},
 ISBN          = {3-540-22345-2},
 URL           = {Hustadt+Konev+Riazanov+Voronkov@IJCAR2004.pdf},
 ABSTRACT      = {In this paper we describe TeMP, the first automatic
 theorem prover for the monodic fragment of FOTL.}
}

In this paper we describe TeMP, the first automatic theorem prover for the monodic fragment of FOTL.

@TECHREPORT{Hustadt+Konev+Riazanov+Voronkov@ULCS-TR2004,
 AUTHOR        = {U. Hustadt and B. Konev and A. Riazanov and A. Voronkov},
 TITLE         = {TeMP: A Temporal Monodic Prover},
 INSTITUTION   = {Department of Computer Science, University of Liverpool},
 YEAR          = {2004},
 TYPE          = {Technical Report},
 NUMBER        = {ULCS-04-004},
 ADDRESS       = {Liverpool, UK},
 URL           = {http://www.csc.liv.ac.uk/research/techreports/tr2004/ulcs-04-004.ps},
 ABSTRACT      = {In this paper we describe TeMP, the first automatic
 theorem prover for the monodic fragment of FOTL.}
}

In this paper we describe TeMP, the first automatic theorem prover for the monodic fragment of FOTL.

@INPROCEEDINGS{Hustadt+Motik+Sattler@ECAI2004,
 AUTHOR        = {U. Hustadt and B. Motik and U. Sattler},
 TITLE         = {Reasoning in Description Logics with a 
 Concrete Domain in the Framework of Resolution},
 BOOKTITLE     = {Proceedings of the 16th European Conference 
 on Artificial Intelligence (ECAI 2004)},
 EDITOR        = {R. L\'{o}pez de M\'{a}ntaras and L. Saitta},
 CADDRESS      = {Valencia, Spain},
 CMONTH        = aug # {~22--27},
 CYEAR         = {2004},
 YEAR          = {2004},  
 PAGES         = {353-357},
 PUBLISHER     = {IOS Press},
 PYEAR         = {2004},
 URL           = {Hustadt+Motik+Sattler@ECAI2004.pdf},
 ABSTRACT = {In description logics, concrete domains are used to model
 concrete properties such as weight, name, or age, having concrete
 values such as integers or strings, with built-in predicates, such as
 <= or =. Until now, reasoning with concrete domains has been studied
 predominantly in the context of tableaux and automata calculi.  In
 this paper, we present a general approach for concrete domain
 reasoning in the resolution framework. We apply this approach to
 devise an optimal decision procedure for SHIQ(D), the extension of
 SHIQ with a restricted form of concrete domains, serving as the
 logical underpinning of the web ontology language OWL-DL.}
}

In description logics, concrete domains are used to model concrete properties such as weight, name, or age, having concrete values such as integers or strings, with built-in predicates, such as <= or =. Until now, reasoning with concrete domains has been studied predominantly in the context of tableaux and automata calculi. In this paper, we present a general approach for concrete domain reasoning in the resolution framework. We apply this approach to devise an optimal decision procedure for SHIQ(D), the extension of SHIQ with a restricted form of concrete domains, serving as the logical underpinning of the web ontology language OWL-DL.

@TECHREPORT{Hustadt+Motik+Sattler@FZI-TR2004,
 AUTHOR        = {Hustadt, U. and Motik, B. and Sattler, U.},
 TITLE         = {Reasoning for Description Logics around SHIQ in a Resolution Framework},
 XTITLE        = {Reasoning for Description Logics around {$\mathcal{SHIQ}$} in a Resolution Framework},
 INSTITUTION   = {FZI},
 ADDRESS       = {Karlsruhe, Germany},
 NUMBER        = {3-8-04/04},
 MONTH         = jun,
 YEAR          = {2004},
 URL           = {FZI-3-8-04-04.pdf},
 ABSTRACT      = {We present several algorithms for reasoning with
 description logics closely related to SHIQ. Firstly, we present an
 algorithm for deciding satisfiability of SHIQ knowl edge bases. Then,
 to enable representing concrete data such as strings or integers, we
 devise a general approach for reasoning with concrete domains in the
 framework of resolution, and apply it to obtain a procedure for
 deciding SHIQ(D). For unary coding of numbers, this procedure is
 worst-case optimal, i.e. it runs in exponential time. Motivated by the
 prospects of reusing optimization techniques from deductive databases,
 such as magic sets, we devise an algorithm for reducing SHIQ(D)
 knowledge bases to disjunctive datalog programs. Furthermore, we show
 that so-called DL-safe rules can be combined with disjunctive programs
 obtained by our transformation to increase the expressivity of the
 logic, without affecting decidability. We show that our algorithms can
 easily be extended to handle answering conjunctive queries over
 SHIQ(D) knowledge bases. Finally, we extend our algorithms to support
 metamodel- ing. Since SHIQ(D) is closely related to OWL-DL, our
 algorithms provide alternative mechanisms for reasoning in the
 Semantic Web.}
}

We present several algorithms for reasoning with description logics closely related to SHIQ. Firstly, we present an algorithm for deciding satisfiability of SHIQ knowl edge bases. Then, to enable representing concrete data such as strings or integers, we devise a general approach for reasoning with concrete domains in the framework of resolution, and apply it to obtain a procedure for deciding SHIQ(D). For unary coding of numbers, this procedure is worst-case optimal, i.e. it runs in exponential time. Motivated by the prospects of reusing optimization techniques from deductive databases, such as magic sets, we devise an algorithm for reducing SHIQ(D) knowledge bases to disjunctive datalog programs. Furthermore, we show that so-called DL-safe rules can be combined with disjunctive programs obtained by our transformation to increase the expressivity of the logic, without affecting decidability. We show that our algorithms can easily be extended to handle answering conjunctive queries over SHIQ(D) knowledge bases. Finally, we extend our algorithms to support metamodel- ing. Since SHIQ(D) is closely related to OWL-DL, our algorithms provide alternative mechanisms for reasoning in the Semantic Web.

@INPROCEEDINGS{Hustadt+Motik+Sattler@KR2004,
 AUTHOR        = {Hustadt, U. and Motik, B. and Sattler, U.},
 TITLE         = {Reducing SHIQ- Description Logic to Disjunctive Datalog Programs},
 XTITLE        = {Reducing {$\mathcal{SHIQ}^-$} Description Logic to Disjunctive Datalog Programs},
 BOOKTITLE     = {Proceedings of the 9th International Conference 
 on Knowledge Representation and Reasoning (KR2004) [Whistler, Canada, June 2-5, 2004]},
 EDITOR        = {Dubois, D. and Welty, C. and Williams, Mary-Anne},
 PUBLISHER     = {AAAI Press},
 PADDRESS      = {Menlo Park, California, USA},
 PYEAR         = {2004},
 CADDRESS      = {Whistler, Canada},
 CMONTH        = jun # {~2-5},
 CYEAR         = {2004},
 YEAR          = {2004},
 PAGES         = {152-162},
 URL           = {http://www.aaai.org/Library/KR/2004/kr04-018.php},
 URL           = {Hustadt+Motik+Sattler@KR2004.pdf},
 ABSTRACT = {As applications of description logics proliferate,
 efficient reasoning with large ABoxes (sets of individuals with
 descriptions) becomes ever more important. Motivated by the prospects
 of reusing optimization techniques from deductive databases, in this
 paper, we present a novel approach to checking consistency of ABoxes,
 instance checking and query answering, w.r.t. ontologies formulated
 using a slight restriction of the description logic SHIQ. Our approach
 proceeds in three steps: (i) the ontology is translated into
 first-order clauses, (ii) TBox and RBox clauses are saturated using a
 resolution-based decision procedure, and (iii) the saturated set of
 clauses is translated into a disjunctive datalog program. Thus, query
 answering can be performed using the resulting program, while applying
 all existing optimization techniques, such as join-order optimizations
 or magic sets. Equally important, the resolution-based decision
 procedure we present is for unary coding of numbers worst-case
 optimal, i.e.  it runs in ExpTime.}
}

As applications of description logics proliferate, efficient reasoning with large ABoxes (sets of individuals with descriptions) becomes ever more important. Motivated by the prospects of reusing optimization techniques from deductive databases, in this paper, we present a novel approach to checking consistency of ABoxes, instance checking and query answering, w.r.t. ontologies formulated using a slight restriction of the description logic SHIQ. Our approach proceeds in three steps: (i) the ontology is translated into first-order clauses, (ii) TBox and RBox clauses are saturated using a resolution-based decision procedure, and (iii) the saturated set of clauses is translated into a disjunctive datalog program. Thus, query answering can be performed using the resulting program, while applying all existing optimization techniques, such as join-order optimizations or magic sets. Equally important, the resolution-based decision procedure we present is for unary coding of numbers worst-case optimal, i.e. it runs in ExpTime.

@article{Hustadt+Schmidt+Georgieva@JoRMiCS2004,
 author    = {U. Hustadt and R. A. Schmidt and L. Georgieva},
 title     = {A Survey of Decidable First-Order Fragments and Description Logics},
 journal   = {JoRMiCS},
 volume    = {1},
 pages     = {251-276},
 year      = {2004},
 url       = {http://www.cosc.brocku.ca/Faculty/Winter/JoRMiCS/Vol1/PDF/v1n11.pdf},
 abstract  = {The guarded fragment and its extensions and subfragments
 are often considered as a framework for investigating the properties
 of description logics. There are also other, some less well-known,
 decidable fragments of first-order logic which all have in common that
 they generalise the standard translation of ALC to first-order logic. We
 provide a short survey of some of these fragments and motivate why
 they are interesting with respect to description logics, mentioning
 also connections to other non-classical logics.} 
}

The guarded fragment and its extensions and subfragments are often considered as a framework for investigating the properties of description logics. There are also other, some less well-known, decidable fragments of first-order logic which all have in common that they generalise the standard translation of ALC to first-order logic. We provide a short survey of some of these fragments and motivate why they are interesting with respect to description logics, mentioning also connections to other non-classical logics.

@INPROCEEDINGS{Schmidt+Orlowska+Hustadt@RSRelMiCSIWAKA2003,
 AUTHOR        = {Schmidt, Renate A. and Or{\l}owska, Ewa and 
 Hustadt, Ullrich},
 TITLE         = {Two proof systems for {Peirce} algebras},
 BOOKTITLE     = {Revised Selected Papers of the 7th International 
 Seminar on Relational Methods in Computer Science and the
 2nd International Workshop on Kleene Algebra},
 YEAR          = {2004},
 EDITOR        = {Berghammer, Rudolf and M{\"o}ller, Bernhard
 and Struth, Georg},
 PAGES         = {238-251},
 PUBLISHER     = {Springer},
 ADDRESS       = {},
 PADDRESS      = {Berlin},
 PYEAR         = {2004},
 CADDRESS      = {Bad Malente, Germany},
 CYEAR         = {2003},
 CMONTH        = may # {~12--17},
 SERIES        = {LNCS},
 VOLUME        = {3051},
 URL           = {Schmidt+Orlowska+Hustadt@RSRelMiCSIWAKA2003.pdf},
 ABSTRACT      = {This paper develops and compares two tableaux-style
 proof systems for Peirce algebras. One is a tableau refutation proof
 system, the other is a proof system in the style of Rasiowa-Sikorski.}
}

This paper develops and compares two tableaux-style proof systems for Peirce algebras. One is a tableau refutation proof system, the other is a proof system in the style of Rasiowa-Sikorski.

@ARTICLE{Schmidt+Tishkovsky+Hustadt@SL2004,
 AUTHOR        = {Schmidt, Renate A. and Tishkovsky, Dmitry and
 Hustadt, Ullrich},
 TITLE         = {Interactions between Knowledge, Action,
 and Commitment within Agent Dynamic Logic},
 JOURNAL       = {Studia Logica},
 YEAR          = {2004},
 VOLUME        = {78},
 NUMBER        = {3},
 PAGES         = {381-415},
 MONTH         = dec,
 URL           = {http://dx.doi.org/10.1007/s11225-004-6042-1},
 ABSTRACT      = {This paper considers a new class of agent dynamic
 logics which provide a formal means of specifying and reasoning about
 the agents' activities and informational, motivational and proactical
 aspects of the behaviour of the agents. We present a Hilbert-style
 deductive system for a basic agent dynamic logic and consider a number
 of extensions of this logic with axiom schemata formalising
 interactions between knowledge and commitment (expressing an agent's
 awareness of her commitments), and interactions between knowledge and
 actions (expressing no learning and persistence of knowledge about
 actions). The deductive systems are proved sound and complete with
 respect to a Kripke-style semantics. Each of the consdered logics is
 shown to have the small model property and therefore decidable.}
}

This paper considers a new class of agent dynamic logics which provide a formal means of specifying and reasoning about the agents' activities and informational, motivational and proactical aspects of the behaviour of the agents. We present a Hilbert-style deductive system for a basic agent dynamic logic and consider a number of extensions of this logic with axiom schemata formalising interactions between knowledge and commitment (expressing an agent's awareness of her commitments), and interactions between knowledge and actions (expressing no learning and persistence of knowledge about actions). The deductive systems are proved sound and complete with respect to a Kripke-style semantics. Each of the consdered logics is shown to have the small model property and therefore decidable.

@article{DBLP:journals/sLogica/SchmidtTH04,
  author       = {Renate A. Schmidt and
                  Dmitry Tishkovsky and
                  Ullrich Hustadt},
  title        = {Interactions between Knowledge, Action and Commitment within Agent
                  Dynamic Logic},
  journal      = {Stud Logica},
  volume       = {78},
  number       = {3},
  pages        = {381--415},
  year         = {2004},
  url          = {https://doi.org/10.1007/s11225-004-6042-1},
  doi          = {10.1007/S11225-004-6042-1},
  timestamp    = {Tue, 01 Sep 2020 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/sLogica/SchmidtTH04.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/HustadtKRV04,
  author       = {Ullrich Hustadt and
                  Boris Konev and
                  Alexandre Riazanov and
                  Andrei Voronkov},
  editor       = {David A. Basin and
                  Micha{\"{e}}l Rusinowitch},
  title        = {TeMP: {A} Temporal Monodic Prover},
  booktitle    = {Automated Reasoning - Second International Joint Conference, {IJCAR}
                  2004, Cork, Ireland, July 4-8, 2004, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {3097},
  pages        = {326--330},
  publisher    = {Springer},
  year         = {2004},
  url          = {https://doi.org/10.1007/978-3-540-25984-8\_23},
  doi          = {10.1007/978-3-540-25984-8\_23},
  timestamp    = {Sun, 06 Oct 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/HustadtKRV04.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/ecai/HustadtMS04,
  author       = {Ullrich Hustadt and
                  Boris Motik and
                  Ulrike Sattler},
  editor       = {Ram{\'{o}}n L{\'{o}}pez de M{\'{a}}ntaras and
                  Lorenza Saitta},
  title        = {Reasoning in Description Logics with a Concrete Domain in the Framework
                  of Resolution},
  booktitle    = {Proceedings of the 16th Eureopean Conference on Artificial Intelligence,
                  ECAI'2004, including Prestigious Applicants of Intelligent Systems,
                  {PAIS} 2004, Valencia, Spain, August 22-27, 2004},
  pages        = {353--357},
  publisher    = {{IOS} Press},
  year         = {2004},
  timestamp    = {Fri, 11 May 2018 12:42:30 +0200},
  biburl       = {https://dblp.org/rec/conf/ecai/HustadtMS04.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/kr/HustadtMS04,
  author       = {Ullrich Hustadt and
                  Boris Motik and
                  Ulrike Sattler},
  editor       = {Didier Dubois and
                  Christopher A. Welty and
                  Mary{-}Anne Williams},
  title        = {Reducing SHIQ-Description Logic to Disjunctive Datalog Programs},
  booktitle    = {Principles of Knowledge Representation and Reasoning: Proceedings
                  of the Ninth International Conference (KR2004), Whistler, Canada,
                  June 2-5, 2004},
  pages        = {152--162},
  publisher    = {{AAAI} Press},
  year         = {2004},
  url          = {http://www.aaai.org/Library/KR/2004/kr04-018.php},
  timestamp    = {Tue, 09 Feb 2021 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/kr/HustadtMS04.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/lpar/HustadtMS04,
  author       = {Ullrich Hustadt and
                  Boris Motik and
                  Ulrike Sattler},
  editor       = {Franz Baader and
                  Andrei Voronkov},
  title        = {A Decomposition Rule for Decision Procedures by Resolution-Based Calculi},
  booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning, 11th
                  International Conference, {LPAR} 2004, Montevideo, Uruguay, March
                  14-18, 2005, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {3452},
  pages        = {21--35},
  publisher    = {Springer},
  year         = {2004},
  url          = {https://doi.org/10.1007/978-3-540-32275-7\_2},
  doi          = {10.1007/978-3-540-32275-7\_2},
  timestamp    = {Tue, 14 May 2019 10:00:55 +0200},
  biburl       = {https://dblp.org/rec/conf/lpar/HustadtMS04.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@ARTICLE{Georgieva+Hustadt+Schmidt@JSC2003,
 AUTHOR   = {Georgieva, L. and Hustadt, U. and Schmidt, R. A.},
 YEAR     = {2003},
 TITLE    = {Hyperresolution for Guarded Formulae},
 JOURNAL  = {Journal of Symbolic Computation},
 VOLUME   = {36},
 NUMBER   = {1-2},
 PAGES    = {163-192},
 URL      = {http://dx.doi.org/10.1016/S0747-7171(03)00034-8},
 ABSTRACT = {This paper investigates the use of hyperresolution as a decision
 procedure and model builder for guarded formulae.
 In general hyperresolution is not a decision procedure for the entire
 guarded fragment.
 However we show that there are natural fragments of the guarded
 fragment which can be decided by hyperresolution.
 In particular, we prove decidability of hyperresolution with or without
 splitting for the fragment GF1- and point out several ways of
 extending this fragment without loosing decidability.
 As hyperresolution is closely related to various tableaux methods
 the present work is also relevant for tableaux methods.
 We compare our approach to hypertableaux, and mention the relationship to other 
 clausal classes which are decidable by hyperresolution.}
}

This paper investigates the use of hyperresolution as a decision procedure and model builder for guarded formulae. In general hyperresolution is not a decision procedure for the entire guarded fragment. However we show that there are natural fragments of the guarded fragment which can be decided by hyperresolution. In particular, we prove decidability of hyperresolution with or without splitting for the fragment GF1- and point out several ways of extending this fragment without loosing decidability. As hyperresolution is closely related to various tableaux methods the present work is also relevant for tableaux methods. We compare our approach to hypertableaux, and mention the relationship to other clausal classes which are decidable by hyperresolution.

@INPROCEEDINGS{Goranko+Hustadt+Schmidt+Vakarelov@RelMiCS2003,
 AUTHOR        = {Goranko, Valentin and Hustadt, Ullrich and 
 Schmidt, Renate and Vakarelov, Dimiter},
 TITLE         = {{SCAN} is complete for all Sahlqvist formulae},
 BOOKTITLE     = {Proceedings of the 7th International Seminar on
 Relational Methods in Computer Science (RelMiCS-7)
 [Bad Malente, Germany, 12-17 May 2003]},
 YEAR          = {2003},
 EDITOR        = {Berghammer, Rudolf and M{\"o}ller, Bernhard},
 PAGES         = {230-241},
 PUBLISHER     = {Christian-Albrechts-Universit{\"a}t Kiel},
 CADDRESS      = {Bad Malente, Germany},
 CYEAR         = {2003},
 CMONTH        = may # {~12-17},
 URL           = {Goranko+Hustadt+Schmidt+Vakarelov@RelMiCS2003},
 ABSTRACT      = {SCAN is an algorithm for reducing monadic
 existential second-order logic formulae to equivalent simpler
 formulae, often first-order logic formulae. It is provably impossible
 for such a reduction to first-order logic to be always successful,
 even if there is an equivalent first-order formula for a second-order
 logic formula. In this paper we show that SCAN successfully computes
 the first-order equivalents of all Sahlqvist formulae in the classical
 (multi-)modal language.}
}

SCAN is an algorithm for reducing monadic existential second-order logic formulae to equivalent simpler formulae, often first-order logic formulae. It is provably impossible for such a reduction to first-order logic to be always successful, even if there is an equivalent first-order formula for a second-order logic formula. In this paper we show that SCAN successfully computes the first-order equivalents of all Sahlqvist formulae in the classical (multi-)modal language.

@INPROCEEDINGS{Hustadt+Konev@CADE2003,
 AUTHOR        = {Hustadt, U. and Konev, Boris},
 YEAR          = {2003},
 TITLE         = {TRP{+}{+} 2.0:  A temporal resolution prover},
 XEDITOR       = {Baader, F.},
 BOOKTITLE     = {Proceedings of the 19th International Conference on Automated Deduction
 (CADE-19) [Miamia Beach, USA, July/August 2003]},
 SERIES        = {Lecture Notes in Artificial Intelligence},
 VOLUME        = {2741},
 PUBLISHER     = {Springer},
 PAGES         = {274-278},
 URL           = {Hustadt+Konev@CADE2003.pdf},
 ABSTRACT      = {In this paper we present TRP++ Version 2.0,
 a theorem prover for propositional linear time logic PLTL. 
 TRP++ is based on the resolution method for PLTL developed by 
 Fisher which involves the translation of PLTL-formulae to 
 separated normal form and the application of the inference rules 
 of the temporal resolution calculus.}
}

In this paper we present TRP++ Version 2.0, a theorem prover for propositional linear time logic PLTL. TRP++ is based on the resolution method for PLTL developed by Fisher which involves the translation of PLTL-formulae to separated normal form and the application of the inference rules of the temporal resolution calculus.

@TECHREPORT{Hustadt+Motik+Sattler@FZI-TR2003,
 AUTHOR        = {Hustadt, U. and Motik, B. and Sattler, U.},
 TITLE         = {Reducing SHIQ- Description Logic to Disjunctive Datalog Programs},
 XTITLE        = {Reducing {$\mathcal{SHIQ}^$-}Description Logic to Disjunctive Datalog Programs},
 INSTITUTION   = {FZI},
 ADDRESS       = {Karlsruhe, Germany},
 NUMBER        = {1-8-11/03},
 MONTH         = nov,
 YEAR          = {2003},
 NOTE          = {Revised version submitted to KR conference, http://www.fzi.de/wim/eng/publikationen.php?id=1103},
 URL           = {FZI-1-8-11-03.pdf},
 ABSTRACT      = {As applications of description logics proliferate,
 efficient reasoning with large ABoxes (sets of individuals with
 descriptions) becomes ever more important. Motivated by the prospects
 of reusing optimization techniques from deductive databases, in this
 paper, we present a novel approach to checking consistency of ABoxes,
 instance checking and query answering, w.r.t. ontologies formulated
 using a slight restriction of the description logic SHIQ. Our approach
 proceeds in three steps: (i) the ontology is translated into
 first-order clauses, (ii) TBox and RBox clauses are saturated using a
 resolution-based decision procedure, and (iii) the saturated set of
 clauses is translated into a disjunctive datalog program. Thus, query
 answering can be performed using the resulting program, while applying
 all existing optimization techniques, such as join-order optimizations
 or magic sets. Equally important, the resolution-based decision
 procedure we present is for unary coding of numbers worst-case
 optimal, i.e. it runs in EXPTIME.} 
}

As applications of description logics proliferate, efficient reasoning with large ABoxes (sets of individuals with descriptions) becomes ever more important. Motivated by the prospects of reusing optimization techniques from deductive databases, in this paper, we present a novel approach to checking consistency of ABoxes, instance checking and query answering, w.r.t. ontologies formulated using a slight restriction of the description logic SHIQ. Our approach proceeds in three steps: (i) the ontology is translated into first-order clauses, (ii) TBox and RBox clauses are saturated using a resolution-based decision procedure, and (iii) the saturated set of clauses is translated into a disjunctive datalog program. Thus, query answering can be performed using the resulting program, while applying all existing optimization techniques, such as join-order optimizations or magic sets. Equally important, the resolution-based decision procedure we present is for unary coding of numbers worst-case optimal, i.e. it runs in EXPTIME.

@inproceedings{Konev+Degtyarev+Dixon+Fisher+Hustadt@TIME2003,
 author    = {Boris Konev and
              Anatoli Degtyarev and
              Clare Dixon and
              Michael Fisher and
              Ullrich Hustadt},
 title     = {Towards the Implementation of First-Order Temporal Resolution:
              the Expanding Domain Case},
 year      = {2003},
 pages     = {72-82},
 url       = {http://doi.ieeecomputersociety.org/10.1109/TIME.2003.1214882},
 booktitle = {Proceedings of the 10th International Symposium on Temporal Representation
              and Reasoning / 4th International Conference on Temporal
              Logic (TIME-ICTL 2003), [Cairns, Queensland, Australia, 8-10 July 2003]},
 publisher = {IEEE Computer Society},
 year      = {2003},
 isbn      = {0-7695-1912-1},
 bibsource = {DBLP, http://dblp.uni-trier.de},
 abstract  = {First-order temporal logic is a concise and powerful notation, 
 with many potential applications in both Computer Science and 
 Artificial Intelligence. While the full logic is highly complex, 
 recent work on monodic first-order temporal logics has identified 
 important enumerable and even decidable fragments. In this paper, 
 we develop a clausal resolution method for the monodic fragment 
 of first-order temporal logic over expanding domains. We first 
 define a normal form for monodic formulae and then introduce novel 
 resolution calculi that can be applied to formulae in this normal form. 
 We state correctness and completeness results for the method. 
 We illustrate the method on a comprehensive example. The method is 
 based on classical first-order resolution and can, thus, be 
 efficiently implemented.}
}

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. In this paper, we develop a clausal resolution method for the monodic fragment of first-order temporal logic over expanding domains. We first define a normal form for monodic formulae and then introduce novel resolution calculi that can be applied to formulae in this normal form. We state correctness and completeness results for the method. We illustrate the method on a comprehensive example. The method is based on classical first-order resolution and can, thus, be efficiently implemented.

@INPROCEEDINGS{Schmidt+Hustadt@CADE2003,
 AUTHOR    = {Schmidt, R. A. and Hustadt, U.},
 YEAR      = {2003},
 TITLE     = {A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae},
 XEDITOR   = {Baader, F.},
 BOOKTITLE = {Proceedings of the 19th International Conference on Automated Deduction 
 (CADE-19) [Miami Beach, USA, July/August 2003]},
 SERIES    = {Lecture Notes in Artificial Intelligence},
 VOLUME    = {2741},
 PUBLISHER = {Springer},
 PAGES     = {412-426},
 URL       = {Schmidt+Hustadt@CADE2003.pdf},
 URL       = {http://dx.doi.org/10.1007/978-3-540-45085-6_36},
 ABSTRACT = {In this paper we present a translation principle, called the
 \emph{axiomatic translation}, for reducing propositional modal logics
 with background theories, including triangular properties such as 
 transitivity, Euclideanness and functionality, to decidable logics.
 The goal of the axiomatic translation principle is to find simplified 
 theories, which capture the inference problems in the original theory, 
 but in a way that is more amenable to automation and easier to deal with 
 by existing theorem provers.
 The principle of the axiomatic translation is conceptually very simple
 and can be largely automated.
 Soundness is automatic under reasonable assumptions, and termination of
 ordered resolution is easily achieved, but the non-trivial part of the 
 approach is proving completeness.}
}

In this paper we present a translation principle, called the \emphaxiomatic translation, for reducing propositional modal logics with background theories, including triangular properties such as transitivity, Euclideanness and functionality, to decidable logics. The goal of the axiomatic translation principle is to find simplified theories, which capture the inference problems in the original theory, but in a way that is more amenable to automation and easier to deal with by existing theorem provers. The principle of the axiomatic translation is conceptually very simple and can be largely automated. Soundness is automatic under reasonable assumptions, and termination of ordered resolution is easily achieved, but the non-trivial part of the approach is proving completeness.

@INCOLLECTION{Schmidt+Hustadt@TARSKI2003,
 AUTHOR      = {Schmidt, R. A. and Hustadt, U.},
 MONTH       = dec,
 YEAR        = {2003},
 TITLE       = {Mechanised Reasoning and Model Generation for Extended 
 Modal Logics},
 SERIES      = {LNCS},
 VOLUME      = {2929},
 EDITOR      = {de Swart, Harrie and Orlowska, Ewa and
 Schmidt, Gunther and Roubens, Marc},
 BOOKTITLE   = {Theory and Applications of Relational Structures
 as Knowledge Instruments. COST Action 274, TARSKI. Revised Papers},
 PAGES       = {38-67},
 URL         = {Schmidt+Hustadt@TARSKI2003.pdf},
 URL         = {http://dx.doi.org/10.1007/978-3-540-24615-2_3},
 ABSTRACT    = {The approach presented in this overview paper exploits that
 modal logics can be seen to be fragments of first-order logic and
 deductive methods can be developed and studied within the framework
 of first-order resolution.
 We focus on a class of extended modal logics very similar in spirit to
 propositional dynamic logic and closely related to description logics.
 We review and discuss the development of decision procedures
 for decidable extended modal logics and look at methods for
 automatically generating models.}
}

The approach presented in this overview paper exploits that modal logics can be seen to be fragments of first-order logic and deductive methods can be developed and studied within the framework of first-order resolution. We focus on a class of extended modal logics very similar in spirit to propositional dynamic logic and closely related to description logics. We review and discuss the development of decision procedures for decidable extended modal logics and look at methods for automatically generating models.

@TECHREPORT{Schmidt+Hustadt@UoMCS-TR2003,
 AUTHOR      = {Schmidt, R. A. and Hustadt, U.},
 TITLE       = {Mechanised Reasoning and Model Generation for Extended Modal Logics},
 MONTH       = {January},
 YEAR        = {2003},
 TYPE        = {Preprint Series},
 NUMBER      = {CSPP-19},
 INSTITUTION = {University of Manchester},
 ADDRESS     = {UK},
 NOTE        = {Submitted for publication.} ,
 URL         = {Schmidt+Hustadt@uOMCS-TR2003.pdf},
 ABSTRACT    = {The approach presented in this overview paper exploits
 that modal logics can be seen to be fragments of first-order logic and
 deductive methods can be developed and studied within the framework of
 first-order resolution. We focus on a class of extended modal logics
 very similar in spirit to propositional dynamic logic and closely
 related to description logics. We review and discuss the development
 of decision procedures for decidable extended modal logics and look at
 methods for automatically generating models.} 
}

The approach presented in this overview paper exploits that modal logics can be seen to be fragments of first-order logic and deductive methods can be developed and studied within the framework of first-order resolution. We focus on a class of extended modal logics very similar in spirit to propositional dynamic logic and closely related to description logics. We review and discuss the development of decision procedures for decidable extended modal logics and look at methods for automatically generating models.

@INPROCEEDINGS{Schmidt+Orlowska+Hustadt@RelMiCS2003,
 AUTHOR        = {Schmidt, Renate A. and Or{\l}owska, Ewa and 
 Hustadt, Ullrich},
 TITLE         = {Two proof systems for {Peirce} algebras},
 BOOKTITLE     = {Proceedings of the 7th International Seminar on
 Relational Methods in Computer Science (RelMiCS-7)
 [Bad Malente, Germany, 12-17 May 2003]},
 YEAR          = {2003},
 EDITOR        = {Berghammer, Rudolf and M{\"o}ller, Bernhard},
 PAGES         = {197--203},
 PUBLISHER     = {Christian-Albrechts-Universit{\"a}t Kiel},
 CADDRESS      = {Bad Malente, Germany},
 CYEAR         = {2003},
 CMONTH        = may # {~12--17},
 URL           = {Schmidt+Orlowska+Hustadt@RelMiCS2003.pdf},
 ABSTRACT      = {This paper develops and compares two tableaux-style proof systems for
 Peirce algebras.
 One is a tableau refutation proof system, the other is a proof system in
 the style of Rasiowa-Sikorski.}
}

This paper develops and compares two tableaux-style proof systems for Peirce algebras. One is a tableau refutation proof system, the other is a proof system in the style of Rasiowa-Sikorski.

@article{DBLP:journals/jsc/GeorgievaHS03,
  author       = {Lilia Georgieva and
                  Ullrich Hustadt and
                  Renate A. Schmidt},
  title        = {Hyperresolution for guarded formulae},
  journal      = {J. Symb. Comput.},
  volume       = {36},
  number       = {1-2},
  pages        = {163--192},
  year         = {2003},
  url          = {https://doi.org/10.1016/S0747-7171(03)00034-8},
  doi          = {10.1016/S0747-7171(03)00034-8},
  timestamp    = {Wed, 17 Feb 2021 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/jsc/GeorgievaHS03.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/RelMiCS/GorankoHSV03,
  author       = {Valentin Goranko and
                  Ullrich Hustadt and
                  Renate A. Schmidt and
                  Dimiter Vakarelov},
  editor       = {Rudolf Berghammer and
                  Bernhard M{\"{o}}ller and
                  Georg Struth},
  title        = {{SCAN} Is Complete for All Sahlqvist Formulae},
  booktitle    = {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, Bad Malente, Germany,
                  May 12-17, 2003, Revised Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {3051},
  pages        = {149--162},
  publisher    = {Springer},
  year         = {2003},
  url          = {https://doi.org/10.1007/978-3-540-24771-5\_13},
  doi          = {10.1007/978-3-540-24771-5\_13},
  timestamp    = {Tue, 14 May 2019 10:00:51 +0200},
  biburl       = {https://dblp.org/rec/conf/RelMiCS/GorankoHSV03.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/RelMiCS/SchmidtOH03,
  author       = {Renate A. Schmidt and
                  Ewa Orlowska and
                  Ullrich Hustadt},
  editor       = {Rudolf Berghammer and
                  Bernhard M{\"{o}}ller and
                  Georg Struth},
  title        = {Two Proof Systems for Peirce Algebras},
  booktitle    = {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, Bad Malente, Germany,
                  May 12-17, 2003, Revised Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {3051},
  pages        = {238--251},
  publisher    = {Springer},
  year         = {2003},
  url          = {https://doi.org/10.1007/978-3-540-24771-5\_21},
  doi          = {10.1007/978-3-540-24771-5\_21},
  timestamp    = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/RelMiCS/SchmidtOH03.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/HustadtK03,
  author       = {Ullrich Hustadt and
                  Boris Konev},
  editor       = {Franz Baader},
  title        = {{TRP++2.0:} {A} Temporal Resolution Prover},
  booktitle    = {Automated Deduction - CADE-19, 19th International Conference on Automated
                  Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {2741},
  pages        = {274--278},
  publisher    = {Springer},
  year         = {2003},
  url          = {https://doi.org/10.1007/978-3-540-45085-6\_21},
  doi          = {10.1007/978-3-540-45085-6\_21},
  timestamp    = {Sun, 06 Oct 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/HustadtK03.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/SchmidtH03,
  author       = {Renate A. Schmidt and
                  Ullrich Hustadt},
  editor       = {Franz Baader},
  title        = {A Principle for Incorporating Axioms into the First-Order Translation
                  of Modal Formulae},
  booktitle    = {Automated Deduction - CADE-19, 19th International Conference on Automated
                  Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {2741},
  pages        = {412--426},
  publisher    = {Springer},
  year         = {2003},
  url          = {https://doi.org/10.1007/978-3-540-45085-6\_36},
  doi          = {10.1007/978-3-540-45085-6\_36},
  timestamp    = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/SchmidtH03.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/time/KonevDDFH03,
  author       = {Boris Konev and
                  Anatoli Degtyarev and
                  Clare Dixon and
                  Michael Fisher and
                  Ullrich Hustadt},
  title        = {Towards the Implementation of First-Order Temporal Resolution: the
                  Expanding Domain Case},
  booktitle    = {10th International Symposium on Temporal Representation and Reasoning
                  / 4th International Conference on Temporal Logic {(TIME-ICTL} 2003),
                  8-10 July 2003, Cairns, Queensland, Australia},
  pages        = {72--82},
  publisher    = {{IEEE} Computer Society},
  year         = {2003},
  url          = {https://doi.org/10.1109/TIME.2003.1214882},
  doi          = {10.1109/TIME.2003.1214882},
  timestamp    = {Sun, 06 Oct 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/time/KonevDDFH03.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@incollection{DBLP:conf/RelMiCS/SchmidtH03,
  author       = {Renate A. Schmidt and
                  Ullrich Hustadt},
  editor       = {Harrie C. M. de Swart and
                  Ewa Orlowska and
                  Gunther Schmidt and
                  Marc Roubens},
  title        = {Mechanised Reasoning and Model Generation for Extended Modal Logics},
  booktitle    = {Theory and Applications of Relational Structures as Knowledge Instruments,
                  {COST} Action 274, TARSKI, Revised Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {2929},
  pages        = {38--67},
  publisher    = {Springer},
  year         = {2003},
  url          = {https://doi.org/10.1007/978-3-540-24615-2\_3},
  doi          = {10.1007/978-3-540-24615-2\_3},
  timestamp    = {Sun, 02 Oct 2022 15:53:27 +0200},
  biburl       = {https://dblp.org/rec/conf/RelMiCS/SchmidtH03.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@ARTICLE{Bennett+Dixon+Fisher+Hustadt+Franconi+Horrocks+de_Rijke@AIR2002,
 AUTHOR        = {Bennett, Brandon and 
 Dixon, Clare and Fisher, Michael and Hustadt, Ullrich and
 Franconi, Enrico and Horrocks, Ian and 
 de Rijke, Maarten},
 TITLE         = {Combinations of Modal Logics},
 JOURNAL       = {AI Review},
 VOLUME        = {17},
 NUMBER        = {1},
 PAGES         = {1-20},
 MONTH         = mar,
 YEAR          = {2002},
 URL           = {Bennett+Dixon+Fisher+Hustadt+Franconi+Horrocks+de_Rijke@AIR2002.pdf},
 URL           = {http://dx.doi.org/10.1023/A:1015057926707},
 ABSTRACT = {There is increasing use of combinations of modal logics
 in both foundational and applied research areas. This article provides
 an introduction to both the principles of such combinations and to
 the variety of techniques that have been developed for them. In
 addition,the article outlines many key research problems yet to be
 tackled within this callenging area of work.}  
}

There is increasing use of combinations of modal logics in both foundational and applied research areas. This article provides an introduction to both the principles of such combinations and to the variety of techniques that have been developed for them. In addition,the article outlines many key research problems yet to be tackled within this callenging area of work.

@INPROCEEDINGS{Georgieva+Hustadt+Schmidt@CADE2002,
 AUTHOR        = {Georgieva, Lilia and Hustadt, Ullrich and Schmidt, Renate A.},
 TITLE         = {A new clausal class decidable by hyperresolution},
 BOOKTITLE     = {Proceedings of the 18th International Conference on Automated Deduc
tion (CADE-18) [Copenhagen, Denmark, 27-30 July 2002]},
 YEAR          = {2002},
 EDITOR        = {Voronkov, Andrei},
 PAGES         = {258-272},
 PUBLISHER     = {Springer},
 PYEAR         = {2002},
 CADDRESS      = {Copenhagen, Denmark},
 CYEAR         = {2002},
 CMONTH        = jul # {~27-30},
 SERIES        = {LNAI},
 VOLUME        = {2392},
 URL           = {Georgieva+Hustadt+Schmidt@CADE2002.pdf},
 URL           = {http://dx.doi.org/10.1007/3-540-45620-1_21},
 ABSTRACT      = {In this paper we define a new clausal class, called
 BU, which can be decided by hyperresolution with
 splitting. We also consider the model generation
 problem for BU and show that hyperresolution plus
 splitting can also be used as a Herbrand model
 generation procedure for BU and, furthermore, that the
 addition of a local minimality test allows us to
 generate only minimal Herbrand models for clause sets
 in BU. In addition, we investigate the relationship of
 BU to other solvable classes.}
}

In this paper we define a new clausal class, called BU, which can be decided by hyperresolution with splitting. We also consider the model generation problem for BU and show that hyperresolution plus splitting can also be used as a Herbrand model generation procedure for BU and, furthermore, that the addition of a local minimality test allows us to generate only minimal Herbrand models for clause sets in BU. In addition, we investigate the relationship of BU to other solvable classes.

@INPROCEEDINGS{Georgieva+Hustadt+Schmidt@DL2002,
 TITLE        = {On the relationship between decidable fragments, non-classical logics, and de
scription logics},
 AUTHOR       = {Georgieva, Lilia and Hustadt, Ullrich and Schmidt, Renate A.},
 PAGES        = {25-36},
 BOOKTITLE    = {Proceedings of the 2002 International Workshop on
 Description Logics (DL 2002) [Toulouse, France, 19-21 April 2002]},
 YEAR         = {2002},
 EDITOR       = {Horrocks, Ian and Tessaris, Sergio},
 PUBLISHER    = {},
 PYEAR        = {2002},
 CADDRESS     = {Toulouse, France},
 CYEAR        = {2002},
 CMONTH       = apr # {~19-21},
 NOTE         = {Proceedings are also available as CEUR Publication at
 http://CEUR-WS.org/Vol-53/},
 URL          = {Georgieva+Hustadt+Schmidt@DL2002.pdf},
 ABSTRACT     = {The guarded fragment and its extensions and subfragments have often 
 been considered as a framework for investigating the properties of 
 description logics. But there are other decidable fragments which all
 have in common that they generalise the standard translation of ALC 
 to first-order logic.
 <p>
 We provide a short survey of some of these fragments and motivate why
 they are interesting with respect to description logics.
 </p>}
}

The guarded fragment and its extensions and subfragments have often been considered as a framework for investigating the properties of description logics. But there are other decidable fragments which all have in common that they generalise the standard translation of ALC to first-order logic.

We provide a short survey of some of these fragments and motivate why they are interesting with respect to description logics.

@ARTICLE{Hustadt+Schmidt@JAR2002,
 AUTHOR   = {Hustadt, U. and Schmidt, R. A.},
 YEAR     = {2001},
 TITLE    = {Using Resolution for Testing Modal Satisfiability and Building Models},
 JOURNAL  = {Journal of Automated Reasoning},
 VOLUME   = {28},
 NUMBER   = {2},
 YEAR     = {2002},
 PAGES    = {205-232},
 MONTH    = feb,
 ISSN     = {0168-7433},
 URL      = {http://dx.doi.org/10.1023/A:1015067300005},
 ABSTRACT = {This paper presents a translation-based resolution decision
 procedure for the multi-modal logic $\textit{K}_{(m)}(\cap,\cup,\smile)$
 defined over families of relations closed under intersection, union and
 converse.  The relations may satisfy certain additional frame properties.
 Different from previous resolution decision procedures which are based
 on ordering refinements our procedure is based on a selection refinement,
 the derivations of which correspond to derivations of tableaux or sequent
 proof systems.  This procedure has the advantage that it can be used
 both as a satisfiability checker and a model builder.  We show that
 tableaux and sequent-style proof systems can be polynomially simulated
 with our procedure.  Furthermore, the finite model property follows for
 a number of extended modal logics.}, 
}

This paper presents a translation-based resolution decision procedure for the multi-modal logic $K}_{(m)}(∩,∪,⌣)$ defined over families of relations closed under intersection, union and converse. The relations may satisfy certain additional frame properties. Different from previous resolution decision procedures which are based on ordering refinements our procedure is based on a selection refinement, the derivations of which correspond to derivations of tableaux or sequent proof systems. This procedure has the advantage that it can be used both as a satisfiability checker and a model builder. We show that tableaux and sequent-style proof systems can be polynomially simulated with our procedure. Furthermore, the finite model property follows for a number of extended modal logics.

@INPROCEEDINGS{Hustadt+Schmidt@KR2002,
 AUTHOR    = {Hustadt, U. and Schmidt, R. A.},
 YEAR      = {2002},
 TITLE     = {Scientific Benchmarking with Temporal Logic Decision Procedures},
 EDITOR    = {Fensel, D. and Giunchiglia, F. and McGuinness, D. and Williams, M.-A.},
 BOOKTITLE = {Principles of Knowledge Representation and Reasoning: Proceedings
 of the Eighth International Conference (KR 2002) [Toulouse, France, 22-25 April 2002]},
 PUBLISHER = {Morgan Kaufmann},
 PAGES     = {533-544},
 CADDRESS  = {Toulouse, France},
 CMONTH    = apr # {~22-25},
 CYEAR     = {2002},
 URL       = {Hustadt+Schmidt@KR2002.pdf},
 ABSTRACT  = {In this paper we propose a hypothesis-driven design of the
 empirical analysis of different decision procedures which we refer to
 as \emph{scientific benchmarking}.  The approach is to start by
 choosing the benchmark problems for which, on the basis of analytical
 considerations, we expect a particular decision procedure to exhibit a
 behaviour different from another decision procedure.  Then empirical
 tests are performed in order to verify the particular hypothesis
 concerning the decision procedures under consideration.  As a case
 study, we apply this methodology to compare different decision
 procedures for propositional temporal logic.  We define two classes of
 randomly generated temporal logic formulae which we use to investigate
 the behaviour of two tableaux-based temporal logic approaches using
 the Logics Workbench, a third tableaux-based approach using the
 STeP system, and temporal resolution using a new prover
 called TRP.}
}

In this paper we propose a hypothesis-driven design of the empirical analysis of different decision procedures which we refer to as \emphscientific benchmarking. The approach is to start by choosing the benchmark problems for which, on the basis of analytical considerations, we expect a particular decision procedure to exhibit a behaviour different from another decision procedure. Then empirical tests are performed in order to verify the particular hypothesis concerning the decision procedures under consideration. As a case study, we apply this methodology to compare different decision procedures for propositional temporal logic. We define two classes of randomly generated temporal logic formulae which we use to investigate the behaviour of two tableaux-based temporal logic approaches using the Logics Workbench, a third tableaux-based approach using the STeP system, and temporal resolution using a new prover called TRP.

@article{DBLP:journals/air/BennettDFHFHR02,
  author       = {Brandon Bennett and
                  Clare Dixon and
                  Michael Fisher and
                  Ullrich Hustadt and
                  Enrico Franconi and
                  Ian Horrocks and
                  Maarten de Rijke},
  title        = {Combinations of Modal Logics},
  journal      = {Artif. Intell. Rev.},
  volume       = {17},
  number       = {1},
  pages        = {1--20},
  year         = {2002},
  url          = {https://doi.org/10.1023/A:1015057926707},
  doi          = {10.1023/A:1015057926707},
  timestamp    = {Tue, 12 Apr 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/air/BennettDFHFHR02.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jar/HustadtS02,
  author       = {Ullrich Hustadt and
                  Renate A. Schmidt},
  title        = {Using Resolution for Testing Modal Satisfiability and Building Models},
  journal      = {J. Autom. Reason.},
  volume       = {28},
  number       = {2},
  pages        = {205--232},
  year         = {2002},
  url          = {https://doi.org/10.1023/A:1015067300005},
  doi          = {10.1023/A:1015067300005},
  timestamp    = {Wed, 02 Sep 2020 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/jar/HustadtS02.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/GeorgievaHS02,
  author       = {Lilia Georgieva and
                  Ullrich Hustadt and
                  Renate A. Schmidt},
  editor       = {Andrei Voronkov},
  title        = {A New Clausal Class Decidable by Hyperresolution},
  booktitle    = {Automated Deduction - CADE-18, 18th International Conference on Automated
                  Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {2392},
  pages        = {260--274},
  publisher    = {Springer},
  year         = {2002},
  url          = {https://doi.org/10.1007/3-540-45620-1\_21},
  doi          = {10.1007/3-540-45620-1\_21},
  timestamp    = {Tue, 14 May 2019 10:00:39 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/GeorgievaHS02.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/dlog/GeorgievaHS02,
  author       = {Lilia Georgieva and
                  Ullrich Hustadt and
                  Renate A. Schmidt},
  editor       = {Ian Horrocks and
                  Sergio Tessaris},
  title        = {On the relationship between decidable fragments, non-classical logics,
                  and description logics},
  booktitle    = {Proceedings of the 2002 International Workshop on Description Logics
                  (DL2002), Toulouse, France, April 19-21, 2002},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {53},
  publisher    = {CEUR-WS.org},
  year         = {2002},
  url          = {https://ceur-ws.org/Vol-53/GeorgievaHustadtSchmidt.ps},
  timestamp    = {Fri, 10 Mar 2023 16:23:16 +0100},
  biburl       = {https://dblp.org/rec/conf/dlog/GeorgievaHS02.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/kr/HustadtS02,
  author       = {Ullrich Hustadt and
                  Renate A. Schmidt},
  editor       = {Dieter Fensel and
                  Fausto Giunchiglia and
                  Deborah L. McGuinness and
                  Mary{-}Anne Williams},
  title        = {Scientific Benchmarking with Temporal Logic Decision Procedures},
  booktitle    = {Proceedings of the Eights International Conference on Principles and
                  Knowledge Representation and Reasoning (KR-02), Toulouse, France,
                  April 22-25, 2002},
  pages        = {533--546},
  publisher    = {Morgan Kaufmann},
  year         = {2002},
  timestamp    = {Tue, 22 Jul 2003 15:20:23 +0200},
  biburl       = {https://dblp.org/rec/conf/kr/HustadtS02.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@INCOLLECTION{Fermueller+Leitsch+Hustadt+Tammet@HAR2001,
 AUTHOR        = {Ferm{\"u}ller, Christian and Leitsch, Alexander and Hustadt, Ullrich and Tammet, Tanel},
 TITLE         = {Resolution Decision Procedures},
 EDITOR        = {Robinson, Alan and Voronkov, Andrei},
 BOOKTITLE     = {Handbook of Automated Reasoning},
 PUBLISHER     = {Elsevier}, 
 YEAR          = {2001},
 PAGES         = {1791-1850},
 CHAPTER       = {25},
 URL           = {Fermueller+Leitsch+Hustadt+Tammet@HAR2001},
 ABSTRACT      = {J. H. Joyner [1973] showed in his thesis that resolution 
 an be turned into a decision procedure for many classes of 
 clause sets that correspond to classical solvable classes.
 On the basis of Joyner's approach we present resolution as decision procedure;
 that means we systematically investigate resolution refinements with respect to
 their potential as decision proedures.}
}

J. H. Joyner [1973] showed in his thesis that resolution an be turned into a decision procedure for many classes of clause sets that correspond to classical solvable classes. On the basis of Joyner's approach we present resolution as decision procedure; that means we systematically investigate resolution refinements with respect to their potential as decision proedures.

@INPROCEEDINGS{Georgieva+Hustadt+Schmidt@IJCARShort2001,
 AUTHOR        = {Georgieva, Lilia and Hustadt, Ullrich and Schmidt, Renate A.},
 TITLE         = {Computational space efficiency and minimal model 
 generation for guarded formulae},
 BOOKTITLE     = {International Joint Conference on Automated Reasoning IJCAR 2001: Short Papers},
 EDITOR        = {Gore{\'e}, R. and Leitsch, A. and Nipkow, T.},
 PAGES         = {34-43},
 PUBLISHER     = {Departimento di Ingegneria dell'Informazione, Universit{\'a} degli Studi di Siena},
 PADDRESS      = {Siena, Italy},
 PYEAR         = {2001},
 CADDRESS      = {Siena, Italy},
 CYEAR         = {2001},
 YEAR          = {2001},
 CMONTH        = jun # {~19--23},
 SERIES        = {Technical Report},
 VOLUME        = {DII 11/01},
 URL           = {http://www.csc.liv.ac.uk/~ullrich/publications/Georgieva+Hustadt+Schmidt@IJCARShort2001.pdf},
 XNOTE         = {Appeared as Technical Report DII 11/01, Departimento di Ingegneria dell'Informazione, Universit{\'a} degli Studi di Siena, Italy},
 ABSTRACT      = {This paper addresses two issues. First, it presents an
 efficient hyperresolution-based decision procedure for subfragments of the
 guareded fragment which requires polynomial space and secondly it 
 describes a minimal model generation procedure which constructs all and
 only minimal Herbrand models for guarded formulae. Both procedures have
 concrete application domains, i.e. they are relevant for many multi-modal
 and descriptions logics that can be embedded into the guarded fragment. 
 The space optimal decision procedure effectively corresponds to
 tableaux-based polynomial space algorithms for testing the concept
 satisfiability of description logics. It is motivated by the trace technique,
 however it does not use blocking. The minimal Herbrand model generation 
 procedure is based on hyperresolution and complement splitting. We study
 the properties of the procedure and show that is sound and complete.}
}

This paper addresses two issues. First, it presents an efficient hyperresolution-based decision procedure for subfragments of the guareded fragment which requires polynomial space and secondly it describes a minimal model generation procedure which constructs all and only minimal Herbrand models for guarded formulae. Both procedures have concrete application domains, i.e. they are relevant for many multi-modal and descriptions logics that can be embedded into the guarded fragment. The space optimal decision procedure effectively corresponds to tableaux-based polynomial space algorithms for testing the concept satisfiability of description logics. It is motivated by the trace technique, however it does not use blocking. The minimal Herbrand model generation procedure is based on hyperresolution and complement splitting. We study the properties of the procedure and show that is sound and complete.

@INPROCEEDINGS{Georgieva+Hustadt+Schmidt@LPAR2001,
 AUTHOR        = {Georgieva, Lilia and Hustadt, Ullrich and Schmidt, Renate A.},
 TITLE         = {Computational space efficiency and minimal model generation
 for guarded formulae},
 BOOKTITLE     = {Proceedings of the 8th International Conference on Logic for 
 Programming, Artificial Intelligence, and Reasoning (LPAR 2001)
 [Havana, Cuba, 3-7 December 2001]},
 YEAR          = {2001},
 EDITOR        = {Nieuwenhuis, R. and Voronkov, A.},
 PAGES         = {85-99},
 PUBLISHER     = {Springer},
 PYEAR         = {2001},
 CADDRESS      = {Havana, Cuba},
 CYEAR         = {2001},
 CMONTH        = dec # {~3-7},
 SERIES        = {LNAI},
 VOLUME        = {2250},
 ISBN          = {3-540-42957-3},
 URL           = {Georgieva+Hustadt+Schmidt@LPAR2001.pdf},
 ABSTRACT      = {This paper investigates the use of hyperresolution as 
 a decision procedure and model builder for guarded formulae.
 In general hyperresolution is not a decision procedure for the entire
 guarded fragment. However we show that there are natural fragments which 
 can be decided by hyperresolution.
 In particular, we prove decidability of hyperresolution with or without
 splitting for the fragment GF1- and point out several ways of
 extending this fragment without loosing decidability.
 As hyperresolution is closely related to various tableaux methods
 the present work is also relevant for tableaux methods.
 We compare our approach to hypertableaux, and 
 mention the relationship to other clausal classes which are
 decidable by hyperresolution.}
}

This paper investigates the use of hyperresolution as a decision procedure and model builder for guarded formulae. In general hyperresolution is not a decision procedure for the entire guarded fragment. However we show that there are natural fragments which can be decided by hyperresolution. In particular, we prove decidability of hyperresolution with or without splitting for the fragment GF1- and point out several ways of extending this fragment without loosing decidability. As hyperresolution is closely related to various tableaux methods the present work is also relevant for tableaux methods. We compare our approach to hypertableaux, and mention the relationship to other clausal classes which are decidable by hyperresolution.

@INCOLLECTION{Hirsch+Hustadt@M4M2001,
 AUTHOR        = {Hirsch, Benjamin and Hustadt, Ullrich},
 TITLE         = {Translating PLTL into WS1S: Application Description},
 BOOKTITLE     = {Methods for Modalities II},
 PUBLISHER     = {University of Amsterdam},
 YEAR          = {2001},
 URL           = {Hirsch+Hustadt@M4M2001.pdf},
 ABSTRACT      = {This paper introduces a technique for translating propositional linear
 time logic PLTL into the weak second-order logic of one successor
 WS1S. Using the MONA tool, a decision procedure for WS1S, we
 obtain a decision procedure for PLTL. We demonstrate the viability of
 this approach by an empirical comparison with STeP, SMV, and
 the Logics Workbench on a class of semi-randomly generated PLTL-formulae.}
}

This paper introduces a technique for translating propositional linear time logic PLTL into the weak second-order logic of one successor WS1S. Using the MONA tool, a decision procedure for WS1S, we obtain a decision procedure for PLTL. We demonstrate the viability of this approach by an empirical comparison with STeP, SMV, and the Logics Workbench on a class of semi-randomly generated PLTL-formulae.

@INCOLLECTION{Hustadt+Dixon+Schmidt+Fisher+Meyer+van_der_Hoek@ATFP2005,
 AUTHOR        = {Hustadt, Ullrich and Dixon, C. and Schmidt, R. A. and Fisher, M.
 and Meyer, J.-J. C. and van der Hoek, W.},
 TITLE         = {Verification within the {KARO} Agent Theory},
 BOOKTITLE     = {Agent Technology from a Formal Perspective},
 YEAR          = {2001},
 EDITOR        = {Rouff, C. A. and Hinchey, M. G. and 
 Rash, J. L. and Truszkowski, W. and Gordon-Spears, D.},
 PUBLISHER     = {Springer},
 PAGES         = {193-226},
 PYEAR         = {2005},
 SERIES        = {NASA Monographs in Systems and Software Engineering},
 ISBN          = {1-85233-947-0},
 URL           = {Hustadt+Dixon+Schmidt+Fisher+Meyer+van_der_Hoek@ATFP2005.pdf},
 ABSTRACT      = {This chapter proposes two new methods for realising 
 automated reasoning within agent-based systems. We concentrate on a
 core of the KARO framework, which is a speci cation framework for
 modelling intelligent agent behaviour. We discuss the advantages of
 each approach and suggest ways of extending each variant to cover
 more of the KARO framework.},
}

This chapter proposes two new methods for realising automated reasoning within agent-based systems. We concentrate on a core of the KARO framework, which is a speci cation framework for modelling intelligent agent behaviour. We discuss the advantages of each approach and suggest ways of extending each variant to cover more of the KARO framework.

@INPROCEEDINGS{Hustadt+Dixon+Schmidt+Fisher+Meyer+van_der_Hoek@FAABS2000,
 AUTHOR        = {Hustadt, Ullrich and Dixon, C. and Schmidt, R. A. and Fisher, M.
 and Meyer, J.-J. C. and van der Hoek, W.},
 TITLE         = {Verification within the {KARO} Agent Theory},
 BOOKTITLE     = {Proceedings of the First International Workshop on
 Formal Approaches to Agent-Based Systems (FAABS 2000)
 [Goddard Space Flight Center, Greenbelt, MD, USA, 5-7 April 2000]},
 YEAR          = {2001},
 EDITOR        = {Rash, J. L. and Rouff, C. A. and Truszkowski, W. and 
 Gordon, D. and Hinchey, M. G.},
 PAGES         = {33-47},
 PUBLISHER     = {Springer},
 PYEAR         = {2001},
 CADDRESS      = {Goddard Space Flight Center, Greenbelt, MD, USA},
 CYEAR         = {2000},
 CMONTH        = apr # {~5--7},
 SERIES        = {LNAI},
 VOLUME        = {1871},
 ISBN          = {3-540-42716-3},
 URL           = {Hustadt+Dixon+Schmidt+Fisher+Meyer+van_der_Hoek@FAABS2000.pdf},
 ABSTRACT      = {This paper discusses automated reasoning in the KARO
 framework.The KARO framework accommodates a range of expressive modal 
 logics for describing the behaviour of intelligent agents. We
 concentrate on a core logic within this framework, in particular, we
 describe two new methods for providing proof methods for this core
 logic, discuss some of the problems we have encountered in their
 design, and present an extended example of the use of the KARO framework
 and the two proof methods.}
}

This paper discusses automated reasoning in the KARO framework.The KARO framework accommodates a range of expressive modal logics for describing the behaviour of intelligent agents. We concentrate on a core logic within this framework, in particular, we describe two new methods for providing proof methods for this core logic, discuss some of the problems we have encountered in their design, and present an extended example of the use of the KARO framework and the two proof methods.

@INPROCEEDINGS{Hustadt+Dixon+Schmidt+Fisher+Meyer+van_der_Hoek@TIME2001,
 AUTHOR        = {Hustadt, Ullrich and Dixon, Clare and Schmidt, Renate A. and 
 Fisher, Michael and Meyer, John-Jules and van der Hoek, Wiebe},
 TITLE         = {Reasoning about agents in the {KARO} framework},
 BOOKTITLE     = {Proceedings of the Eighth International Symposium on Temporal Representation and Reasoning 
 (TIME-01) [Cividale del Friuli, Italy, 14-16 June 2001]},
 YEAR          = {2001},
 EDITOR        = {Bettini, Claudio and Montanari, Angelo},
 PAGES         = {206-213},
 PUBLISHER     = {IEEE Press},
 PADDRESS      = {Los Alamitos, CA, USA},
 PYEAR         = {2001},
 CADDRESS      = {Cividale del Friuli, Italy},
 CYEAR         = {2001},
 CMONTH        = jun # {~14--16},
 URL           = {Hustadt+Dixon+Schmidt+Fisher+Meyer+van_der_Hoek@TIME2001.pdf},
 URL           = {http://doi.ieeecomputersociety.org/10.1109/TIME.2001.930719},
 ABSTRACT      = {This paper proposes two methods for realising
 automated reasoning about agent-based systems. The framework for
 modelling intelligent agent behaviour that we focus on is a core of
 KARO logic, an expressive combination of various modal logics
 including propositional dynamic logic, a modal logic of knowledge, a
 modal logic of wishes, and additional non-standard operators. The
 first method we present is based on a translation of core KARO logic
 to first-order logic combined with first-order resolution. The second
 method uses an embedding of core KARO logic into a combination of
 branching-time temporal logic CTL and multi-modal S5
 plus a clausal resolution calculus for these combined logics. We
 discuss the advantages and shortcomings of each approach and suggest
 ways to extend each variant to cover more of the KARO framework.}
}

This paper proposes two methods for realising automated reasoning about agent-based systems. The framework for modelling intelligent agent behaviour that we focus on is a core of KARO logic, an expressive combination of various modal logics including propositional dynamic logic, a modal logic of knowledge, a modal logic of wishes, and additional non-standard operators. The first method we present is based on a translation of core KARO logic to first-order logic combined with first-order resolution. The second method uses an embedding of core KARO logic into a combination of branching-time temporal logic CTL and multi-modal S5 plus a clausal resolution calculus for these combined logics. We discuss the advantages and shortcomings of each approach and suggest ways to extend each variant to cover more of the KARO framework.

@INPROCEEDINGS{Hustadt+Schmidt@IDEESMTL2001,
 AUTHOR        = {Hustadt, Ullrich and Schmidt, Renate A.},
 TITLE         = {Formulae which Highlight Differences between 
 Temporal Logic and Dynamic Logic Provers},
 BOOKTITLE     = {Issues in the Design and Experimental Evaluation of
 Systems for Modal and Temporal Logics},
 YEAR          = {2001},
 EDITOR        = {Giunchiglia, E. and Massacci, F.},
 PUBLISHER     = {Dipartimento di Ingegneria dell'Informazione,
 Unversit{\'a} degli Studi di Siena},
 PAGES         = {68-76},
 PADDRESS      = {Siena, Italy},
 PYEAR         = {2001},
 CADDRESS      = {Siena, Italy},
 CYEAR         = {2001},
 CMONTH        = jun # {~18--19},
 SERIES        = {Technical Report DII 14/01},
 URL           = {Hustadt+Schmidt@IDEESMTL2001.pdf},
 ABSTRACT      = {In this Note we compare different inference methods for
 propositional temporal logic by empirical analysis.
 We define a class of randomly generated temporal logic formulae which
 we use to investigate the behaviour of a tableaux-based temporal logic approach
 using the Logics Workbench, a tableaux-based approach for propositional
 dynamic logic using an appropriate translation and the prover
 DLP, and temporal resolution using TRP.}
}

In this Note we compare different inference methods for propositional temporal logic by empirical analysis. We define a class of randomly generated temporal logic formulae which we use to investigate the behaviour of a tableaux-based temporal logic approach using the Logics Workbench, a tableaux-based approach for propositional dynamic logic using an appropriate translation and the prover DLP, and temporal resolution using TRP.

@article{DBLP:journals/jolli/Hustadt01,
  author       = {Ullrich Hustadt},
  title        = {Temporal Logic: Mathematical Foundations and Computational Aspects,
                  Volume 2, Dov M. Gabbay, Mark A. Reynolds, and Marcelo Finger},
  journal      = {J. Log. Lang. Inf.},
  volume       = {10},
  number       = {3},
  pages        = {406--410},
  year         = {2001},
  url          = {https://doi.org/10.1023/A:1011212908144},
  doi          = {10.1023/A:1011212908144},
  timestamp    = {Thu, 17 Sep 2020 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/jolli/Hustadt01.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/lpar/GeorgievaHS01,
  author       = {Lilia Georgieva and
                  Ullrich Hustadt and
                  Renate A. Schmidt},
  editor       = {Robert Nieuwenhuis and
                  Andrei Voronkov},
  title        = {Computational Space Efficiency and Minimal Model Generation for Guarded
                  Formulae},
  booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning, 8th
                  International Conference, {LPAR} 2001, Havana, Cuba, December 3-7,
                  2001, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {2250},
  pages        = {85--99},
  publisher    = {Springer},
  year         = {2001},
  url          = {https://doi.org/10.1007/3-540-45653-8\_6},
  doi          = {10.1007/3-540-45653-8\_6},
  timestamp    = {Sun, 02 Oct 2022 16:11:18 +0200},
  biburl       = {https://dblp.org/rec/conf/lpar/GeorgievaHS01.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/time/HustadtDSFMH01,
  author       = {Ullrich Hustadt and
                  Clare Dixon and
                  Renate A. Schmidt and
                  Michael Fisher and
                  John{-}Jules Ch. Meyer and
                  Wiebe van der Hoek},
  title        = {Reasoning about agents in the {KARO} framework},
  booktitle    = {Eigth International Symposium on Temporal Representation and Reasoning,
                  TIME-01, Civdale del Friuli, Italy, June 14-16, 2001},
  pages        = {206--213},
  publisher    = {{IEEE} Computer Society},
  year         = {2001},
  url          = {https://doi.org/10.1109/TIME.2001.930719},
  doi          = {10.1109/TIME.2001.930719},
  timestamp    = {Sun, 06 Oct 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/time/HustadtDSFMH01.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@incollection{DBLP:books/el/RV01/FermullerLHT01,
  author       = {Christian G. Ferm{\"{u}}ller and
                  Alexander Leitsch and
                  Ullrich Hustadt and
                  Tanel Tammet},
  editor       = {John Alan Robinson and
                  Andrei Voronkov},
  title        = {Resolution Decision Procedures},
  booktitle    = {Handbook of Automated Reasoning (in 2 volumes)},
  pages        = {1791--1849},
  publisher    = {Elsevier and {MIT} Press},
  year         = {2001},
  url          = {https://doi.org/10.1016/b978-044450813-3/50027-8},
  doi          = {10.1016/B978-044450813-3/50027-8},
  timestamp    = {Mon, 16 Sep 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/books/el/RV01/FermullerLHT01.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@ARTICLE{De_Nivelle+Schmidt+Hustadt@IGPL2000,
 AUTHOR  = {De Nivelle, H. and Schmidt, R. A. and Hustadt, U.},
 TITLE   = {Resolution-Based Methods for Modal Logics},
 JOURNAL = {Logic Journal of the IGPL},
 MONTH   = may,
 VOLUME  = {8},
 NUMBER  = {3},
 PAGES   = {265-292},
 ISSN    = {1367-0751},
 YEAR    = {2000},
 URL     = {http://www3.oup.co.uk:80/igpl/Volume_08/Issue_03/pdf/denivelle.pdf},
 ABSTRACT = {In this paper we give an overview of a selection of proof systems for
 propositional modal logics, namely, standard tableaux, 
 modal KE tableaux, modal resolution and translation-based resolution.
 We will concentrate on translation-based resolution methods describing
 different translation-methods and various refinements of resolution.
 We also discuss how tableaux and modal
 resolution methods can be simulated in the general framework of
 resolution.}
}

In this paper we give an overview of a selection of proof systems for propositional modal logics, namely, standard tableaux, modal KE tableaux, modal resolution and translation-based resolution. We will concentrate on translation-based resolution methods describing different translation-methods and various refinements of resolution. We also discuss how tableaux and modal resolution methods can be simulated in the general framework of resolution.

@inproceedings{Ganzinger+Hustadt+Meyer+Schmidt@AiML1998,
 author    = {Harald Ganzinger and
              Ullrich Hustadt and
              Christoph Meyer and
              Renate A. Schmidt},
 title     = {A Resolution-Based Decision Procedure for Extensions of K4},
 year      = {1998},
 pages     = {225-246},
 editor    = {Michael Zakharyaschev and
              Krister Segerberg and
              Maarten de Rijke and
              Heinrich Wansing},
 booktitle = {Advances in Modal Logic 2, papers from the second workshop
              on "Advances in Modal logic," held in Uppsala, Sweden, 1998},
 publisher = {CSLI Publications},
 year      = {2000},
 isbn      = {1-57586-271-9},
 url       = {Ganzinger+Hustadt+Meyer+Schmidt@AiML1998.pdf},
 abstract = {This paper presents a resolution decision procedure for
 transitive propositional modal logics. The procedure combines the
 relational translation method with an ordered chaining calculus
 designed to avoid unnecessary inferences with transitive relations. We
 show the logics K4, KD4 and S4 can be transformed into a bounded class
 of well-structured clauses closed under ordered resolution and
 negative chaining.} 
}

This paper presents a resolution decision procedure for transitive propositional modal logics. The procedure combines the relational translation method with an ordered chaining calculus designed to avoid unnecessary inferences with transitive relations. We show the logics K4, KD4 and S4 can be transformed into a bounded class of well-structured clauses closed under ordered resolution and negative chaining.

@INPROCEEDINGS{Georgieva+Hustadt+Schmidt@FTP2000,
 AUTHOR        = {Georgieva, Lilia and Hustadt, Ullrich and Schmidt, Renate A.},
 TITLE         = {Hyperresolution for Guarded Formulae},
 PAGES         = {101-112},
 YEAR          = {2000},
 BOOKTITLE     = {Proceedings of the Third International Workshop on 
 First-Order Theorem Proving (FTP 2000) [St. Andrews, Scotland, 2-4 July 2000]},
 EDITOR        = {Baumgartner, Peter and Zhang, Hantao},
 PUBLISHER     = {Institut f{\"u}r Informatik, Universit{\"a}t Koblenz-Landau},
 PADDRESS      = {Koblenz, Germany},
 PYEAR         = {2000},
 CADDRESS      = {St. Andrews, Scotland},
 CYEAR         = {2000},
 CMONTH        = jul # {~3--5},
 SERIES        = {Fachberichte Informatik},
 VOLUME        = {5/2000},
 URL           = {Georgieva+Hustadt+Schmidt@FTP2000.pdf},
 ABSTRACT      = {This paper investigates the use of hyperresolution
 as a decision procedure and model builder for guarded formulae. In
 general hyperresolution is not a decision procedure for the entire
 guarded fragment. However we show that there are natural fragements
 which can be decided by hyperresolution. In particular, we prove
 decidability of hyperresolution with or without splitting for the
 fragment GF1- and point out several ways of extending this fragment
 without loosing decidability. As hyperresolution is closely related to
 various tableaux methods the present work is also relevant for
 tableaux methods. We compare our approach to hypertableaux, and
 mention the relationship to other clausal classes which are decidable
 by hyperresolution.}
}

This paper investigates the use of hyperresolution as a decision procedure and model builder for guarded formulae. In general hyperresolution is not a decision procedure for the entire guarded fragment. However we show that there are natural fragements which can be decided by hyperresolution. In particular, we prove decidability of hyperresolution with or without splitting for the fragment GF1- and point out several ways of extending this fragment without loosing decidability. As hyperresolution is closely related to various tableaux methods the present work is also relevant for tableaux methods. We compare our approach to hypertableaux, and mention the relationship to other clausal classes which are decidable by hyperresolution.

@INPROCEEDINGS{Hustadt+Dixon+Schmidt+Fisher@FroCoS2000,
 AUTHOR        = {Hustadt, Ullrich and Dixon, Clare and Schmidt, Renate A. and Fisher, M.},
 TITLE         = {Normal Forms and Proofs in Combined Modal and Temporal Logics},
 BOOKTITLE     = {Proceedings of the Third International Workshop on Frontiers of Combining Systems
 (FroCoS 2000) [Nancy, France, 22-24 March 2000]},
 YEAR          = {2000},
 PUBLISHER     = {Springer},
 PYEAR         = {2000},
 CADDRESS      = {Nancy, France},
 CYEAR         = {2000},
 CMONTH        = mar # {~22--24},
 SERIES        = {LNAI},
 VOLUME        = {1794},
 PAGES         = {73-87},
 URL           = {Hustadt+Dixon+Schmidt+Fisher@FroCoS2000.pdf},
 ABSTRACT      = {Our aim in this paper is to present an approach
 that is general enough to capture a wide range of combinations of
 temporal and modal logics, but still provides viable means for 
 effective theorem proving.}
}

Our aim in this paper is to present an approach that is general enough to capture a wide range of combinations of temporal and modal logics, but still provides viable means for effective theorem proving.

@INCOLLECTION{Hustadt+Schmidt@SAT2000,
 AUTHOR        = {Hustadt, U. and Schmidt, R. A.},
 TITLE         = {Using Resolution for Testing Modal Satisfiability and Building Models},
 BOOKTITLE     = {{SAT2000}: Highlights of Satisfiability Research in the Year 2000},
 PAGES         = {459-483},
 PUBLISHER     = {IOS Press},
 PADDRESS      = {Amsterdam},
 YEAR          = {2000},
 EDITOR        = {Gent, I. and van Maaren, H. and Walsh, T.},
 SERIES        = {Frontiers in Artificial Intelligence and Applications},
 VOLUME        = {63},
 ISBN          = {1-58603-061-2},
 URL           = {Hustadt+Schmidt@SAT2000.pdf},
 ABSTRACT      = {This paper presents a translation-based resolution
 decision procedure for the multi-modal logic K_m(\cap,\cup,\conv)
 defined over families of relations closed under intersection, union
 and converse. The relations may satisfy certain additional frame
 properties. Different from previous resolution decision procedures
 which are based on ordering refinements our procedure is based on a
 selection refinement, the derivations of which correspond to
 derivations of tableaux or sequent proof systems. This procedure has
 the advantage that it can be used both as a satisfiability checker and
 a model builder. We show that tableaux and sequent-style proof systems
 can be polynomially simulated with our procedure. Furthermore, the
 finite model property follows for a number of extended modal logics.} 
}

This paper presents a translation-based resolution decision procedure for the multi-modal logic K_m(∩,∪,o̧nv) defined over families of relations closed under intersection, union and converse. The relations may satisfy certain additional frame properties. Different from previous resolution decision procedures which are based on ordering refinements our procedure is based on a selection refinement, the derivations of which correspond to derivations of tableaux or sequent proof systems. This procedure has the advantage that it can be used both as a satisfiability checker and a model builder. We show that tableaux and sequent-style proof systems can be polynomially simulated with our procedure. Furthermore, the finite model property follows for a number of extended modal logics.

@INPROCEEDINGS{Hustadt+Schmidt@TABLEAUX2000,
 AUTHOR        = {Hustadt, Ullrich and Schmidt, Renate},
 TITLE         = {{MSPASS}: Modal reasoning by translation and first-order resolution},
 PAGES         = {67-71},
 BOOKTITLE     = {Proceedings of the International Conference on
 Automated Reasoning with Analytic Tableaux and Related Methods 
 (TABLEAUX 2000) [St. Andrews, Scotland, 3-7 July 2000]},
 YEAR          = {2000},
 EDITOR        = {Dyckhoff, Roy},
 PUBLISHER     = {Springer},
 PADDRESS      = {Berlin},
 PYEAR         = {2000},
 CADDRESS      = {St. Andrews, Scotland},
 CYEAR         = {2000},
 CMONTH        = jul # {3-7},
 SERIES        = {LNAI},
 VOLUME        = {1847},
 ISBN          = {3-540-67697-X},
 URL           = {Hustadt+Schmidt@TABLEAUX2000.pdf},
 ABSTRACT      = {MSPASS is an extension of the first-order
 theorem prover SPASS, which can be used as a modal logic
 theorem prover, a theorem prover for description
 logics and a theorem prover for the relational calculus.}
}

MSPASS is an extension of the first-order theorem prover SPASS, which can be used as a modal logic theorem prover, a theorem prover for description logics and a theorem prover for the relational calculus.

@INPROCEEDINGS{Schmidt+Hustadt@CADE2000,
 AUTHOR    = {Schmidt, R. A. and Hustadt, U.},
 CMONTH     = jun # {~17--20,},
 CYEAR      = {2000},
 YEAR      = {2000},
 TITLE     = {A Resolution Decision Procedure for Fluted Logic},
 EDITOR    = {McAllester, D.},
 BOOKTITLE = {Proceedings of the 17th International Conference
 on Automated Deduction (CADE-17)</em> [Pittsburgh, USA, 17-20 June2000]},
 SERIES    = {Lecture Notes in Artificial Intelligence},
 VOLUME    = {1831},
 PUBLISHER = {Springer},
 PAGES     = {433-448},
 URL       = {Schmidt+Hustadt@CADE2000.pdf},
 URL       = {http://dx.doi.org/10.1007/10721959_34},
 ABSTRACT = {Fluted logic is a fragment of first-order logic without
 function symbols in which the arguments of atomic subformulae form
 ordered sequences. A consequence of this restriction is that, whereas
 first-order logic is only semi-decidable, fluted logic is decidable.
 In this paper we present a sound, complete and terminating inference
 procedure for fluted logic. Our characterisation of fluted logic is in
 terms of a new class of so-called fluted clauses. We show that this
 class is decidable by an ordering refinement of first-order resolution
 and a new form of dynamic renaming, called separation.} 
}

Fluted logic is a fragment of first-order logic without function symbols in which the arguments of atomic subformulae form ordered sequences. A consequence of this restriction is that, whereas first-order logic is only semi-decidable, fluted logic is decidable. In this paper we present a sound, complete and terminating inference procedure for fluted logic. Our characterisation of fluted logic is in terms of a new class of so-called fluted clauses. We show that this class is decidable by an ordering refinement of first-order resolution and a new form of dynamic renaming, called separation.

@article{DBLP:journals/igpl/HustadtNS00,
  author       = {Ullrich Hustadt and
                  Hans de Nivelle and
                  Renate A. Schmidt},
  title        = {Resolution-Based Methods for Modal Logics},
  journal      = {Log. J. {IGPL}},
  volume       = {8},
  number       = {3},
  pages        = {265--292},
  year         = {2000},
  url          = {https://doi.org/10.1093/jigpal/8.3.265},
  doi          = {10.1093/JIGPAL/8.3.265},
  timestamp    = {Fri, 06 Mar 2020 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/igpl/HustadtNS00.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/arw/GeorgievaHS00,
  author       = {Lilia Georgieva and
                  Ullrich Hustadt and
                  Renate A. Schmidt},
  editor       = {Hans J{\"{u}}rgen Ohlbach and
                  Ulrich Endriss and
                  Odinaldo Rodrigues and
                  Stefan Schlobach},
  title        = {Hyperresolution for Guarded Formulae},
  booktitle    = {Proceedings of the Seventh Workshop on Automated Reasoning, Bridging
                  the Gap between Theory and Practice, King's College London, UK, 20-21
                  July 2000},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {32},
  publisher    = {CEUR-WS.org},
  year         = {2000},
  url          = {https://ceur-ws.org/Vol-32/georgieva.ps.gz},
  timestamp    = {Fri, 10 Mar 2023 16:22:28 +0100},
  biburl       = {https://dblp.org/rec/conf/arw/GeorgievaHS00.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/arw/Hustadt00,
  author       = {Ullrich Hustadt},
  editor       = {Hans J{\"{u}}rgen Ohlbach and
                  Ulrich Endriss and
                  Odinaldo Rodrigues and
                  Stefan Schlobach},
  title        = {Practical Proof Methods for Combined Modal and Temporal Logics},
  booktitle    = {Proceedings of the Seventh Workshop on Automated Reasoning, Bridging
                  the Gap between Theory and Practice, King's College London, UK, 20-21
                  July 2000},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {32},
  publisher    = {CEUR-WS.org},
  year         = {2000},
  url          = {https://ceur-ws.org/Vol-32/hustadt.ps.gz},
  timestamp    = {Fri, 10 Mar 2023 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/arw/Hustadt00.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/SchmidtH00,
  author       = {Renate A. Schmidt and
                  Ullrich Hustadt},
  editor       = {David A. McAllester},
  title        = {A Resolution Decision Procedure for Fluted Logic},
  booktitle    = {Automated Deduction - CADE-17, 17th International Conference on Automated
                  Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {1831},
  pages        = {433--448},
  publisher    = {Springer},
  year         = {2000},
  url          = {https://doi.org/10.1007/10721959\_34},
  doi          = {10.1007/10721959\_34},
  timestamp    = {Tue, 14 May 2019 10:00:39 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/SchmidtH00.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/faabs/HustadtDSFMH00,
  author       = {Ullrich Hustadt and
                  Clare Dixon and
                  Renate A. Schmidt and
                  Michael Fisher and
                  John{-}Jules Ch. Meyer and
                  Wiebe van der Hoek},
  editor       = {James L. Rash and
                  Christopher A. Rouff and
                  Walt Truszkowski and
                  Diana F. Gordon and
                  Michael G. Hinchey},
  title        = {Verification within the {KARO} Agent Theory},
  booktitle    = {Formal Approaches to Agent-Based Systems, First International Workshop,
                  {FAABS} 2000 Greenbelt, MD, USA, April 5-7, 2000, Revised Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1871},
  pages        = {33--47},
  publisher    = {Springer},
  year         = {2000},
  url          = {https://doi.org/10.1007/3-540-45484-5\_3},
  doi          = {10.1007/3-540-45484-5\_3},
  timestamp    = {Sun, 06 Oct 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/faabs/HustadtDSFMH00.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/frocos/HustadtDSF00,
  author       = {Ullrich Hustadt and
                  Clare Dixon and
                  Renate A. Schmidt and
                  Michael Fisher},
  editor       = {H{\'{e}}l{\`{e}}ne Kirchner and
                  Christophe Ringeissen},
  title        = {Normal Forms and Proofs in Combined Modal and Temporal Logics},
  booktitle    = {Frontiers of Combining Systems, Third International Workshop, FroCoS
                  2000, Nancy, France, March 22-24, 2000, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {1794},
  pages        = {73--87},
  publisher    = {Springer},
  year         = {2000},
  url          = {https://doi.org/10.1007/10720084\_6},
  doi          = {10.1007/10720084\_6},
  timestamp    = {Tue, 14 May 2019 10:00:51 +0200},
  biburl       = {https://dblp.org/rec/conf/frocos/HustadtDSF00.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tableaux/HustadtS00,
  author       = {Ullrich Hustadt and
                  Renate A. Schmidt},
  editor       = {Roy Dyckhoff},
  title        = {{MSPASS:} Modal Reasoning by Translation and First-Order Resolution},
  booktitle    = {Automated Reasoning with Analytic Tableaux and Related Methods, International
                  Conference, {TABLEAUX} 2000, St Andrews, Scotland, UK, July 3-7, 2000,
                  Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {1847},
  pages        = {67--71},
  publisher    = {Springer},
  year         = {2000},
  url          = {https://doi.org/10.1007/10722086\_7},
  doi          = {10.1007/10722086\_7},
  timestamp    = {Wed, 25 Sep 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/tableaux/HustadtS00.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@INPROCEEDINGS{Hustadt+Schmidt@CADE1999,
 AUTHOR    = {Hustadt, U. and Schmidt, R. A.},
 YEAR      = {1999},
 TITLE     = {Maslov's Class {K} Revisited},
 EDITOR    = {Ganzinger, H.},
 BOOKTITLE = {Proceedings of the 16th International Conference on Automated Deduction 
 (CADE-16) [Trento, Italy, 7-10 July 1999]},
 SERIES    = {Lecture Notes in Artificial Intelligence},
 VOLUME    = {1632},
 PUBLISHER = {Springer},
 PAGES     = {172-186},
 ISBN      = {3-540-66222-7},
 URL       = {Hustadt+Schmidt@CADE1999.pdf},
 ABSTRACT  = {This paper gives a new treatment of Maslov's class K
 in the framework of resolution. More specifically, we show that K
 and the class DK consisting of disjunction of formulae in K
 can be decided by a resolution refinement based on liftable
 orderings. We also discuss relationships to other solvable and
 unsolvable classes.},
}

This paper gives a new treatment of Maslov's class K in the framework of resolution. More specifically, we show that K and the class DK consisting of disjunction of formulae in K can be decided by a resolution refinement based on liftable orderings. We also discuss relationships to other solvable and unsolvable classes.

@INPROCEEDINGS{Hustadt+Schmidt@IJCAI1999,
 AUTHOR    = {Hustadt, U. and Schmidt, R. A.},
 YEAR      = {1999},
 TITLE     = {On the relation of resolution and tableaux proof systems for description logics},
 EDITOR    = {Dean, Thomas},
 BOOKTITLE = {Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence 
 (IJCAI'99) [Stockholm, Sweden, 31 July-6 August 1999]},
 VOLUME    = {1},
 PUBLISHER = {Morgan Kaufmann},
 PAGES     = {202-207},
 URL       = {Hustadt+Schmidt@IJCAI1999.pdf},
 ABSTRACT  = {This paper investigates the relationship between resolution and
 tableaux proof system for the satisfiability of general
 knowledge bases in the description logic ALC. We show
 that resolution proof systems can polynomially simulate their
 tableaux counterpart. Our resolution proof system is based 
 on a selection refinement and utilises standard redundancy elimination 
 criteria to ensure termination.},
}

This paper investigates the relationship between resolution and tableaux proof system for the satisfiability of general knowledge bases in the description logic ALC. We show that resolution proof systems can polynomially simulate their tableaux counterpart. Our resolution proof system is based on a selection refinement and utilises standard redundancy elimination criteria to ensure termination.

@ARTICLE{Hustadt+Schmidt@JANCL1999,
 AUTHOR  = {Hustadt, U. and Schmidt, R. A.},
 YEAR    = {1999},
 TITLE   = {An Empirical Analysis of Modal Theorem Provers},
 JOURNAL = {Journal of Applied Non-Classical Logics},
 VOLUME  = {9},
 NUMBER  = {4},
 PAGES   = {479-522},
 URL     = {http://dx.doi.org/10.1080/11663081.1999.10510981},
 URL     = {Hustadt+Schmidt@JANCL1999.pdf},
 ABSTRACT = {This paper reports on an empirical performance analysis of
 four modal theorem provers on benchmark suites of randomly generated
 formulae.
 The theorem provers tested are the Davis-Putnam-based procedure
 KSAT, the tableaux-based system KRIS, the sequent-based Logics
 Workbench, and a translation approach combined with the first-order
 theorem prover SPASS.
<p>
 Our benchmark suites are sets of multi-modal formulae in a certain normal 
 form randomly generated according to the scheme of Giunchiglia and 
 Sebastiani [GS96a, GS96b].
 We investigate the quality of the random modal formulae and show
 that the scheme has some shortcomings, which may lead to mistaken
 conclusions.
 We propose improvements to the evaluation method and show that the
 translation approach provides a viable alternative to the other
 approaches.},
}

This paper reports on an empirical performance analysis of four modal theorem provers on benchmark suites of randomly generated formulae. The theorem provers tested are the Davis-Putnam-based procedure KSAT, the tableaux-based system KRIS, the sequent-based Logics Workbench, and a translation approach combined with the first-order theorem prover SPASS.

Our benchmark suites are sets of multi-modal formulae in a certain normal form randomly generated according to the scheme of Giunchiglia and Sebastiani [GS96a, GS96b]. We investigate the quality of the random modal formulae and show that the scheme has some shortcomings, which may lead to mistaken conclusions. We propose improvements to the evaluation method and show that the translation approach provides a viable alternative to the other approaches.

@INPROCEEDINGS{Hustadt+Schmidt@SFTP1998,
 AUTHOR    = {Hustadt, U. and Schmidt, R. A.},
 TITLE     = {Issues of Decidability for Description Logics in the Framework of Resolution},
 EDITOR    = {Caferra, R. and Salzer, G.},
 PAGES     = {192-206},
 PMONTH    = jan,
 PYEAR     = {2000},
 CYEAR     = {1998},
 YEAR      = {1999},
 BOOKTITLE = {Automated Deduction in Classical and Non-Classical Logics},
 SERIES    = {LNAI},
 VOLUME    = {1761},
 PUBLISHER = {Springer},
 URL       = {Hustadt+Schmidt@SFTP1998.pdf},
 URL       = {http://dx.doi.org/10.1007/3-540-46508-1_13},
 ABSTRACT  = {We describe two methods on the basis of which efficient
 resolution decision procedures can be developed for a range of
 description logics. The first method uses an ordering restriction and
 applies to the description logic ALB, which extends ALC with the top
 role, full role negation, role intersection, role disjunction, role
 converse, domain restriction, range restriction, and role hierarchies.
 The second method is based solely on a selection restriction and
 applies to reducts of ALB without the top role and role negation. The
 latter method can be viewed as a polynomial simulation of familiar
 tableaux-based decision procedures. It can also be employed for
 automated model generation.}
}

We describe two methods on the basis of which efficient resolution decision procedures can be developed for a range of description logics. The first method uses an ordering restriction and applies to the description logic ALB, which extends ALC with the top role, full role negation, role intersection, role disjunction, role converse, domain restriction, range restriction, and role hierarchies. The second method is based solely on a selection restriction and applies to reducts of ALB without the top role and role negation. The latter method can be viewed as a polynomial simulation of familiar tableaux-based decision procedures. It can also be employed for automated model generation.

@INPROCEEDINGS{Hustadt+Schmidt+Weidenbach@DL1999,
 AUTHOR    = {Hustadt, U. and Schmidt, R. A. and Weidenbach, C.},
 YEAR      = {1999},
 TITLE     = {{MSPASS}: Subsumption Testing with {SPASS}},
 EDITOR    = {P. Lambrix and A. Borgida and M. Lenzerini and R. M{\"o}ller and P. Patel-Schneider},
 BOOKTITLE = {Proceedings of the International Workshop on Description Logics (DL'99)
 [Link{\"o}ping University, Sweden]},
 PUBLISHER = {Link{\"o}ping University},
 PAGES     = {136-137},
 URL       = {Hustadt+Schmidt+Weidenbach@DL1999.pdf},
 ABSTRACT  = {SPASS is an enhancement of the first-order theorem
 prover SPASS with a translator of modal formulae, formulae of
 description logics, and formulae of the relational calculus into
 first-order logic with equality. SPASS is one of the fastest and most
 sophisticated existing first-order theorem provers and its performance
 compares well with special purpose theorem provers for modal logics,
 description logics and first-order logic, in general.}
}

SPASS is an enhancement of the first-order theorem prover SPASS with a translator of modal formulae, formulae of description logics, and formulae of the relational calculus into first-order logic with equality. SPASS is one of the fastest and most sophisticated existing first-order theorem provers and its performance compares well with special purpose theorem provers for modal logics, description logics and first-order logic, in general.

@PHDTHESIS{Hustadt@UNISB1999,
 AUTHOR        = {Hustadt, Ullrich},
 TITLE         = {Resolution-Based Decision Procedures for Subclasses of First-Order Logic},
 SCHOOL        = {Universit{\"a}t des Saarlandes},
 YEAR          = {1999},
 ADDRESS       = {Saarbr{\"u}cken, Germany},
 MONTH         = nov,
 URL           = {Hustadt@UNISB1999.pdf},
 ABSTRACT      = {This thesis studies decidable fragments of first-order logic which are
 relevant to the field of non-classical logic and knowledge
 representation.
 We show that refinements of resolution based on suitable liftable
 orderings provide decision procedures for the subclasses E<SUP>+</SUP>,
 Maslov's class K, and Maslov's class DK of first-order logic. By the use of 
 semantics-based translation methods  we can embed the description logic ALB
 and extensions of the basic modal logic K into fragments of first-order logic.
 We describe various decision procedures based on ordering refinements
 and selection functions for these fragments and show that a polynomial
 simulation of tableaux-based decision procedures for these logics is
 possible. In the final part of the thesis we develop a benchmark suite 
 and perform an empirical analysis of various modal theorem provers.}
}

This thesis studies decidable fragments of first-order logic which are relevant to the field of non-classical logic and knowledge representation. We show that refinements of resolution based on suitable liftable orderings provide decision procedures for the subclasses E⁺, Maslov's class K, and Maslov's class DK of first-order logic. By the use of semantics-based translation methods we can embed the description logic ALB and extensions of the basic modal logic K into fragments of first-order logic. We describe various decision procedures based on ordering refinements and selection functions for these fragments and show that a polynomial simulation of tableaux-based decision procedures for these logics is possible. In the final part of the thesis we develop a benchmark suite and perform an empirical analysis of various modal theorem provers.

@phdthesis{DBLP:phd/dnb/Hustadt99,
  author       = {Ullrich Hustadt},
  title        = {Resolution based decision procedures for subclasses of first-order
                  logic},
  school       = {Saarland University, Saarbr{\"{u}}cken, Germany},
  year         = {1999},
  url          = {http://scidok.sulb.uni-saarland.de/volltexte/2004/190/index.html},
  urn          = {urn:nbn:de:bsz:291-scidok-1907},
  timestamp    = {Sat, 17 Jul 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/phd/dnb/Hustadt99.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jancl/HustadtS99,
  author       = {Ullrich Hustadt and
                  Renate A. Schmidt},
  title        = {An empirical analysis of modal theorem provers},
  journal      = {J. Appl. Non Class. Logics},
  volume       = {9},
  number       = {4},
  pages        = {479--522},
  year         = {1999},
  url          = {https://doi.org/10.1080/11663081.1999.10510981},
  doi          = {10.1080/11663081.1999.10510981},
  timestamp    = {Sat, 25 Apr 2020 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/jancl/HustadtS99.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/HustadtS99,
  author       = {Ullrich Hustadt and
                  Renate A. Schmidt},
  editor       = {Harald Ganzinger},
  title        = {Maslov's Class {K} Revisited},
  booktitle    = {Automated Deduction - CADE-16, 16th International Conference on Automated
                  Deduction, Trento, Italy, July 7-10, 1999, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {1632},
  pages        = {172--186},
  publisher    = {Springer},
  year         = {1999},
  url          = {https://doi.org/10.1007/3-540-48660-7\_12},
  doi          = {10.1007/3-540-48660-7\_12},
  timestamp    = {Wed, 25 Sep 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/HustadtS99.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/dlog/HustadtSW99,
  author       = {Ullrich Hustadt and
                  Renate A. Schmidt and
                  Christoph Weidenbach},
  editor       = {Patrick Lambrix and
                  Alexander Borgida and
                  Maurizio Lenzerini and
                  Ralf M{\"{o}}ller and
                  Peter F. Patel{-}Schneider},
  title        = {{MSPASS:} Subsumption Testing with {SPASS}},
  booktitle    = {Proceedings of the 1999 International Workshop on Description Logics
                  (DL'99), Link{\"{o}}ping, Sweden, July 30 - August 1, 1999},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {22},
  publisher    = {CEUR-WS.org},
  year         = {1999},
  url          = {https://ceur-ws.org/Vol-22/schmidt.ps},
  timestamp    = {Fri, 10 Mar 2023 16:23:16 +0100},
  biburl       = {https://dblp.org/rec/conf/dlog/HustadtSW99.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/ijcai/HustadtS99,
  author       = {Ullrich Hustadt and
                  Renate A. Schmidt},
  editor       = {Thomas Dean},
  title        = {On the Relation of Resolution and Tableaux Proof Systems for Description
                  Logics},
  booktitle    = {Proceedings of the Sixteenth International Joint Conference on Artificial
                  Intelligence, {IJCAI} 99, Stockholm, Sweden, July 31 - August 6, 1999.
                  2 Volumes, 1450 pages},
  pages        = {110--117},
  publisher    = {Morgan Kaufmann},
  year         = {1999},
  url          = {http://ijcai.org/Proceedings/99-1/Papers/017.pdf},
  timestamp    = {Tue, 20 Aug 2019 16:18:16 +0200},
  biburl       = {https://dblp.org/rec/conf/ijcai/HustadtS99.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@INPROCEEDINGS{Hustadt+Schmidt@FTP1998,
 AUTHOR      = {Hustadt, U. and Schmidt, R. A.},
 TITLE       = {Issues of Decidability for Description Logics in the Framework of Resolution},
 PAGES       = {152-161},
 EDITOR      = {Caferra, R. and Salzer, G.},
 BOOKTITLE   = {Proceedings of the 2nd International Workshop on First-order Theorem Proving (FTP'98)},
 SERIES      = {Technical report},
 VOLUME      = {E1852-GS-981},
 PUBLISHER   = {Technische Universit{\"a}t Wien},
 ADDRESS     = {Vienna, Austria},
 YEAR        = {1998},
 URL         = {Hustadt+Schmidt@FTP1998.pdf},
 ABSTRACT    = {We describe two methods on the basis of which
 efficient resolution decision procedures can be developed for a range
 of description logics. The first method uses an ordering restriction
 and applies to the description logic ALB, which extends ALC with the
 top role, full role negation, role intersection, role disjunction,
 role converse, domain restriction, range restriction, and role
 hierarchies. The second method is based solely on a selection
 restriction and applies to reducts of ALB without the top role and
 role negation. The latter method can be viewed as a polynomial
 simulation of familiar tableaux-based decision procedures. It can also
 be employed for automated model generation.}
}

We describe two methods on the basis of which efficient resolution decision procedures can be developed for a range of description logics. The first method uses an ordering restriction and applies to the description logic ALB, which extends ALC with the top role, full role negation, role intersection, role disjunction, role converse, domain restriction, range restriction, and role hierarchies. The second method is based solely on a selection restriction and applies to reducts of ALB without the top role and role negation. The latter method can be viewed as a polynomial simulation of familiar tableaux-based decision procedures. It can also be employed for automated model generation.

@INPROCEEDINGS{Hustadt+Schmidt@TABLEAUX1998,
 AUTHOR    = {Hustadt, U. and Schmidt, R. A.},
 CMONTH    = may # {~5--8},
 YEAR      = {1998},
 TITLE     = {Simplification and Backjumping in Modal Tableau},
 EDITOR    = {de Swart, H.},
 BOOKTITLE = {Proceedings the the International Conference on 
 Automated Reasoning with Analytic Tableaux and Related Methods
 (TABLEAUX'98) [Oisterwijk, The Netherlands, 5-8 May 1998]},
 SERIES    = {Lecture Notes in Computer Science},
 VOLUME    = {1397},
 PUBLISHER = {Springer},
 PAGES     = {187-201},
 URL       = {Hustadt+Schmidt@TABLEAUX1998.pdf},
 ABSTRACT  = {This paper is concerned with various schemes for enhancing
 the performance of modal tableau procedures. It discusses techniques
 and strategies for dealing with the nondeterminism in tableau calculi, as
 well as simplification and backjumping. Benchmark results obtained with
 randomly generated modal formulae show the effect of combinations of
 different schemes.}
}

This paper is concerned with various schemes for enhancing the performance of modal tableau procedures. It discusses techniques and strategies for dealing with the nondeterminism in tableau calculi, as well as simplification and backjumping. Benchmark results obtained with randomly generated modal formulae show the effect of combinations of different schemes.

@INPROCEEDINGS{HustadtSchmidtWeidenbach98,
 AUTHOR    = {Hustadt, U. and Schmidt, R. A. and Weidenbach, C.},
 CMONTH    = may # {~5--8},
 YEAR      = {1998},
 TITLE     = {Optimised Functional Translation and Resolution},
 EDITOR    = {de Swart, H.},
 BOOKTITLE = {Proceddings of the International Conference on
 Automated Reasoning with Analytic Tableaux and Related Methods
 (TABLEAUX'98) [Oisterwijk, The Netherlands, 5-8 May 1998]},
 SERIES    = {Lecture Notes in Computer Science},
 VOLUME    = {1397},
 PUBLISHER = {Springer},
 PAGES     = {36-37},
 URL       = {Hustadt+Schmidt+Weidenbach@TABLEAUX1998.pdf},
 URL       = {http://dx.doi.org/10.1007/3-540-69778-0_9},
 ABSTRACT  = {This paper describes our approach to modal theorem
 proving. We make use of a first-order theorem prover SPASS and a
 translation of modal logics to path logics via the optimised
 functional translation. Path logics are clausal logics over the
 language of the monadic fragment of sorted first-order logic with a
 special binary function symbol for defining accessibility. Clauses of
 path logics are restricted in that only Skolem terms which are
 constants may occur and the prefix stability property holds. Ordinary
 resolution without any refinement strategies is a decision procedure
 for the path logics associated with K(m) and KT(m). Our decision
 procedure for S4 uses an a priori term depth bound. SPASS uses ordered
 resolution and ordered factoring, it supports splitting and branch
 condensing (splitting amounts to case analysis while branch condensing
 resembles branch pruning in the Logics Workbench), it has an extensive
 set of reduction rules including tautology deletion, subsumption and
 condensing, and it supports dynamic sort theories by additional
 inference and reduction rules.}
}

This paper describes our approach to modal theorem proving. We make use of a first-order theorem prover SPASS and a translation of modal logics to path logics via the optimised functional translation. Path logics are clausal logics over the language of the monadic fragment of sorted first-order logic with a special binary function symbol for defining accessibility. Clauses of path logics are restricted in that only Skolem terms which are constants may occur and the prefix stability property holds. Ordinary resolution without any refinement strategies is a decision procedure for the path logics associated with K(m) and KT(m). Our decision procedure for S4 uses an a priori term depth bound. SPASS uses ordered resolution and ordered factoring, it supports splitting and branch condensing (splitting amounts to case analysis while branch condensing resembles branch pruning in the Logics Workbench), it has an extensive set of reduction rules including tautology deletion, subsumption and condensing, and it supports dynamic sort theories by additional inference and reduction rules.

@inproceedings{DBLP:conf/aiml/GanzingerHMS98,
  author       = {Harald Ganzinger and
                  Ullrich Hustadt and
                  Christoph Meyer and
                  Renate A. Schmidt},
  editor       = {Michael Zakharyaschev and
                  Krister Segerberg and
                  Maarten de Rijke and
                  Heinrich Wansing},
  title        = {A Resolution-Based Decision Procedure for Extensions of {K4}},
  booktitle    = {Advances in Modal Logic 2, papers from the second workshop on "Advances
                  in Modal logic," held in Uppsala, Sweden, 16-18 October 1998},
  pages        = {225--246},
  publisher    = {{CSLI} Publications},
  year         = {1998},
  timestamp    = {Wed, 17 Jan 2024 17:12:17 +0100},
  biburl       = {https://dblp.org/rec/conf/aiml/GanzingerHMS98.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/ftp/HustadtS98,
  author       = {Ullrich Hustadt and
                  Renate A. Schmidt},
  editor       = {Ricardo Caferra and
                  Gernot Salzer},
  title        = {Issues of Decidability for Description Logics in the Framework of
                  Resolution},
  booktitle    = {Automated Deduction in Classical and Non-Classical Logics, Selected
                  Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1761},
  pages        = {191--205},
  publisher    = {Springer},
  year         = {1998},
  url          = {https://doi.org/10.1007/3-540-46508-1\_13},
  doi          = {10.1007/3-540-46508-1\_13},
  timestamp    = {Mon, 05 Feb 2024 20:35:45 +0100},
  biburl       = {https://dblp.org/rec/conf/ftp/HustadtS98.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tableaux/HustadtS98,
  author       = {Ullrich Hustadt and
                  Renate A. Schmidt},
  editor       = {Harrie C. M. de Swart},
  title        = {Simplification and Backjumping in Modal Tableau},
  booktitle    = {Automated Reasoning with Analytic Tableaux and Related Methods, International
                  Conference, {TABLEAUX} '98, Oisterwijk, The Netherlands, May 5-8,
                  1998, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {1397},
  pages        = {187--201},
  publisher    = {Springer},
  year         = {1998},
  url          = {https://doi.org/10.1007/3-540-69778-0\_22},
  doi          = {10.1007/3-540-69778-0\_22},
  timestamp    = {Tue, 14 May 2019 10:00:54 +0200},
  biburl       = {https://dblp.org/rec/conf/tableaux/HustadtS98.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@INPROCEEDINGS{Hustadt+Schmidt@IJCAI1997,
 AUTHOR    = {Hustadt, U. and Schmidt, R. A.},
 MONTH     = {August},
 YEAR      = {1997},
 TITLE     = {On Evaluating Decision Procedures for Modal Logics},
 EDITOR    = {Pollack, M.},
 BOOKTITLE = {Proceedings of the 
 Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97)
 [Nagoya, Japan, 23-29 August 1997]},
 VOLUME    = {1},
 PUBLISHER = {Morgan Kaufmann},
 PAGES     = {202-207},
 URL       = {Hustadt+Schmidt@IJCAI1997.pdf},
 NOTE      = {An extended version is available as Research Report
 MPI-I-97-2-003, Max-Planck-Institut f{\"u}r Informatik,
 Saarbr{\"u}cken, Germany.},
 ABSTRACT = {This paper investigates the evaluation method of decision
 procedures for multi-modal logic proposed by Giunchiglia and
 Sebastiani as an adaptation from the evaluation method of Mitchell et
 al. of decision procedures for propositional logic. We compare three
 different theorem proving approaches, namely, the Davis-Putnam-based
 procedure KSAT, the tableaux-based system KRIS and a translation
 approach combined with first-order resolution. Our results do not
 support the claims of Giunchiglia and Sebastiani concerning the
 computational superiority of KSAT over KRIS, and an easy-hard-easy
 pattern for randomly generated modal formulae.}, 
}

This paper investigates the evaluation method of decision procedures for multi-modal logic proposed by Giunchiglia and Sebastiani as an adaptation from the evaluation method of Mitchell et al. of decision procedures for propositional logic. We compare three different theorem proving approaches, namely, the Davis-Putnam-based procedure KSAT, the tableaux-based system KRIS and a translation approach combined with first-order resolution. Our results do not support the claims of Giunchiglia and Sebastiani concerning the computational superiority of KSAT over KRIS, and an easy-hard-easy pattern for randomly generated modal formulae.

@TECHREPORT{Hustadt+Schmidt@MPII-TR1997,
 AUTHOR        = {Hustadt, Ullrich and Schmidt, Renate A.},
 TITLE         = {On evaluating decision procedures for modal logic},
 INSTITUTION   = {Max-Planck-Institut f{\"u}r Informatik},
 YEAR          = {1997},
 TYPE          = {Research report},
 NUMBER        = {MPI-I-97-2-003},
 ADDRESS       = {Saarbr{\"u}cken, Germany},
 MONTH         = feb,
 URL           = {Hustadt+Schmidt@MPII-TR1997.pdf},
 ABSTRACT      = {This paper reports on empirical performance analysis
 of four modal theorem provers on benchmark suites of randomly
 generated formulae. The theorem provers tested are the
 Davis-Putnam-based procedure KSAT, the tableaux-based system
 KRIS, the sequent-based Logics Workbench, and a
 translation approach combined with the first-order theorem prover
 SPASS.
 <p>
 Our benchmark suites are sets of multi-modal formulae in a certain
 normal form randomly generated according to the scheme of 
 Giunchiglia and Sebastiani (1996a,1996b).
 We investigate the quality of the random modal formulae and show that
 the scheme has some shortcomings, which may lead to mistaken conclusions.
 We propose improvements to the evaluation method 
 and show that the translation approach has superior
 computational behaviour compared to the other three approaches.
 </p>},
}

This paper reports on empirical performance analysis of four modal theorem provers on benchmark suites of randomly generated formulae. The theorem provers tested are the Davis-Putnam-based procedure KSAT, the tableaux-based system KRIS, the sequent-based Logics Workbench, and a translation approach combined with the first-order theorem prover SPASS.

Our benchmark suites are sets of multi-modal formulae in a certain normal form randomly generated according to the scheme of Giunchiglia and Sebastiani (1996a,1996b). We investigate the quality of the random modal formulae and show that the scheme has some shortcomings, which may lead to mistaken conclusions. We propose improvements to the evaluation method and show that the translation approach has superior computational behaviour compared to the other three approaches.

@inproceedings{DBLP:conf/ijcai/HustadtS97,
  author       = {Ullrich Hustadt and
                  Renate A. Schmidt},
  title        = {On Evaluating Decision Procedures for Modal Logic},
  booktitle    = {Proceedings of the Fifteenth International Joint Conference on Artificial
                  Intelligence, {IJCAI} 97, Nagoya, Japan, August 23-29, 1997, 2 Volumes},
  pages        = {202--209},
  publisher    = {Morgan Kaufmann},
  year         = {1997},
  url          = {http://ijcai.org/Proceedings/97-1/Papers/033.pdf},
  timestamp    = {Tue, 20 Aug 2019 16:17:27 +0200},
  biburl       = {https://dblp.org/rec/conf/ijcai/HustadtS97.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@INCOLLECTION{Ohlbach+Schmidt+Hustadt@PTML1996,
 AUTHOR    = {Ohlbach, Hans J{\"u}rgen and Schmidt, Renate A. and Hustadt, Ullrich},
 YEAR      = {1996},
 TITLE     = {Translating Graded Modalities into Predicate Logics},
 EDITOR    = {Wansing, H.},
 BOOKTITLE = {Proof Theory of Modal Logic},
 SERIES    = {Applied Logic Series},
 VOLUME    = {2},
 PUBLISHER = {Kluwer},
 ADDRESS   = {Dordrecht, The Netherlands},
 PAGES     = {253-291},
 URL       = {http://dx.doi.org/10.1007/978-94-017-2798-3_14},
 ABSTRACT  = {In the logic of graded modalities it is possible to talk
  about sets of finite cardinality.  Various calculi exist for graded
  modal logics and all generate vast amounts of case distinctions.  In
  this paper we present an optimized translation from graded modal logic
  into many-sorted predicate logic.  This translation has the advantage
  that in contrast to known approaches our calculus enables us to reason
  with cardinalities of sets symbolically.  In many cases the length of
  proofs for theorems of this calculus is independent of the
  cardinalities. The translation is sound and complete.},
}

In the logic of graded modalities it is possible to talk about sets of finite cardinality. Various calculi exist for graded modal logics and all generate vast amounts of case distinctions. In this paper we present an optimized translation from graded modal logic into many-sorted predicate logic. This translation has the advantage that in contrast to known approaches our calculus enables us to reason with cardinalities of sets symbolically. In many cases the length of proofs for theorems of this calculus is independent of the cardinalities. The translation is sound and complete.

@INPROCEEDINGS{Ohlbach+Schmidt+Hustadt@DL1995,
 AUTHOR    = {Ohlbach, Hans J{\"u}rgen and Schmidt, Renate A. and 
              Hustadt, Ullrich},
 TITLE     = {Symbolic Arithmetical Reasoning with Qualified Number 
              Restrictions},
 BOOKTITLE = {International Workshop on Description Logics (DL'95)
 [Rome, Italy, 2-3 June 1995]},
 PMONTH    = may,
 PYEAR     = {1995},
 EDITOR    = {Borgida, A. and Lenzerini, M. and Nardi, D. and Nebel, B.},
 PAGES     = {89-95},
 CADDRESS  = {Rome, Italy},
 CMONTH    = jun # {~2--3},
 CYEAR     = {1995},
 YEAR      = {1995},
 URL       = {Ohlbach+Schmidt+Hustadt@DL1995.pdf},
 NOTE      = {Proceedings appeared as Technical Report RAP.07.95, Dipartimento di 
              Informatica e Sistemistica, Univ. degli studia di Roma, 
              1995},
 ABSTRACT  = {Many inference systems used for concept description logics 
     are constraint systems that employ tableaux methods. These have the 
     disadvantage that for reasoning with qualified number 
     restrictions n new constant symbols are generated for each concept 
     of the form (atleast n R C). In this paper we present an alternative
     method that avoids the generation of constants and uses a restricted
     form of symbolic arithmetic considerably different from the tableaux
     method. The method we use is introduced in Ohlbach, Schmidt and 
     Hustadt (May 1995) for reasoning with graded modalities. We exploit 
     the exact correspondence between the concept description language 
     ALCN and the multi-modal version of the graded modal logic K and 
     show how the method can be applied to ALCN as well. 
     This paper is a condensed version of Ohlbach et al. (May 1995). We 
     omit proofs and much of the technical details, but we include some 
     examples.}
}

Many inference systems used for concept description logics are constraint systems that employ tableaux methods. These have the disadvantage that for reasoning with qualified number restrictions n new constant symbols are generated for each concept of the form (atleast n R C). In this paper we present an alternative method that avoids the generation of constants and uses a restricted form of symbolic arithmetic considerably different from the tableaux method. The method we use is introduced in Ohlbach, Schmidt and Hustadt (May 1995) for reasoning with graded modalities. We exploit the exact correspondence between the concept description language ALCN and the multi-modal version of the graded modal logic K and show how the method can be applied to ALCN as well. This paper is a condensed version of Ohlbach et al. (May 1995). We omit proofs and much of the technical details, but we include some examples.

@TECHREPORT{Ohlbach+Schmidt+Hustadt@MPII-TR1995.pdf,
 AUTHOR      = {Ohlbach, Hans J{\"u}rgen and Schmidt, Renate A. and 
                Hustadt, Ullrich},
 YEAR        = {1995},
 TITLE       = {Translating Graded Modalities into Predicate Logic},
 TYPE        = {Technical Report},
 NUMBER      = {MPI-I-95-2-008},
 INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
 ADDRESS     = {Saarbr{\"u}cken},
 NOTE        = {Also appeared in H. Wansing, editor, Proof Theory of Modal Logic, 
                Kluwer, 1996.},
 URL         = {Ohlbach+Schmidt+Hustadt@MPII-TR1995.pdf},
 ABSTRACT    = {In the logic of graded modalities it is possible to talk
     about sets of finite cardinality.  Various calculi exist for graded
     modal logics and all generate vast amounts of case distinctions.  In
     this paper we present an optimized translation from graded modal logic
     into many-sorted predicate logic.  This translation has the advantage
     that in contrast to known approaches our calculus enables us to reason
     with cardinalities of sets symbolically.  In many cases the length of
     proofs for theorems of this calculus is independent of the
     cardinalities. The translation is sound and complete.},
}

In the logic of graded modalities it is possible to talk about sets of finite cardinality. Various calculi exist for graded modal logics and all generate vast amounts of case distinctions. In this paper we present an optimized translation from graded modal logic into many-sorted predicate logic. This translation has the advantage that in contrast to known approaches our calculus enables us to reason with cardinalities of sets symbolically. In many cases the length of proofs for theorems of this calculus is independent of the cardinalities. The translation is sound and complete.

@INPROCEEDINGS{Hustadt@KRDB1994,
 AUTHOR        = {Hustadt, Ullrich},
 TITLE         = {Do we need the closed-world assumption in knowledge
representation},
 BOOKTITLE     = {Working Notes of the KI'94 Workshop: Reasoning about 
                  Structured Objects: Knowledge Representation Meets 
                  Databases (KRDB'94) [Saarbr\"ucken, Germany, 20-21 September 1994]},
 EDITOR        = {Baader, Franz and Buchheit, Martin and Jeusfeld, Manfred A.
                  and Nutt, Werner},
 PAGES         = {24-26},
 NOTE          = {Appeared as Document D-94-11, DFKI, Saarbr{\"u}cken, Germany
 as well as CEUR Workshop Proceedings, Vol. 1},
 PMONTH        = nov,
 PYEAR         = {1994},
 CADDRESS      = {Saarbr{\"u}cken, Germany},
 CYEAR         = {1994},
 YEAR          = {1994},
 CMONTH        = sep # {~20--21},
 URL           = {Hustadt@KRDB1994.pdf},
 ABSTRACT      = {In this paper I want to focus on some principal 
     differences between data models of database systems and knowledge 
     representation languages.  
     <p>
     The data manipulation languages of data models are based on the
     closed-world, unique-name, and domain-closure assumption.
     Data manipulation languages and query languages of
     knowledge representation formalisms differ considerably in their
     underlying assumptions. They are based on the open-world, unique-name, 
     and open-domain assumption. 
     That means, that even if the data definition language and the data
     manipulation language of a database management system and a knowledge
     base management system would coincide, the results of data
     manipulations would differ. 
     </p>r
     I present some examples that show the usefulness
     of closed-world inferences in natural language processing. Thus
     knowledge representation languages sticking to the open-world
     assumption seem to be insufficient for natural language processing.}
}

In this paper I want to focus on some principal differences between data models of database systems and knowledge representation languages.

The data manipulation languages of data models are based on the closed-world, unique-name, and domain-closure assumption. Data manipulation languages and query languages of knowledge representation formalisms differ considerably in their underlying assumptions. They are based on the open-world, unique-name, and open-domain assumption. That means, that even if the data definition language and the data manipulation language of a database management system and a knowledge base management system would coincide, the results of data manipulations would differ.

r I present some examples that show the usefulness of closed-world inferences in natural language processing. Thus knowledge representation languages sticking to the open-world assumption seem to be insufficient for natural language processing.

@INPROCEEDINGS{Hustadt@MEP-KI1994,
 AUTHOR        = {Hustadt, Ullrich},
 TITLE         = {Common and Mutual Belief for Agent Modeling},
 BOOKTITLE     = {{KI-94} Workshops: Extended Abstracts},
 EDITOR        = {Kunze, J{\"u}rgen and Stoyan, Herbert},
 CADDRESS      = {Saarbr{\"u}cken, Germany},
 CYEAR         = {1994},
 CMONTH        = sep # {~18--23},
 PYEAR         = {1994},
 PMONTH        = sep,
 PAGES         = {123--124},
 PUBLISHER     = {Gesellschaft f{\"u}r Informatik e. V.},
 PADDRESS      = {Bonn},
 PYEAR         = {1994},
 YEAR          = {1994},
 URL           = {Hustadt@MEP-KI1994.pdf},
 ABSTRACT      = {In this paper we consider a dialog situation between
 a system and a heterogeneous group of dialog partners. Our problem is
 to find adequate representational means for describing the beliefs,
 goals, and plans of each agent. We assume that we can provide a
 sufficiently detailed description of the knowledge base of the system,
 but we don't have complete descriptions of the knowledge bases of all
 other participating agents.  To provide the initial knowledge base for
 these agents, we support mutual and common group beliefs, knowledge,
 and desires.}
}

In this paper we consider a dialog situation between a system and a heterogeneous group of dialog partners. Our problem is to find adequate representational means for describing the beliefs, goals, and plans of each agent. We assume that we can provide a sufficiently detailed description of the knowledge base of the system, but we don't have complete descriptions of the knowledge bases of all other participating agents. To provide the initial knowledge base for these agents, we support mutual and common group beliefs, knowledge, and desires.

@INPROCEEDINGS{Hustadt94d,
 AUTHOR        = {Hustadt, Ullrich},
 TITLE         = {A Multi-Modal Logic for Stereotyping},
 BOOKTITLE     = {Proceedings of the Fourth International
                  Conference on User Modeling (UM94)
 [Hyannis, MA, USA, 15-19 August 1994]},
 CADDRESS      = {Hyannis, MA, USA}, 
 CMONTH        = aug # {~15--19},
 CYEAR         = {1994},
 YEAR          = {1994},
 PAGES         = {87-92},
 PYEAR         = {1994},
 PMONTH        = aug,
 PUBLISHER     = {The MITRE Corporation},
 XNOTE         = {Order copies from: Bradley A. Goodman, The MITRE Corporation,
                  Artificial Intelligence Center, 202 Burlingtom Road, 
                  Bedford, MA 01730-1420, USA},
 URL           = {Hustadt@UM1994.pdf},
 ABSTRACT      = {In a mixed-initiative dialogue between multiple 
     interlocutors, the ability to construct, to maintain, and to exploit an 
     explicit model of the dialogue partners' beliefs, goals, and plans is 
     indispensable. 
     An \emph{agent model} is required for identifying the objects which the
     dialogue partner is talking about, for planning the appropriate dialogue
     contributions towards achieving the own goals, and for determining the
     effects of planned dialogue contributions on the dialogue partner.}
}

In a mixed-initiative dialogue between multiple interlocutors, the ability to construct, to maintain, and to exploit an explicit model of the dialogue partners' beliefs, goals, and plans is indispensable. An \emphagent model is required for identifying the objects which the dialogue partner is talking about, for planning the appropriate dialogue contributions towards achieving the own goals, and for determining the effects of planned dialogue contributions on the dialogue partner.

@inproceedings{DBLP:conf/krdb/Hustadt94,
  author       = {Ullrich Hustadt},
  editor       = {Franz Baader and
                  Martin Buchheit and
                  Manfred A. Jeusfeld and
                  Werner Nutt},
  title        = {Do we need the closed world assumption in knowledge representation?},
  booktitle    = {Reasoning about Structured Objects: Knowledge Representation Meets
                  Databases, Proceedings of 1st Workshop KRDB'94, Saarbr{\"{u}}cken,
                  Germany, September 20-22, 1994},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {1},
  publisher    = {CEUR-WS.org},
  year         = {1994},
  url          = {https://ceur-ws.org/Vol-1/hustadt-long.ps},
  timestamp    = {Fri, 10 Mar 2023 16:23:33 +0100},
  biburl       = {https://dblp.org/rec/conf/krdb/Hustadt94.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@INPROCEEDINGS{Hustadt@ICLP-ARW1993,
 AUTHOR        = {Hustadt, Ullrich},
 TITLE         = {Abductive Disjunctive Logic Programming},
 BOOKTITLE     = {Proceedings of the ICLP 93 Postconference Workshop on Abductive Reasoning
 [Budapest, Hungary, 24-25 June 1993]},
 YEAR          = {1993},
 EDITOR        = {Codognet, Philippe and Dung, Phan Minh and Kakas, 
                  Antonis C. and Mancarella, Paola},
 CADDRESS      = {Budapest, Hungary},
 CMONTH        = June # {~24--25},
 URL           = {Hustadt@ICLP-ARW1993.pdf},
 ABSTRACT      = {Eshghi and Kowalski (1989) introduced the notion of an 
     abductive framework and proposed stable models as a semantics for 
     abduction. They showed that abductive frameworks can be used to provide 
     an alternative basis for negation-as-failure in logic programming. Kakas 
     and Mancarella (1990) introduced the notion of generalized stable models 
     by suitably extending the definition of stable models. The semantics of
     generalized stable models clarifies the meaning of integrity constraints
     within an abductive framework.
     In (Satoh and Iwayama, 1992) a goal-directed method for computing 
     the generalized stable models of an abductive framework has been
     proposed. Their method is correct for any consistent abductive
     framework. Whereas abductive frameworks correspond to normal logic
     programs with integrity constraints, I propose an extension to
     disjunctive normal logic programs. Disjunctive normal logic programs 
     extend normal logic programs to disjunctive logic programs and
     therefore, provide full first-order expressibility.}
}

Eshghi and Kowalski (1989) introduced the notion of an abductive framework and proposed stable models as a semantics for abduction. They showed that abductive frameworks can be used to provide an alternative basis for negation-as-failure in logic programming. Kakas and Mancarella (1990) introduced the notion of generalized stable models by suitably extending the definition of stable models. The semantics of generalized stable models clarifies the meaning of integrity constraints within an abductive framework. In (Satoh and Iwayama, 1992) a goal-directed method for computing the generalized stable models of an abductive framework has been proposed. Their method is correct for any consistent abductive framework. Whereas abductive frameworks correspond to normal logic programs with integrity constraints, I propose an extension to disjunctive normal logic programs. Disjunctive normal logic programs extend normal logic programs to disjunctive logic programs and therefore, provide full first-order expressibility.

@INPROCEEDINGS{Hustadt@MEP-KI1993,
 AUTHOR        = {Hustadt, Ullrich},
 TITLE         = {Automated Support for the Development of 
Non-Classical Logics},
 BOOKTITLE     = {Modeling Epistemic Propositions: Workshop during the 
                  17th German Conference on Artificial Intelligence (KI'93)
                  [Berlin, Germany, 13-14 September 1993]},
 EDITOR        = {B{\"u}rckert, Hans-J{\"u}rgen and Nutt, Werner},
 ADDRESS      = {Berlin, Germany},
 CYEAR         = {1993},
 CMONTH        =  sep # {13-14},
 YEAR          = {1993},
 NOTE          = {Available as DFKI Document D-93-25, DFKI, Saarbr{\"u}cken, 
                  Germany},
 PYEAR         = {1993},
 PMONTH        = dec,
 URL           = {Hustadt@MEP-KI1993.pdf},
 ABSTRACT      = {The most natural means for specifying a non-classical 
     logic is by means of a Hilbert calculus. Usually, the semantics of a 
     non-classical logic is given in terms of possible worlds. 
     Given an axiomatization of a non-classical logics,  the 
     \emph{correspondence problem} in these logics is to find for every given 
     Hilbert axiom an equivalent property of the accessibility 
     relation (van Benthem (1984)). 
     For mechanizing deduction in non-classical logics it is very 
     important to find these correspondences (Ohlbach (1991)).
     So far the method for finding the correspondences was mostly by 
     intuition and the verification required complex proofs 
     (van Benthem (1984)).
     \par
     Whereas KRIS is a single-agent knowledge representation 
     system, i. e. KRIS is only able to represent general world
     knowledge or the knowledge of one agent about the world, MOTEL is a
     multi-agent knowledge representation system. The MOTEL language allows
     modal contexts and modal concept forming operators which
     allow to represent and reason about the believes and wishes of
     multiple agents. Furthermore it is possible to represent defaults and
     stereotypes.}
}

The most natural means for specifying a non-classical logic is by means of a Hilbert calculus. Usually, the semantics of a non-classical logic is given in terms of possible worlds. Given an axiomatization of a non-classical logics, the \emphcorrespondence problem in these logics is to find for every given Hilbert axiom an equivalent property of the accessibility relation (van Benthem (1984)). For mechanizing deduction in non-classical logics it is very important to find these correspondences (Ohlbach (1991)). So far the method for finding the correspondences was mostly by intuition and the verification required complex proofs (van Benthem (1984)). \par Whereas KRIS is a single-agent knowledge representation system, i. e. KRIS is only able to represent general world knowledge or the knowledge of one agent about the world, MOTEL is a multi-agent knowledge representation system. The MOTEL language allows modal contexts and modal concept forming operators which allow to represent and reason about the believes and wishes of multiple agents. Furthermore it is possible to represent defaults and stereotypes.

@INPROCEEDINGS{Hustadt+Nonnengart@AI1993,
 AUTHOR        = {Hustadt, Ullrich and Nonnengart, Andreas},
 TITLE         = {Modalities in Knowledge Representation},
 BOOKTITLE     = {Proceedings of the 6th Australian Joint Conference 
 on Artificial Intelligence (AI'93) 
 [Melbourne, Australia, 16-19 November 1993]},
 PAGES         = {249-254},
 EDITOR        = {Rowles, Chris and Liu, Huan and Foo, Norman},
 CMONTH         = {16-19~} # nov ,
 CADDRESS       = {Melbourne, Australia},
 YEAR          = {1993},
 PUBLISHER     = {World Scientific},
 URL           = {Hustadt+Nonnengart@AI1993.pdf},
 ABSTRACT      = {Standard knowledge representation systems are supposed 
 to be able to represent either common or individual knowledge 
 about the world. In this paper we propose an extension to 
 such knowledge representation systems which, in a uniform 
 manner, allows to express beliefs of multiple agents as 
 well as knowledge, desire, time and in fact any modality 
 which has a first-order predicate logic possible world semantics.},
}

Standard knowledge representation systems are supposed to be able to represent either common or individual knowledge about the world. In this paper we propose an extension to such knowledge representation systems which, in a uniform manner, allows to express beliefs of multiple agents as well as knowledge, desire, time and in fact any modality which has a first-order predicate logic possible world semantics.

@TECHREPORT{Hustadt+Nonnengart+Schmidt+Timm@MPII-TR1992,
 AUTHOR      = {Hustadt, U. and Nonnengart, A. and Schmidt, R. and Timm, J.}, 
 TITLE       = {MOTEL User Manual},
 YEAR        = {1992},
 INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
 NUMBER      = {MPI-I-92-236},
 TYPE        = {Technical Report},
 URL         = {Hustadt+Nonnengart+Schmidt+Timm@MPII-TR1993.pdf},
 ABSTRACT    = {MOTEL is a logic-based knowledge representation languages 
     of the KL-ONE family. It contains as a kernel the KRIS
     language which is a decidable sublanguage of first-order 
     predicate logic (see Baader and Hollunder (1990)). Whereas 
     KRIS is a single-agent knowledge representation 
     system, i.e. KRIS is only able to represent general 
     world knowledge or the knowledge of one agent about the 
     world, MOTEL is a multi-agent knowledge representation 
     system. The MOTEL language allows modal contexts and modal 
     concept forming operators which allow to represent and 
     reason about the believes and wishes of multiple agents. 
     Furthermore it is possible to represent defaults and stereotypes. 
     Beside the basic resoning facilities for consistency checking, 
     classification, and realization, MOTEL provides an abductive 
     inference mechanism. Furthermore it is able to give explanations 
     for its inferences.},
}

MOTEL is a logic-based knowledge representation languages of the KL-ONE family. It contains as a kernel the KRIS language which is a decidable sublanguage of first-order predicate logic (see Baader and Hollunder (1990)). Whereas KRIS is a single-agent knowledge representation system, i.e. KRIS is only able to represent general world knowledge or the knowledge of one agent about the world, MOTEL is a multi-agent knowledge representation system. The MOTEL language allows modal contexts and modal concept forming operators which allow to represent and reason about the believes and wishes of multiple agents. Furthermore it is possible to represent defaults and stereotypes. Beside the basic resoning facilities for consistency checking, classification, and realization, MOTEL provides an abductive inference mechanism. Furthermore it is able to give explanations for its inferences.