4 Search Results for "Hansen, Jörg"

Document
DOI: 10.4230/LIPIcs.RTA.2015.143
A Coinductive Framework for Infinitary Rewriting and Equational Reasoning

Authors: Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.
Cite as

Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva. A Coinductive Framework for Infinitary Rewriting and Equational Reasoning. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 143-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{endrullis_et_al:LIPIcs.RTA.2015.143,
  author =	{Endrullis, J\"{o}rg and Hansen, Helle Hvid and Hendriks, Dimitri and Polonsky, Andrew and Silva, Alexandra},
  title =	{{A Coinductive Framework for Infinitary Rewriting and Equational Reasoning}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{143--159},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.143},
  URN =		{urn:nbn:de:0030-drops-51949},
  doi =		{10.4230/LIPIcs.RTA.2015.143},
  annote =	{Keywords: infinitary rewriting, coinduction}
}
Document
DOI: 10.4230/OASIcs.SSV.2011.32
Adaptable Value-Set Analysis for Low-Level Code

Authors: Jörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, and Mads Chr. Olesen

Published in: OASIcs, Volume 24, 6th International Workshop on Systems Software Verification (2012)

Abstract
This paper presents a framework for binary code analysis that uses only SAT-based algorithms. Within the framework, incremental SAT solving is used to perform a form of weakly relational value-set analysis in a novel way, connecting the expressiveness of the value sets to computational complexity. Another key feature of our framework is that it translates the semantics of binary code into an intermediate representation. This allows for a straightforward translation of the program semantics into Boolean logic and eases the implementation efforts, too. We show that leveraging the efficiency of contemporary SAT solvers allows us to prove interesting properties about medium-sized microcontroller programs.
Cite as

Jörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, and Mads Chr. Olesen. Adaptable Value-Set Analysis for Low-Level Code. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 32-43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{brauer_et_al:OASIcs.SSV.2011.32,
  author =	{Brauer, J\"{o}rg and Hansen, Ren\'{e} Rydhof and Kowalewski, Stefan and Larsen, Kim G. and Olesen, Mads Chr.},
  title =	{{Adaptable Value-Set Analysis for Low-Level Code}},
  booktitle =	{6th International Workshop on Systems Software Verification},
  pages =	{32--43},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-36-1},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{24},
  editor =	{Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.32},
  URN =		{urn:nbn:de:0030-drops-35884},
  doi =		{10.4230/OASIcs.SSV.2011.32},
  annote =	{Keywords: Abstract interpretation, SAT solving, embedded systems}
}
Document
DOI: 10.4230/DagSemProc.07122.25
Prioritized Conditional Imperatives:Problems and a New Proposal

Authors: Jörg Hansen

Published in: Dagstuhl Seminar Proceedings, Volume 7122, Normative Multi-agent Systems (2007)

Abstract
The sentences of deontic logic may be understood as describing what an agent ought to do when faced with a given set of norms. If these norms come into conflict, the best the agent can be expected to do is to follow a maximal subset of the norms. Intuitively, a priority ordering of the norms can be helpful in determining the relevant sets and resolve conflicts, but a formal resolution mechanism has been difficult to provide. In particular, reasoning about prioritized conditional imperatives is overshadowed by problems such as the `order puzzle' that are not satisfactorily resolved by existing approaches. The paper provides a new proposal as to how these problems may be overcome.
Cite as

Jörg Hansen. Prioritized Conditional Imperatives:Problems and a New Proposal. In Normative Multi-agent Systems. Dagstuhl Seminar Proceedings, Volume 7122, pp. 1-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{hansen:DagSemProc.07122.25,
  author =	{Hansen, J\"{o}rg},
  title =	{{Prioritized Conditional Imperatives:Problems and a New Proposal}},
  booktitle =	{Normative Multi-agent Systems},
  pages =	{1--30},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7122},
  editor =	{Guido Boella and Leon van der Torre and Harko Verhagen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07122.25},
  URN =		{urn:nbn:de:0030-drops-9147},
  doi =		{10.4230/DagSemProc.07122.25},
  annote =	{Keywords: Deontic logic, default logic, priorities, logic of imperatives}
}
Document
DOI: 10.4230/DagSemProc.07122.28
Ten Philosophical Problems in Deontic Logic

Authors: Jörg Hansen, Gabriella Pigozzi, and Leendert van der Torre

Published in: Dagstuhl Seminar Proceedings, Volume 7122, Normative Multi-agent Systems (2007)

Abstract
The paper discusses ten philosophical problems in deontic logic: how to formally represent norms, when a set of norms may be termed `coherent', how to deal with normative conflicts, how contrary-to-duty obligations can be appropriately modeled, how dyadic deontic operators may be redefined to relate to sets of norms instead of preference relations between possible worlds, how various concepts of permission can be accommodated, how meaning postulates and counts-as conditionals can be taken into account, and how sets of norms may be revised and merged. The problems are discussed from the viewpoint of input/output logic as developed by van der Torre Makinson. We argue that norms, not ideality, should take the central position in deontic semantics, and that a semantics that represents norms, as input/output logic does, provides helpful tools for analyzing, clarifying and solving the problems of deontic logic.
Cite as

Jörg Hansen, Gabriella Pigozzi, and Leendert van der Torre. Ten Philosophical Problems in Deontic Logic. In Normative Multi-agent Systems. Dagstuhl Seminar Proceedings, Volume 7122, pp. 1-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{hansen_et_al:DagSemProc.07122.28,
  author =	{Hansen, J\"{o}rg and Pigozzi, Gabriella and van der Torre, Leendert},
  title =	{{Ten Philosophical Problems in Deontic Logic}},
  booktitle =	{Normative Multi-agent Systems},
  pages =	{1--26},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7122},
  editor =	{Guido Boella and Leon van der Torre and Harko Verhagen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07122.28},
  URN =		{urn:nbn:de:0030-drops-9413},
  doi =		{10.4230/DagSemProc.07122.28},
  annote =	{Keywords: Deontic logic, normative systems, input/output logic}
}
  • Refine by Author
  • 2 Hansen, Jörg
  • 1 Brauer, Jörg
  • 1 Endrullis, Jörg
  • 1 Hansen, Helle Hvid
  • 1 Hansen, René Rydhof
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 Deontic logic
  • 1 Abstract interpretation
  • 1 SAT solving
  • 1 coinduction
  • 1 default logic
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2007
  • 1 2012
  • 1 2015

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