14 Search Results for "Herzig, Andreas"

Document
DOI: 10.4230/OASIcs.Programming.2025.20
On the Effectiveness of Interpreter-Guided Compiler Testing

Authors: Federico Lochbaum and Guillermo Polito

Published in: OASIcs, Volume 134, Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)

Abstract
Guaranteeing that a compiler behaves correctly is a complex task often approached through test generation and fuzzing. Compiler test generation must not only ensure that a compiler generates code that does not break, but also that it implements the programming language semantics. Recently, interpreter-guided test generation has been proposed to test JIT compilers: Concolic-execution on the interpreter yields test cases for the language semantics which are then validated between differential testing of the interpreter and compiler. In previous work, this solution has been shown to find interpreter/compiler differences. However, little has been said about the effectiveness and the solution limits. In this paper we study the behavior of this technique, to shed light on future improvements and research. We experiment with this technique on the JIT compiler for the Pharo programming language, on two different backends: ARMv7 and x86. We explore how effective the solution is in terms of compiler coverage and its limitations, and we discuss how future research can overcome them. Moreover, we investigate how this technique combined with random constraint mutations increases backend compiler coverage.
Cite as

Federico Lochbaum and Guillermo Polito. On the Effectiveness of Interpreter-Guided Compiler Testing. In Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025). Open Access Series in Informatics (OASIcs), Volume 134, pp. 20:1-20:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lochbaum_et_al:OASIcs.Programming.2025.20,
  author =	{Lochbaum, Federico and Polito, Guillermo},
  title =	{{On the Effectiveness of Interpreter-Guided Compiler Testing}},
  booktitle =	{Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)},
  pages =	{20:1--20:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-382-9},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{134},
  editor =	{Edwards, Jonathan and Perera, Roly and Petricek, Tomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Programming.2025.20},
  URN =		{urn:nbn:de:0030-drops-243040},
  doi =		{10.4230/OASIcs.Programming.2025.20},
  annote =	{Keywords: Virtual Machines, Concolic Testing, JIT compilers, interpreters, Differential Testing, Constraint Mutations, Compiler Coverage}
}
Document
DOI: 10.4230/OASIcs.Programming.2025.8
Fuzzing as Editor Feedback

Authors: Marcel Garus, Jens Lincke, and Robert Hirschfeld

Published in: OASIcs, Volume 134, Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)

Abstract
Live programming requires concrete examples, but coming up with examples takes effort. However, there are ways to execute code without specifying examples, such as fuzzing. Fuzzing is a technique that synthesizes program inputs to find bugs in security-critical software. While fuzzing focuses on finding crashes, it also produces valid inputs as a byproduct. Our approach is to make use of this to show examples, including edge cases, directly in the editor. To provide examples for individual pieces of code, we implement fuzzing at the granularity of functions. We integrate it into the compiler pipeline and language tooling of Martinaise, a custom programming language with a limited feature set. Initially, our examples are random and then mutate based on coverage feedback to reach interesting code locations and become smaller. We evaluate our tool in small case studies, showing generated examples for numbers, strings, and composite objects. Our fuzzed examples still feel synthetic, but since they are grounded in the dynamic behavior of code, they can cover the entire execution and show edge cases.
Cite as

Marcel Garus, Jens Lincke, and Robert Hirschfeld. Fuzzing as Editor Feedback. In Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025). Open Access Series in Informatics (OASIcs), Volume 134, pp. 8:1-8:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{garus_et_al:OASIcs.Programming.2025.8,
  author =	{Garus, Marcel and Lincke, Jens and Hirschfeld, Robert},
  title =	{{Fuzzing as Editor Feedback}},
  booktitle =	{Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)},
  pages =	{8:1--8:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-382-9},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{134},
  editor =	{Edwards, Jonathan and Perera, Roly and Petricek, Tomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Programming.2025.8},
  URN =		{urn:nbn:de:0030-drops-242926},
  doi =		{10.4230/OASIcs.Programming.2025.8},
  annote =	{Keywords: Fuzzing, Example-based Programming, Babylonian Programming, Dynamic Analysis, Code Coverage, Randomized Testing, Function-Level Fuzzing}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.17
Description Complexity of Unary Structures in First-Order Logic with Links to Entropy

Authors: Reijo Jaakkola, Antti Kuusisto, and Miikka Vilander

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
The description complexity of a model is the length of the shortest formula that defines the model. We study the description complexity of unary structures in first-order logic FO, also drawing links to semantic complexity in the form of entropy. The class of unary structures provides, e.g., a simple way to represent tabular Boolean data sets as relational structures. We define structures with FO-formulas that are strictly linear in the size of the model as opposed to using the naive quadratic ones, and we use arguments based on formula size games to obtain related lower bounds for description complexity. For a typical structure the upper and lower bounds in fact match up to a sublinear term, leading to a precise asymptotic result on the expected description complexity of a randomly selected structure. We then give bounds on the relationship between Shannon entropy and description complexity. We extend this relationship also to Boltzmann entropy by establishing an asymptotic match between the two entropies. Despite the simplicity of unary structures, our arguments require the use of formula size games, Stirling’s approximation and Chernoff bounds.
Cite as

Reijo Jaakkola, Antti Kuusisto, and Miikka Vilander. Description Complexity of Unary Structures in First-Order Logic with Links to Entropy. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jaakkola_et_al:LIPIcs.CSL.2025.17,
  author =	{Jaakkola, Reijo and Kuusisto, Antti and Vilander, Miikka},
  title =	{{Description Complexity of Unary Structures in First-Order Logic with Links to Entropy}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{17:1--17:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.17},
  URN =		{urn:nbn:de:0030-drops-227749},
  doi =		{10.4230/LIPIcs.CSL.2025.17},
  annote =	{Keywords: formula size, finite model theory, formula size games, entropy, randomness}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.9
On Homogeneous Models of Fluted Languages

Authors: Daumantas Kojelis

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We study the fluted fragment of first-order logic which is often viewed as a multi-variable non-guarded extension to various systems of description logics lacking role-inverses. In this paper we show that satisfiable fluted sentences (even under reasonable extensions) admit special kinds of "nice" models which we call globally/locally homogeneous. Homogeneous models allow us to simplify methods for analysing fluted logics with counting quantifiers and establish a novel result for the decidability of the (finite) satisfiability problem for the fluted fragment with periodic counting. More specifically, we will show that the (finite) satisfiability problem for the language is Tower-complete. If only two variable are used, computational complexity drops to NExpTime-completeness. We supplement our findings by showing that generalisations of fluted logics, such as the adjacent fragment, have finite and general satisfiability problems which are, respectively, Σ⁰₁- and Π⁰₁-complete. Additionally, satisfiability becomes Σ¹₁-complete if periodic counting quantifiers are permitted.
Cite as

Daumantas Kojelis. On Homogeneous Models of Fluted Languages. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kojelis:LIPIcs.CSL.2025.9,
  author =	{Kojelis, Daumantas},
  title =	{{On Homogeneous Models of Fluted Languages}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{9:1--9:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.9},
  URN =		{urn:nbn:de:0030-drops-227669},
  doi =		{10.4230/LIPIcs.CSL.2025.9},
  annote =	{Keywords: Fluted Fragment, Fluted Logic, Fluted Fragment with Periodic Counting, Adjacent Fragment, Adjacent Fragment with Counting, Adjacent Fragment with Periodic Counting, Counting Quantifiers, Periodic Counting Quantifiers, Decidable Fragments of First-Order Logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.42
Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations

Authors: Tim S. Lyon

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for Gödel-Löb provability logic. In particular, we consider Sambin and Valentini’s sequent system GL_{seq}, Shamkanov’s non-wellfounded and cyclic sequent systems GL_∞ and GL_{circ}, Poggiolesi’s tree-hypersequent system CSGL, and Negri’s labeled sequent system G3GL. Shamkanov provided proof-theoretic correspondences between GL_{seq}, GL_∞, and GL_{circ}, and Goré and Ramanayake showed how to transform proofs between CSGL and G3GL, however, the exact nature of proof transformations between the former three systems and the latter two systems has remained an open problem. We solve this open problem by showing how to restructure tree-hypersequent proofs into an end-active form and introduce a novel linearization technique that transforms such proofs into linear nested sequent proofs. As a result, we obtain a new proof-theoretic tool for extracting linear nested sequent systems from tree-hypersequent systems, which yields the first cut-free linear nested sequent calculus LNGL for Gödel-Löb provability logic. We show how to transform proofs in LNGL into a certain normal form, where proofs repeat in stages of modal and local rule applications, and which are translatable into GL_{seq} and G3GL proofs. These new syntactic transformations, together with those mentioned above, establish full proof-theoretic correspondences between GL_{seq}, GL_∞, GL_{circ}, CSGL, G3GL, and LNGL while also giving (to the best of the author’s knowledge) the first constructive proof mappings between structural (viz. labeled, tree-hypersequent, and linear nested sequent) systems and a cyclic sequent system.
Cite as

Tim S. Lyon. Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 42:1-42:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lyon:LIPIcs.CSL.2025.42,
  author =	{Lyon, Tim S.},
  title =	{{Unifying Sequent Systems for G\"{o}del-L\"{o}b Provability Logic via Syntactic Transformations}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{42:1--42:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.42},
  URN =		{urn:nbn:de:0030-drops-227992},
  doi =		{10.4230/LIPIcs.CSL.2025.42},
  annote =	{Keywords: Cyclic proof, G\"{o}del-L\"{o}b logic, Labeled sequent, Linear nested sequent, Modal logic, Non-wellfounded proof, Proof theory, Proof transformation, Tree-hypersequent}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.41
Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents

Authors: Tim S. Lyon, Ian Shillito, and Alwen Tiu

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
It is well-known that extending the Hilbert axiomatic system for first-order intuitionistic logic with an exclusion operator, that is dual to implication, collapses the domains of models into a constant domain. This makes it an interesting problem to find a sound and complete proof system for first-order bi-intuitionistic logic with non-constant domains that is also conservative over first-order intuitionistic logic. We solve this problem by presenting the first sound and complete proof system for first-order bi-intuitionistic logic with increasing domains. We formalize our proof system as a polytree sequent calculus (a notational variant of nested sequents), and prove that it enjoys cut-elimination and is conservative over first-order intuitionistic logic. A key feature of our calculus is an explicit eigenvariable context, which allows us to control precisely the scope of free variables in a polytree structure. Semantically this context can be seen as encoding a notion of Scott’s existence predicate for intuitionistic logic. This turns out to be crucial to avoid the collapse of domains and to prove the completeness of our proof system. The explicit consideration of the variable context in a formula sheds light on a previously overlooked dependency between the residuation principle and the existence predicate in the first-order setting, which may help to explain the difficulty in designing a sound and complete proof system for first-order bi-intuitionistic logic.
Cite as

Tim S. Lyon, Ian Shillito, and Alwen Tiu. Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 41:1-41:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lyon_et_al:LIPIcs.CSL.2025.41,
  author =	{Lyon, Tim S. and Shillito, Ian and Tiu, Alwen},
  title =	{{Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{41:1--41:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.41},
  URN =		{urn:nbn:de:0030-drops-227987},
  doi =		{10.4230/LIPIcs.CSL.2025.41},
  annote =	{Keywords: Bi-intuitionistic, Cut-elimination, Conservativity, Domain, First-order, Polytree, Proof theory, Reachability, Sequent}
}
Document
Vision
DOI: 10.4230/TGDK.1.1.13
Autonomy in the Age of Knowledge Graphs: Vision and Challenges

Authors: Jean-Paul Calbimonte, Andrei Ciortea, Timotheus Kampik, Simon Mayer, Terry R. Payne, Valentina Tamma, and Antoine Zimmermann

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
In this position paper, we propose that Knowledge Graphs (KGs) are one of the prime approaches to support the programming of autonomous software systems at the knowledge level. From this viewpoint, we survey how KGs can support different dimensions of autonomy in such systems: For example, the autonomy of systems with respect to their environment, or with respect to organisations; and we discuss related practical and research challenges. We emphasise that KGs need to be able to support systems of autonomous software agents that are themselves highly heterogeneous, which limits how these systems may use KGs. Furthermore, these heterogeneous software agents may populate highly dynamic environments, which implies that they require adaptive KGs. The scale of the envisioned systems - possibly stretching to the size of the Internet - highlights the maintainability of the underlying KGs that need to contain large-scale knowledge, which requires that KGs are maintained jointly by humans and machines. Furthermore, autonomous agents require procedural knowledge, and KGs should hence be explored more towards the provisioning of such knowledge to augment autonomous behaviour. Finally, we highlight the importance of modelling choices, including with respect to the selected abstraction level when modelling and with respect to the provisioning of more expressive constraint languages.
Cite as

Jean-Paul Calbimonte, Andrei Ciortea, Timotheus Kampik, Simon Mayer, Terry R. Payne, Valentina Tamma, and Antoine Zimmermann. Autonomy in the Age of Knowledge Graphs: Vision and Challenges. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{calbimonte_et_al:TGDK.1.1.13,
  author =	{Calbimonte, Jean-Paul and Ciortea, Andrei and Kampik, Timotheus and Mayer, Simon and Payne, Terry R. and Tamma, Valentina and Zimmermann, Antoine},
  title =	{{Autonomy in the Age of Knowledge Graphs: Vision and Challenges}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{13:1--13:22},
  ISSN =	{2942-7517},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.13},
  URN =		{urn:nbn:de:0030-drops-194872},
  doi =		{10.4230/TGDK.1.1.13},
  annote =	{Keywords: Knowledge graphs, Autonomous Systems}
}
Document
Position
DOI: 10.4230/TGDK.1.1.2
Large Language Models and Knowledge Graphs: Opportunities and Challenges

Authors: Jeff Z. Pan, Simon Razniewski, Jan-Christoph Kalo, Sneha Singhania, Jiaoyan Chen, Stefan Dietze, Hajira Jabeen, Janna Omeliyanenko, Wen Zhang, Matteo Lissandrini, Russa Biswas, Gerard de Melo, Angela Bonifati, Edlira Vakaj, Mauro Dragoni, and Damien Graux

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
Large Language Models (LLMs) have taken Knowledge Representation - and the world - by storm. This inflection point marks a shift from explicit knowledge representation to a renewed focus on the hybrid representation of both explicit knowledge and parametric knowledge. In this position paper, we will discuss some of the common debate points within the community on LLMs (parametric knowledge) and Knowledge Graphs (explicit knowledge) and speculate on opportunities and visions that the renewed focus brings, as well as related research topics and challenges.
Cite as

Jeff Z. Pan, Simon Razniewski, Jan-Christoph Kalo, Sneha Singhania, Jiaoyan Chen, Stefan Dietze, Hajira Jabeen, Janna Omeliyanenko, Wen Zhang, Matteo Lissandrini, Russa Biswas, Gerard de Melo, Angela Bonifati, Edlira Vakaj, Mauro Dragoni, and Damien Graux. Large Language Models and Knowledge Graphs: Opportunities and Challenges. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 2:1-2:38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{pan_et_al:TGDK.1.1.2,
  author =	{Pan, Jeff Z. and Razniewski, Simon and Kalo, Jan-Christoph and Singhania, Sneha and Chen, Jiaoyan and Dietze, Stefan and Jabeen, Hajira and Omeliyanenko, Janna and Zhang, Wen and Lissandrini, Matteo and Biswas, Russa and de Melo, Gerard and Bonifati, Angela and Vakaj, Edlira and Dragoni, Mauro and Graux, Damien},
  title =	{{Large Language Models and Knowledge Graphs: Opportunities and Challenges}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{2:1--2:38},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.2},
  URN =		{urn:nbn:de:0030-drops-194766},
  doi =		{10.4230/TGDK.1.1.2},
  annote =	{Keywords: Large Language Models, Pre-trained Language Models, Knowledge Graphs, Ontology, Retrieval Augmented Language Models}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.9
A Concurrent Language for Argumentation: Preliminary Notes

Authors: Stefano Bistarelli and Carlo Taticchi

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
While agent-based modelling languages naturally implement concurrency, the currently available languages for argumentation do not allow to explicitly model this type of interaction. In this paper we introduce a concurrent language for handling process arguing and communicating using a shared argumentation framework (reminding shared constraint store as in concurrent constraint). We introduce also basic expansions, contraction and revision procedures as main bricks for enforcement, debate, negotiation and persuasion.
Cite as

Stefano Bistarelli and Carlo Taticchi. A Concurrent Language for Argumentation: Preliminary Notes. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bistarelli_et_al:OASIcs.Gabbrielli.9,
  author =	{Bistarelli, Stefano and Taticchi, Carlo},
  title =	{{A Concurrent Language for Argumentation: Preliminary Notes}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{9:1--9:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.9},
  URN =		{urn:nbn:de:0030-drops-132311},
  doi =		{10.4230/OASIcs.Gabbrielli.9},
  annote =	{Keywords: Argumentation, Concurrent Language, Debating, Negotiation, Belief Revision}
}
Document
DOI: 10.4230/DagSemProc.09351.8
Speech acts as announcements

Authors: Nadine Guiraud, Andreas Herzig, and Emiliano Lorini

Published in: Dagstuhl Seminar Proceedings, Volume 9351, Information processing, rational belief change and social interaction (2009)

Abstract
Our aim is to use the logic of public announcements and more generally dynamic epistemic logics as a logic of speech acts. To that end we start from a simple multimodal logic of beliefs and goals (without common belief), and add public announcements. We suppose that announcements do not modify goals. We then consider several variants of speech acts of assertive and directive force and provide a modelling in terms of speech acts.
Cite as

Nadine Guiraud, Andreas Herzig, and Emiliano Lorini. Speech acts as announcements. In Information processing, rational belief change and social interaction. Dagstuhl Seminar Proceedings, Volume 9351, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{guiraud_et_al:DagSemProc.09351.8,
  author =	{Guiraud, Nadine and Herzig, Andreas and Lorini, Emiliano},
  title =	{{Speech acts as announcements}},
  booktitle =	{Information processing, rational belief change and social interaction},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9351},
  editor =	{Giacomo Bonanno and James Delgrande and Hans Rott},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09351.8},
  URN =		{urn:nbn:de:0030-drops-22935},
  doi =		{10.4230/DagSemProc.09351.8},
  annote =	{Keywords: Logic of belief, logic of goals, speech act theory, dynamic epistemic logic, public announcements}
}
Document
DOI: 10.4230/DagSemProc.09351.5
Epistemic Games in Modal Logic: Joint Actions, Knowledge and Preferences all together

Authors: Emiliano Lorini, François Schwarzentruber, and Andreas Herzig

Published in: Dagstuhl Seminar Proceedings, Volume 9351, Information processing, rational belief change and social interaction (2009)

Abstract
We present in this work a sound and complete modal logic called EDLA (Epistemic Dynamic Logic of Agency) integrating the concepts of joint action, preference and knowledge and enabling to reason about epistemic games in strategic form. We provide complexity results for EDLA. In the second part of the paper, we study in EDLA the epistemic and rationality conditions of some classical solution concepts like Nash equilibrium and Iterated Deletion of Strictly Dominated Strategies (IDSDS). In the last part of the paper we combine EDLA with Dynamic Epistemic Logic (DEL) in order to model epistemic game dynamics.
Cite as

Emiliano Lorini, François Schwarzentruber, and Andreas Herzig. Epistemic Games in Modal Logic: Joint Actions, Knowledge and Preferences all together. In Information processing, rational belief change and social interaction. Dagstuhl Seminar Proceedings, Volume 9351, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{lorini_et_al:DagSemProc.09351.5,
  author =	{Lorini, Emiliano and Schwarzentruber, Fran\c{c}ois and Herzig, Andreas},
  title =	{{Epistemic Games in Modal Logic: Joint Actions, Knowledge and Preferences all together}},
  booktitle =	{Information processing, rational belief change and social interaction},
  pages =	{1--20},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9351},
  editor =	{Giacomo Bonanno and James Delgrande and Hans Rott},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09351.5},
  URN =		{urn:nbn:de:0030-drops-22313},
  doi =		{10.4230/DagSemProc.09351.5},
  annote =	{Keywords: Modal logic, game theory, epistemic games}
}
Document
DOI: 10.4230/DagSemProc.09121.14
Dynamic Context Logic and its Application to Norm

Authors: Guillaume Aucher, Davide Grossi, Andreas Herzig, and Emiliano Lorini

Published in: Dagstuhl Seminar Proceedings, Volume 9121, Normative Multi-Agent Systems (2009)

Abstract
Building on a simple modal logic of context, the paper presents a dynamic logic characterizing operations of contraction and expansion on theories. We investigate the mathematical properties of the logic, and use it to develop an axiomatic and semantic analysis of norm change in normative systems. The proposed analysis advances the state of the art by providing a formal semantics of norm-change which, at the same time, takes into account several different aspects of the phenomenon, such as permission and obligation dynamics, as well as the dynamics of classificatory rules.
Cite as

Guillaume Aucher, Davide Grossi, Andreas Herzig, and Emiliano Lorini. Dynamic Context Logic and its Application to Norm. In Normative Multi-Agent Systems. Dagstuhl Seminar Proceedings, Volume 9121, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{aucher_et_al:DagSemProc.09121.14,
  author =	{Aucher, Guillaume and Grossi, Davide and Herzig, Andreas and Lorini, Emiliano},
  title =	{{Dynamic Context Logic and its Application to Norm}},
  booktitle =	{Normative Multi-Agent Systems},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9121},
  editor =	{Guido Boella and Pablo Noriega and Gabriella Pigozzi and Harko Verhagen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09121.14},
  URN =		{urn:nbn:de:0030-drops-19009},
  doi =		{10.4230/DagSemProc.09121.14},
  annote =	{Keywords: Context logic, norm change, deontic logic}
}
Document
DOI: 10.4230/DagSemProc.07351.15
Optimal Regression for Reasoning about Knowledge and Actions

Authors: Hans van Ditmarsch, Andreas Herzig, and Tiago de Lima

Published in: Dagstuhl Seminar Proceedings, Volume 7351, Formal Models of Belief Change in Rational Agents (2007)

Abstract
We show how in the propositional case both Reiter's and Scherl & Levesque's solutions to the frame problem can be modelled in dynamic epistemic logic (DEL), and provide an optimal regression algorithm for the latter. Our method is as follows: we extend Reiter's framework by integrating observation actions and modal operators of knowledge, and encode the resulting formalism in DEL with announcement and assignment operators. By extending Lutz' recent satisfiability-preserving reduction to our logic, we establish optimal decision procedures for both Reiter's and Scherl & Levesque's approaches: satisfiability is NP-complete for one agent, PSPACE-complete for multiple agents and EXPTIME-complete when common knowledge is involved.
Cite as

Hans van Ditmarsch, Andreas Herzig, and Tiago de Lima. Optimal Regression for Reasoning about Knowledge and Actions. In Formal Models of Belief Change in Rational Agents. Dagstuhl Seminar Proceedings, Volume 7351, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{vanditmarsch_et_al:DagSemProc.07351.15,
  author =	{van Ditmarsch, Hans and Herzig, Andreas and de Lima, Tiago},
  title =	{{Optimal Regression for Reasoning about Knowledge and Actions}},
  booktitle =	{Formal Models of Belief Change in Rational Agents},
  pages =	{1--22},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7351},
  editor =	{Giacomo Bonanno and James Delgrande and J\'{e}r\^{o}me Lang and Hans Rott},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07351.15},
  URN =		{urn:nbn:de:0030-drops-12077},
  doi =		{10.4230/DagSemProc.07351.15},
  annote =	{Keywords: Reasoning about action and change, reasoning about knowledge, situation calculus, frame problem, dynamic epistemic logic}
}
Document
DOI: 10.4230/DagSemProc.05321.12
On updates with integrity constraints

Authors: Andreas Herzig

Published in: Dagstuhl Seminar Proceedings, Volume 5321, Belief Change in Rational Agents: Perspectives from Artificial Intelligence, Philosophy, and Economics (2005)

Abstract
In his paper ``Making Counterfactual Assumptions'' Frank Veltman has proposed a new semantics for counterfactual conditionals. It is based on a particular update operation, and we show that it provides a new and interesting way of updating logical databases under integrity constraints which generalizes in particular Winslett's PMA.
Cite as

Andreas Herzig. On updates with integrity constraints. In Belief Change in Rational Agents: Perspectives from Artificial Intelligence, Philosophy, and Economics. Dagstuhl Seminar Proceedings, Volume 5321, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{herzig:DagSemProc.05321.12,
  author =	{Herzig, Andreas},
  title =	{{On updates with integrity constraints}},
  booktitle =	{Belief Change in Rational Agents: Perspectives from Artificial Intelligence, Philosophy, and Economics},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5321},
  editor =	{James Delgrande and Jerome Lang and Hans Rott and Jean-Marc Tallon},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05321.12},
  URN =		{urn:nbn:de:0030-drops-3344},
  doi =		{10.4230/DagSemProc.05321.12},
  annote =	{Keywords: Updates, PMA, prime implicants}
}
  • Refine by Type
  • 14 Document/PDF
  • 8 Document/HTML

  • Refine by Publication Year
  • 6 2025
  • 2 2023
  • 1 2020
  • 3 2009
  • 1 2007
  • Show More...

  • Refine by Author
  • 5 Herzig, Andreas
  • 3 Lorini, Emiliano
  • 2 Lyon, Tim S.
  • 1 Aucher, Guillaume
  • 1 Bistarelli, Stefano
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs
  • 3 OASIcs
  • 2 TGDK
  • 5 DagSemProc

  • Refine by Classification
  • 3 Computing methodologies → Knowledge representation and reasoning
  • 2 Theory of computation → Constructive mathematics
  • 2 Theory of computation → Modal and temporal logics
  • 2 Theory of computation → Proof theory
  • 1 Computer systems organization → Self-organizing autonomic computing
  • Show More...

  • Refine by Keyword
  • 2 Modal logic
  • 2 Proof theory
  • 2 dynamic epistemic logic
  • 1 Adjacent Fragment
  • 1 Adjacent Fragment with Counting
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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