2 Search Results for "Bolander, Thomas"

Document
DOI: 10.4230/LIPIcs.TYPES.2020.5
Synthetic Completeness for a Terminating Seligman-Style Tableau System

Authors: Asta Halkjær From

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract
Hybrid logic extends modal logic with nominals that name worlds. Seligman-style tableau systems for hybrid logic divide branches into blocks named by nominals to achieve a local proof style. We present a Seligman-style tableau system with a formalization in the proof assistant Isabelle/HOL. Our system refines an existing system to simplify formalization and we claim termination from this relationship. Existing completeness proofs that account for termination are either analytic or based on translation, but synthetic proofs have been shown to generalize to richer logics and languages. Our main result is the first synthetic completeness proof for a terminating hybrid logic tableau system. It is also the first formalized completeness proof for any hybrid logic proof system.
Cite as

Asta Halkjær From. Synthetic Completeness for a Terminating Seligman-Style Tableau System. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{from:LIPIcs.TYPES.2020.5,
  author =	{From, Asta Halkj{\ae}r},
  title =	{{Synthetic Completeness for a Terminating Seligman-Style Tableau System}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.5},
  URN =		{urn:nbn:de:0030-drops-138847},
  doi =		{10.4230/LIPIcs.TYPES.2020.5},
  annote =	{Keywords: Hybrid logic, Seligman-style tableau, synthetic completeness, Isabelle/HOL}
}
Document
DOI: 10.4230/DagRep.7.6.1
Epistemic Planning (Dagstuhl Seminar 17231)

Authors: Chitta Baral, Thomas Bolander, Hans van Ditmarsch, and Sheila McIlrath

Published in: Dagstuhl Reports, Volume 7, Issue 6 (2018)

Abstract
The seminar Epistemic Planning brought together the research communities of Dynamic Epistemic Logic, Knowledge Representation and Reasoning, and Automated Planning to address fundamental problems on the topic of epistemic planning. In the context of this seminar, dynamic epistemic logic investigates the formal semantics of communication and communicative actions, knowledge representation and reasoning focuses on theories of action and change, and automated planning investigates computational techniques and tools to generate plans. The original goals of the seminar were to develop benchmarks for epistemic planning, to explore the relationship between knowledge and belief in multi-agent epistemic planning, to develop models of agency and capability in epistemic planning and to explore action types and their representations (these originally separate goals were merged during the seminar), and finally to identify practical tools and resources. An additional goal explored during the workshop was the correspondence between planning problems and games.
Cite as

Chitta Baral, Thomas Bolander, Hans van Ditmarsch, and Sheila McIlrath. Epistemic Planning (Dagstuhl Seminar 17231). In Dagstuhl Reports, Volume 7, Issue 6, pp. 1-47, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{baral_et_al:DagRep.7.6.1,
  author =	{Baral, Chitta and Bolander, Thomas and van Ditmarsch, Hans and McIlrath, Sheila},
  title =	{{Epistemic Planning (Dagstuhl Seminar 17231)}},
  pages =	{1--47},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{7},
  number =	{6},
  editor =	{Baral, Chitta and Bolander, Thomas and van Ditmarsch, Hans and McIlrath, Sheila},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.7.6.1},
  URN =		{urn:nbn:de:0030-drops-82857},
  doi =		{10.4230/DagRep.7.6.1},
  annote =	{Keywords: Automated Planning, Knowledge Representation and Reasoning, Reasoning About Actions, Dynamic Epistemic Logic, Multi-Agent Systems}
}
  • Refine by Author
  • 1 Baral, Chitta
  • 1 Bolander, Thomas
  • 1 From, Asta Halkjær
  • 1 McIlrath, Sheila
  • 1 van Ditmarsch, Hans

  • Refine by Classification
  • 1 Theory of computation → Modal and temporal logics

  • Refine by Keyword
  • 1 Automated Planning
  • 1 Dynamic Epistemic Logic
  • 1 Hybrid logic
  • 1 Isabelle/HOL
  • 1 Knowledge Representation and Reasoning
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2017
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact