| 1. |
- Enqvist, Sebastian, et al.
(author)
-
A Structuralist Framework for the Logic of Theory Change
- 2011
-
In: Belief revision meets philosophy of science. - 9789048196081
-
Book chapter (other academic/artistic)abstract
- Belief revision theory and philosophy of science both aspire to shed light on the dynamics of knowledge – on how our view of the world changes (typically) in the light of new evidence. Yet these two areas of research have long seemed strangely detached from each other, as witnessed by the small number of cross-references and researchers working in both domains. One may speculate as to what has brought about this surprising, and perhaps unfortunate, state of affairs. One factor may be that while belief revision theory has traditionally been pursued in a bottom- up manner, focusing on the endeavors of single inquirers, philosophers of science, inspired by logical empiricism, have tended to be more interested in science as a multi-agent or agent-independent phenomenon.
|
|
| 2. |
- Kehoe, Laura, et al.
(author)
-
Make EU trade with Brazil sustainable
- 2019
-
In: Science. - : American Association for the Advancement of Science (AAAS). - 0036-8075 .- 1095-9203. ; 364:6438, s. 341-
-
Journal article (other academic/artistic)
|
|
| 3. |
- Afshari, Bahareh, 1981, et al.
(author)
-
Cyclic proofs for the first-order mu-calculus
- 2024
-
In: Logic Journal of the IGPL. - : Oxford University Press (OUP). - 1367-0751 .- 1368-9894. ; 32:1, s. 1-34
-
Journal article (peer-reviewed)abstract
- We introduce a path-based cyclic proof system for first-order mu-calculus, the extension of first-order logic by second-order quantifiers for least and greatest fixed points of definable monotone functions. We prove soundness of the system and demonstrate it to be as expressive as the known trace-based cyclic systems of Dam and Sprenger. Furthermore, we establish cut-free completeness of our system for the fragment corresponding to the modal mu-calculus.
|
|
| 4. |
- Afshari, Bahareh, 1981, et al.
(author)
-
PROOF SYSTEMS FOR TWO-WAY MODAL MU-CALCULUS
- 2023
-
In: Journal of Symbolic Logic (JSL). - 0022-4812 .- 1943-5886.
-
Journal article (peer-reviewed)abstract
- We present sound and complete sequent calculi for the modal mu-calculus with converse modalities, aka two-way modal mu-calculus. Notably, we introduce a cyclic proof system wherein proofs can be represented as finite trees with back-edges, i.e., finite graphs. The sequent calculi incorporate ordinal annotations and structural rules for managing them. Soundness is proved with relative ease as is the case for the modal mu-calculus with explicit ordinals. The main ingredients in the proof of completeness are isolating a class of non-wellfounded proofs with sequents of bounded size, called slim proofs, and a counter-model construction that shows slimness suffices to capture all validities. Slim proofs are further transformed into cyclic proofs by means of re-assigning ordinal annotations.
|
|
| 5. |
|
|
| 6. |
- Carlsnaes, Walter, 1943-, et al.
(author)
-
Editors' Introduction
- 2011. - 1
-
In: Foreign Policy Analysis. - London : Sage Publications. - 9781412921442 ; 3:1, s. 7-12
-
Book chapter (other academic/artistic)
|
|
| 7. |
- Enqvist, Sebastian, et al.
(author)
-
A coalgebraic view of characteristic formulas in equational modal fixed point logic
- 2014
-
In: Coalgebraic Methods in Computer Science : 12th IFIP WG 1.3 International Workshop, CMCS 2014, Colocated with ETAPS 2014, Grenoble, France, April 5-6, 2014, Revised Selected Papers / Lecture notes in computer science (LNCS). - 1611-3349 .- 0302-9743. ; LNCS 8446
-
Conference paper (peer-reviewed)
|
|
| 8. |
|
|
| 9. |
- Enqvist, Sebastian
(author)
-
A new coalgebraic Lindström theorem
- 2016
-
In: Journal of Logic and Computation. - : Oxford University Press (OUP). - 0955-792X .- 1465-363X. ; 26:5, s. 1541-1566
-
Journal article (peer-reviewed)abstract
- In a recent article, Alexander Kurz and Yde Venema establish a Lindström theorem for coalgebraic modal logic that is shown to imply a modal Lindström theorem by Maarten de Rijke. A later modal Lindström theorem has been established by Johan van Benthem, and this result still lacks a coalgebraic formulation. The main obstacle has so far been the lack of a suitable notion of ‘submodels’ in coalgebraic semantics, and the problem is left open by Kurz and Venema. In this article, we propose a solution to this problem and derive a general coalgebraic Lindström theorem along the lines of van Benthem's result. We provide several applications of the result.
|
|
| 10. |
- Enqvist, Sebastian, et al.
(author)
-
An expressive completeness theorem for coalgebraic modal mu-calculi
- 2017
-
In: Logical Methods in Computer Science. - 1860-5974. ; 13:2
-
Journal article (peer-reviewed)abstract
- Generalizing standard monadic second-order logic for Kripke models, we introduce monadic second-order logic interpreted over coalgebras for an arbitrary set functor. We then consider invariance under behavioral equivalence of MSO-formulas. More specifically, we investigate whether the coalgebraic mu-calculus is the bisimulation-invariant fragment of the monadic second-order language for a given functor. Using automata theoretic techniques and building on recent results by the third author, we show that in order to provide such a characterization result it suffices to find what we call an adequate uniform construction for the coalgebraic type functor. As direct applications of this result we obtain a partly new proof of the Janin-Walukiewicz Theorem for the modal mu-calculus, avoiding the use of syntactic normal forms, and bisimulation invariance results for the bag functor (graded modal logic) and all exponential polynomial functors (including the game functor). As a more involved application, involving additional non-trivial ideas, we also derive a characterization theorem for the monotone modal mu-calculus, with respect to a natural monadic second-order language for monotone neighborhood models.
|
|
| 11. |
- Enqvist, Sebastian, et al.
(author)
-
Bisimulations for coalgebras on Stone spaces
- 2018
-
In: Journal of logic and computation (Print). - : Oxford University Press (OUP). - 0955-792X .- 1465-363X. ; 28:6, s. 991-1010
-
Journal article (peer-reviewed)abstract
- We introduce and study bisimulations for coalgebras on Stone spaces (Kupke et al., 2004, Theoretical Computer Science, 327, 109-134), motivated by previous work on ultrafilter extensions for coalgebras (Kupke et al., 2005, Algebra and Coalgebra in Computer Science, 263-277), bisimulations for the Vietoris functor (Bezhanishvili et al., 2010, Journal of Logic and Computation, 20, 1017-1040) and building on an idea of Gorin and Schroder (2013, Algebra and Coalgebra in Computer Science, 8089, 253-266). We provide a condition under which our notion of bisimulation gives a sound and complete proof method for behavioural equivalence, and show that it generalizes Vietoris bisimulations. Our main technical result proves that the topological closure of any bisimulation between Stone coalgebras in our sense is still a bisimulation. This answers a question raised in Bezhanishvili et al. (2010, Journal of Logic and Computation, 20, 1017-1040), and also leads to a simpler proof of the main theorem in that paper, that the topological closure of a Kripke bisimulation is a Vietoris bisimulation. As a second application of our general bisimulation concept, we study neighbourhood bisimulations on descriptive frames for monotone modal logic as they were introduced in Hansen et al. (2009, Logical Methods in Computer Science, 5, 1-38). From our general results we derive that these are sound and complete for behavioural equivalence and that the topological closure of a neighbourhood bisimulation is still a neighbourhood bisimulation, in analogy with the main result in Bezhanishvili et al. (2010, Journal of Logic and Computation, 20, 1017-1040). Finally, we apply our result to bisimulations for Stone companions of set functors as defined in Kupke et al.
|
|
| 12. |
- Enqvist, Sebastian, et al.
(author)
-
Completeness for coalgebraic fixpoint logic
- 2016
-
In: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). - 1868-8969. - 9783959770224 ; 62, s. 1-7
-
Conference paper (peer-reviewed)abstract
- We introduce an axiomatization for the coalgebraic fixed point logic which was introduced by Venema as a generalization, based on Moss' coalgebraic modality, of the well-known modal mucalculus. Our axiomatization can be seen as a generalization of Kozen's proof system for the modal mu-calculus to the coalgebraic level of generality. It consists of a complete axiomatization for Moss' modality, extended with Kozen's axiom and rule for the fixpoint operators. Our main result is a completeness theorem stating that, for functors that preserve weak pullbacks and restrict to finite sets, our axiomatization is sound and complete for the standard interpretation of the language in coalgebraic models. Our proof is based on automata-theoretic ideas: in particular, we introduce the notion of consequence game for modal automata, which plays a crucial role in the proof of our main result. The result generalizes the celebrated Kozen-Walukiewicz completeness theorem for the modal mu-calculus, and our automata-theoretic methods simplify parts of Walukiewicz' proof.
|
|
| 13. |
- Enqvist, Sebastian, et al.
(author)
-
Completeness for mu-calculi : A coalgebraic approach
- 2019
-
In: Annals of Pure and Applied Logic. - : Elsevier BV. - 0168-0072 .- 1873-2461. ; 170:5, s. 578-641
-
Journal article (peer-reviewed)abstract
- We set up a generic framework for proving completeness results for variants of the modal mu-calculus, using tools from coalgebraic modal logic. We illustrate the method by proving two new completeness results: for the graded mu-calculus (which is equivalent to monadic second-order logic on the class of unranked tree models), and for the monotone modal mu-calculus. Besides these main applications, our result covers the Kozen-Walukiewicz completeness theorem for the standard modal mu-calculus, as well as the linear-time mu-calculus and modal fixpoint logics on ranked trees. Completeness of the linear time mu-calculus is known, but the proof we obtain here is different and places the result under a common roof with Walukiewicz' result. Our approach combines insights from the theory of automata operating on potentially infinite objects, with methods from the categorical framework of coalgebra as a general theory of state-based evolving systems. At the interface of these theories lies the notion of a coalgebraic modal one-step language. One of our main contributions here is the introduction of the novel concept of a disjunctive basis for a modal one-step language. Generalizing earlier work, our main general result states that in case a coalgebraic modal logic admits such a disjunctive basis, then soundness and completeness at the one-step level transfer to the level of the full coalgebraic modal mu-calculus.
|
|
| 14. |
- Enqvist, Sebastian
(author)
-
Contraction in Interrogative Belief Revision
- 2010
-
In: Erkenntnis. - : Springer Science and Business Media LLC. - 1572-8420 .- 0165-0106. ; 72:3, s. 315-335
-
Journal article (peer-reviewed)abstract
- In the paper "On the role of the research agenda in epistemic change", Olsson and Westlund have suggested that the notion of epistemic state employed in the standard framework of belief revision (Alchourrn et al. 1985; Gardenfors 1988) should be extended to include a representation of the agent's research agenda (Olsson and Westlund 2006). The resulting framework will here be referred to as interrogative belief revision. In this paper, I attempt to deal with the problem of how research agendas should change in contraction, a problem largely left open by Olsson and Westlund. Two desiderata of an appropriate solution are suggested: one is a principle of continuity, stating that changes in the research agenda should somehow reflect that certain long term research interests are kept fixed. The other desideratum, which is based on part of Olsson and Westlund's motivation for adding research agendas to the epistemic states, is that we should be able to account for how contraction may serve to open up new, fruitful hypotheses for investigation. In order to achieve these desiderata, I base my solution on a revised version of Olsson and Westlund's notion of epistemic state.
|
|
| 15. |
- Enqvist, Sebastian, et al.
(author)
-
DISJUNCTIVE BASES : NORMAL FORMS AND MODEL THEORY FOR MODAL LOGICS
- 2019
-
In: Logical Methods in Computer Science. - 1860-5974. ; 15:1
-
Journal article (peer-reviewed)abstract
- We present the concept of a disjunctive basis as a generic framework for normal forms in modal logic based on coalgebra. Disjunctive bases were defined in previous work on completeness for modal fixpoint logics, where they played a central role in the proof of a generic completeness theorem for coalgebraic mu-calculi. Believing the concept has a much wider significance, here we investigate it more thoroughly in its own right. We show that the presence of a disjunctive basis at the one-step level entails a number of good properties for a coalgebraic mu-calculus, in particular, a simulation theorem showing that every alternating automaton can be transformed into an equivalent nondeterministic one. Based on this, we prove a Lyndon theorem for the full fixpoint logic, its fixpoint-free fragment and its one-step fragment, a Uniform Interpolation result, for both the full mu-calculus and its fixpoint-free fragment, and a Janin-Walukiewicz-style characterization theorem for the mu-calculus under slightly stronger assumptions. We also raise the questions, when a disjunctive basis exists, and how disjunctive bases arc related to Moss' coalgebraic nabla modalities. Nabla formulas provide disjunctive bases for many coalgebraic modal logics, but there are cases where disjunctive bases give useful normal forms even when nabla formulas fail to do so, our prime example being graded modal logic. We also show that disjunctive bases are preserved by forming sums, products and compositions of coalgebraic modal logics, providing tools for modular construction of modal logics admitting disjunctive bases. Finally, we consider the problem of giving a category-theoretic formulation of disjunctive bases, and provide a partial solution.
|
|
| 16. |
- Enqvist, Sebastian
(author)
-
Flat modal fixpoint logics with the converse modality
- 2018
-
In: Journal of logic and computation (Print). - : Oxford University Press (OUP). - 0955-792X .- 1465-363X. ; 28:6, s. 1065-1097
-
Journal article (peer-reviewed)abstract
- We prove a generic completeness result for a class of modal fixpoint logics corresponding to flat fragments of the two-way mu-calculus, with the restriction that the fixpoint connectives involved must be disjunctive formulas. This extends earlier work by Santocanale and Venema. We observe that Santocanale and Venema's proof that least fixpoints in the free algebras of flat fixpoint logics are constructive, using finitary adjoints, no longer works when the converse modality is introduced. Instead, our completeness proof directly constructs a model for a consistent formula, using the induction rule in a way that is similar to the standard completeness proof for propositional dynamic logic. This approach is combined with the concept of a focus, which has previously been used in tableau-based reasoning for modal fixpoint logics, and the use of networks, which is a well-known tool for proving completeness of modal logics.
|
|
| 17. |
|
|
| 18. |
- Enqvist, Sebastian
(author)
-
Interrogative Belief Revision
- 2011
-
Doctoral thesis (other academic/artistic)abstract
- This thesis deals with the theory of interrogative belief revision, a recent development in the subfield of philosophical logic known as belief revision theory. While classical belief revision theory deals with the dynamics of an agent’s beliefs, interrogative belief revision aims to describe the dynamics of the agent’s questions about the world, or research agenda, as well. Great emphasis is put on the interaction between belief change and changes in the research agenda. I develop both the technical framework for this theory by constructing and investigating modal logics for reasoning about the dynamics of research interests, as well as pursuing further the philosophical foundations and applications of the theory. Among the contributions of the thesis are: - a novel interpretation of the theory founded on a notion of epistemic strategies - a solution to the previously open problem of contraction and revision in this context - several systems of modal logic that can be used to reason about interrogative belief revision - completeness results and decidability results for these logics - a characterization of a class of relevant conditionals based on a notion of agenda relevance
|
|
| 19. |
|
|
| 20. |
- Enqvist, Sebastian
(author)
-
Interrogative Belief Revision in Modal Logic
- 2009
-
In: Journal of Philosophical Logic. - : Springer Science and Business Media LLC. - 0022-3611 .- 1573-0433. ; 38:5, s. 527-548
-
Journal article (peer-reviewed)abstract
- The well known AGM framework for belief revision has recently been extended to include a model of the research agenda of the agent, i.e. a set of questions to which the agent wishes to find answers (Olsson & Westlund in Erkenntnis, 65, 165-183, 2006). The resulting model has later come to be called interrogative belief revision. While belief revision has been studied extensively from the point of view of modal logic, so far interrogative belief revision has only been dealt with in the metalanguage approach in which AGM was originally presented. In this paper, I show how to model interrogative belief revision in a modal object language using a class of operators for questions. In particular, the solution I propose will be shown to capture the notion of K-truncation, a method for agenda update in the case of expansion constructed by Olsson & Westlund. Two case studies are conducted: first, an interrogative extension of Krister Segerberg's system DDL, and then a similar extension of Giacomo Bonanno's modal logic for belief revision. Sound and complete axioms will be provided for both of the resulting logics.
|
|
| 21. |
- Enqvist, Sebastian
(author)
-
Modelling Epistemic Actions in Interrogative Belief Revision
- 2012
-
In: Journal of Logic and Computation. - : Oxford University Press (OUP). - 0955-792X .- 1465-363X. ; 22:6, s. 1335-1365
-
Journal article (peer-reviewed)abstract
- Abstract in UndeterminedInterrogative belief revision is a relatively recent framework for belief revision theory, in which the epistemic state of an agent includes a representation of that agent's research agenda, i.e. the set of questions the agent wants to have answers to. This added structure opens new possibilites for various types of epistemic change that cannot be distinguished in traditional belief revision. In this article I use the so-called 'action model' approach known from the literature on dynamic epistemic logic to provide a unified framework in which we can reason about these various types of epistemic changes. I show how to model some natural examples of epistemic changes involving change of the research agenda in this framework. The action models give rise to a dynamic logic which is proven to be decidable.
|
|
| 22. |
|
|
| 23. |
|
|
| 24. |
- Enqvist, Sebastian, et al.
(author)
-
The Temporal Logic of Coalitional Goal Assignments in Concurrent Multiplayer Games
- 2022
-
In: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 23:4
-
Journal article (peer-reviewed)abstract
- We introduce and study a natural extension of the Alternating time temporal logic ATL, called Temporal Logic of Coalitional Goal Assignments (TLCGA). It features one new and quite expressive coalitional strategic operator, called the coalitional goal assignment operator ⦉ γ ⦊, where γ is a mapping assigning to each set of players in the game its coalitional goal, formalised by a path formula of the language of TLCGA, i.e., a formula prefixed with a temporal operator X, U, or G, representing a temporalised objective for the respective coalition, describing the property of the plays on which that objective is satisfied. Then, the formula ⦉ γ ⦊ intuitively says that there is a strategy profile Σ for the grand coalition Agt such that for each coalition C, the restriction Σ |C of Σ to C is a collective strategy of C that enforces the satisfaction of its objective γ (C) in all outcome plays enabled by Σ |C.We establish fixpoint characterizations of the temporal goal assignments in a μ-calculus extension of TLCGA, discuss its expressiveness and illustrate it with some examples, prove bisimulation invariance and Hennessy–Milner property for it with respect to a suitably defined notion of bisimulation, construct a sound and complete axiomatic system for TLCGA, and obtain its decidability via finite model property.
|
|
| 25. |
- Genot, Emmanuel, et al.
(author)
-
The Best of All PossibleWorlds: Where Interrogative Games Meet Research Agendas
- 2011
-
In: Belief Revision Meets Philosophy of Science. - Dordrecht : Springer Netherlands. - 9789048196081 - 9789048196098 ; 21, s. 225-252
-
Book chapter (peer-reviewed)abstract
- Erik J. Olsson and David Westlund have recently argued that the standard belief revision representation of an epistemic state is defective. In order to adequately model an epistemic state one needs, in addition to a belief set (or corpus, or theory, i.e. a set closed under deduction) K and (say) an entrenchment relation E, a research agenda A, i.e. a set of questions satisfying certain corpus-relative preconditions (hence called K-questions) the agent would like to have answers to. Informally, the preconditions guarantee that the set of potential answers represent a partition of possible expansions of K, hence are equivalent to well-behaved sets of alternative hypotheses.
|
|
