@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.