M&M2013- Abstracts for Modality and Modalities, 2013
Mikkel Birkegaard Andersen
"Multi-agent plausibility planning"
This talk reports in on ongoing work in epistemic planning, specifically work on a multi-agent version of plausibility planning. Previous work has produced single-agent plausibility planning, where plausibility models capture a priori beliefs about the outcomes of actions, and multi-agent epistemic planning (without plausibilities). With plausibilities, an agent can reason about expected outcomes of actions before carrying them out, and thus plan only for those outcomes it deems plausible (saving computational time and possibly sanity). For plausibility planning a language for plan verification and an algorithm for plan synthesis has previously been developed.
These two previous frameworks are being generalised to multi-agent plausibility planning, allowing agents to plan for the expected (outcomes of) actions of others, and work to help or hinder them in their endeavours. Crucial here is the ability to embrace the perspective of others in order to understand how they see the world and possibly predict their actions. An algorithm for plan synthesis that does exactly that will be presented.
These two previous frameworks are being generalised to multi-agent plausibility planning, allowing agents to plan for the expected (outcomes of) actions of others, and work to help or hinder them in their endeavours. Crucial here is the ability to embrace the perspective of others in order to understand how they see the world and possibly predict their actions. An algorithm for plan synthesis that does exactly that will be presented.
Martin Mose Bentzen
"Action Type Deontic Logic for Ethical Robots"
In this talk, a deontic logic for artificial agents is presented. First, the logic is motivated by informal examples. The examples take potential obstacles to Human-Robot Interaction as their starting point. Secondly, the logic, Action Type Deontic Logic, is introduced in an abstract form. Thirdly, it is suggested how this logic can be applied to models of strategic situations familiar from game theory and STIT theory.
Patrick Blackburn
"Seligman-style Tableau for Hybrid Logic (Part 1)"
Tableau systems, natural deduction, and resolution systems for hybrid logic are usually ''labelled deduction systems'', often with the nominals and operators of the object language being used asthe labelling apparatus. This approach is now standard, but there is an interesting (though somewhat overlooked) alternative. In some classic papers dating back to the mid-1990s (see references below) Jerry Seligman proposed natural deduction and sequent calculi for hybrid logic that avoided labeling. In the last few weeks Torben Braüner, Thomas Bolander, Klaus Frovin Jørgensen and myself have (for a variety of reasons) been led to ask: what would (or should) a Seligman-style tableau system for hybrid logic look like? Somewhat to our surprise, what began as an exercise to fill in a gap in the landscape of hybrid proof systems has become a full blown research project, since in many respects we now find Seligman's approach superior to labeled tableau.
In this talk I shall motivate the Seligman-style approach, and discuss the first type of tableaux system we developed for it. As will become clear in the course of my talk, the sytem(s) discussed here are not fully satisfactory - but they do make very clear the intuitions driving Seligman-style tableaux reasoning, and they also motivate the rather more abstract style of tableau that we now favour (Thomas Bolander will discuss these in his talk).
Background Reading:
1) Hybrid Logic and its Proof-Theory, by Torben Braüner, Applied Logic Series, vol. 37. Springer, 2011.
2) Hybrid-logical Reasoning in False-Belief Tasks, by Torben Braüner, In Schipper, B. (ed.) Proceedings of Fourteenth Conference on Theoretical Aspects of Rationality and Knowledge (TARK), pages 186-195, 2013, Available at http://tark.org
3) The Logic of Correct Description, by Jerry Seligman, In de Rijke, M. (ed.) Advances in Intensional Logic, Applied Logic Series, vol. 7, pages 107-135. Kluwer,1997.
4) Internalisation: The Case of Hybrid Logics, by Jerry Seligman, Journal of Logic and Computation, volume 11, pages 671-689, 2001.
In this talk I shall motivate the Seligman-style approach, and discuss the first type of tableaux system we developed for it. As will become clear in the course of my talk, the sytem(s) discussed here are not fully satisfactory - but they do make very clear the intuitions driving Seligman-style tableaux reasoning, and they also motivate the rather more abstract style of tableau that we now favour (Thomas Bolander will discuss these in his talk).
Background Reading:
1) Hybrid Logic and its Proof-Theory, by Torben Braüner, Applied Logic Series, vol. 37. Springer, 2011.
2) Hybrid-logical Reasoning in False-Belief Tasks, by Torben Braüner, In Schipper, B. (ed.) Proceedings of Fourteenth Conference on Theoretical Aspects of Rationality and Knowledge (TARK), pages 186-195, 2013, Available at http://tark.org
3) The Logic of Correct Description, by Jerry Seligman, In de Rijke, M. (ed.) Advances in Intensional Logic, Applied Logic Series, vol. 7, pages 107-135. Kluwer,1997.
4) Internalisation: The Case of Hybrid Logics, by Jerry Seligman, Journal of Logic and Computation, volume 11, pages 671-689, 2001.
- Thomas Bolander
"Seligman-style Tableau for Hybrid Logic (Part 2)"
"Seligman-style Tableau for Hybrid Logic (Part 2)"
I will continue the story on Seligman-style tableau calculi that Patrick initiated in the previous talk. I will present our (current) favourite variant of the calculus, give example derivations and compare these to derivations in existing tableau calculi for hybrid logic. I will sketch our completeness proof and address the termination problem.
- Torben Braüner
- "Hybrid-Logical Proofs: With an Application to False-Belief Tasks"
Hybrid logic is an extension of ordinary modal logic which allows explicit reference to individual points in a Kripke model. This additional expressive power is useful for many applications. For example when reasoning about time one often wants to formulate a series of statements about what happens at specific times.
There is little consensus about proof-theory for ordinary modal logic. Many modal-logical proof systems lack important properties and the relationships between proof systems for different modal logics are often unclear. I start my talk by briefly describing how these deficiencies are remedied by hybrid-logical proof-theory.
I then show how a proof system for hybrid logic can be used to formalize false-belief tasks, which are used in cognitive psychology to test theory of mind. Giving a correct answer to such a false-belief task requires a shift from one's own perspective to another perspective (time, place, or person). This perspective shift can be handled directly in hybrid logic by letting points in a model represent perspectives.
There is little consensus about proof-theory for ordinary modal logic. Many modal-logical proof systems lack important properties and the relationships between proof systems for different modal logics are often unclear. I start my talk by briefly describing how these deficiencies are remedied by hybrid-logical proof-theory.
I then show how a proof system for hybrid logic can be used to formalize false-belief tasks, which are used in cognitive psychology to test theory of mind. Giving a correct answer to such a false-belief task requires a shift from one's own perspective to another perspective (time, place, or person). This perspective shift can be handled directly in hybrid logic by letting points in a model represent perspectives.
- Nina Gierasimczuk
- "Convergence to knowledge. A logical perspective."
I will give several examples on how the interdisciplinary toolbox of logic, computability, and formal learning theory can be used for dealing with the
problem of learning viewed from the perspective of modal logics of knowledge and belief change. In particular, I will focus on characterizations of successful learning processes, on computational aspects of convergence to certainty, topological aspects of convergence to safe belief, and, last but not least, on the reliability of various update and revision procedures.
problem of learning viewed from the perspective of modal logics of knowledge and belief change. In particular, I will focus on characterizations of successful learning processes, on computational aspects of convergence to certainty, topological aspects of convergence to safe belief, and, last but not least, on the reliability of various update and revision procedures.
- Jens Ulrik Hansen
- "Modal logics for comparative evidence and informational cascades"
In modeling reasoning and information dynamics in real-life social phenomena such as informational cascades, new aspects are required of logics for multi-agent systems and rational interaction. What some of these new aspects amount to, will be explained using the herding phenomena known as informational cascades as an example. More specific, I explain how general modal logics can be developed to deal with various forms of comparative evidence and information dynamics. As a special interesting case is a logic for counting evidence that might replace Bayesian reasoning in several cases of informational cascades.
- Vincent Hendricks
- "Structures of Social Proof"
Abstract After having been victim of extensive cyber-bullying on miscellanous social media for a number of years, a young woman committed suicide in late 2012. The horrific campaign against the woman---virtual and real---leading up to her death exhibit both the possible cost-neutral posts of evil on social media and the unfortunate reliance on social proof among users resulting in pluralistic ignorance, bystander-effects aided by informational cascades. The structure and modularity of social proof is unravelled including formal characterizations of the socio-epistemic phenomena in good part responsible for victimizing Amanda Todd as information goes out of control.
- Martin Holm Jensen
"Connecting Epistemic Planning and Knowledge-Based Programs"
"Connecting Epistemic Planning and Knowledge-Based Programs"
In planning the aim is to describe a course of action (a plan) so that an agent achieves her goal. This very general mental capability can be formulated in many ways, in this presentation we will consider knowledge-based programs (KBPs) and single-agent epistemic planning (EP). While both frameworks are based on epistemic logic, there are immediate differences in the way actions are described. Here we show connections between the action theories of KBPs and the event models of EP. These connections allow polynomial reductions (in both directions) of the respective plan existence problems. We readily obtain complexity results of EP plan existence, subject to restrictions on the underlying logic. Finally we discuss how these restrictions may be utilized for finding decidable fragments of multi-agent epistemic planning.
- Klaus Frovin Jørgensen
"Proof Systems in Indexical Hybrid Logic"
- Klaus Frovin Jørgensen
"Proof Systems in Indexical Hybrid Logic"
In this talk we report from the ongoing work within indexical hybrid logic. One of the goals of this work - which is joint work with Patrick Blackburn - aims at providing complete axiomatisations of (a hybrid logical version of) Kaplan's logic of demonstratives. Last year we gave a complete tableau system for hybrid tense logic with the indexicals 'now', 'yesterday', 'today' and 'tomorrow'. Meanwhile this system has been improved as we have also provided complete systems in Hilbert style and natural deduction. One of the general advantages of our formalisations is the so called local character of the structure that is being imposed on the four indexicals. In this talk elaborate on the different proof systems as well show how the general axiomatisation simplify over different frames such as the linear ones.
Sara Negri
"Generation of proofs and countermodels in labelled sequent calculi"
Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin's method of maximal consistent sets of formulas. The powerful formalism of labelled sequent calculi, on the other hand, makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame class is found. Proof search in a basic system also gives a heuristic for finding frame correspondents of modal axioms, and thus, ultimately, for finding complete sequent calculi for axiomatically presented logics. A number of examples will illustrate the method, its subtleties, challenges, and present scope.
Nikolaj Nottelmann
"Modal epistemology: A very brief tutorial"
The purpose of this talk is to give the uninitiated at least a brief glimpse of the current main themes within modal epistemology. Overall, this field is concerned with the following questions: 1. Which modal claims form a cognitive domain? (e.g. de dicto modal statements, de re modal statements). 2. Which methods, if any, may reliably lead to true beliefs within the relevant cognitive domains, if any? 3. How could we gain justified belief and knowledge within said domains? 4. Is it possible to acquire certainty and/or indefeasible justified belief within those domains?
Questions (1) and (2) naturally lead to questions about the metaphysics of modality, not least to questions concerning the reality and nature of essences, possible worlds etc. Question (2) also involves a diagnosis of the epistemic power - within the relevant domains - of processes such as empirical observation, imagining, conceiving, “rational insight” etc. Important questions involve the natures of such methods, and whether they may - even in the best case - merely provide evidence in favour of modal beliefs, or if, e.g., there are modal ties between (some version of) possibility and (ideal) conceivability. Question (3) asks us to probe our general conceptions of epistemic justification and knowledge in the light of the results achieved above. Finally, question (4) asks us to consider whether some sources of modal knowledge, if any, are so strong as to render the relevant grounds for belief immune to undermining and/or error.
It is safe to say that contemporary modal epistemology is strongly informed by Kripke’s thesis that de re modal knowledge is possible and may be achieved partly due to scientific inquiry (e.g. knowledge that water necessarily contains hydrogen). I will aim to provide an overview of the several ways in which the widespread acceptance of this thesis has drastically shaped the contemporary landscape.
Questions (1) and (2) naturally lead to questions about the metaphysics of modality, not least to questions concerning the reality and nature of essences, possible worlds etc. Question (2) also involves a diagnosis of the epistemic power - within the relevant domains - of processes such as empirical observation, imagining, conceiving, “rational insight” etc. Important questions involve the natures of such methods, and whether they may - even in the best case - merely provide evidence in favour of modal beliefs, or if, e.g., there are modal ties between (some version of) possibility and (ideal) conceivability. Question (3) asks us to probe our general conceptions of epistemic justification and knowledge in the light of the results achieved above. Finally, question (4) asks us to consider whether some sources of modal knowledge, if any, are so strong as to render the relevant grounds for belief immune to undermining and/or error.
It is safe to say that contemporary modal epistemology is strongly informed by Kripke’s thesis that de re modal knowledge is possible and may be achieved partly due to scientific inquiry (e.g. knowledge that water necessarily contains hydrogen). I will aim to provide an overview of the several ways in which the widespread acceptance of this thesis has drastically shaped the contemporary landscape.
- Carlo Proietti
"Fitch Paradox. Reformulation strategies for its solution."
"Fitch Paradox. Reformulation strategies for its solution."
Fitch-Church paradox (1963) consists of a straightforward formal derivation in modal logic to the effect that (a) p Kp entails (b) p Kp. It was only fifteen years after Fitch’s article was published that W.D. Hart interpreted this “unjustly neglected logical gem” as a genuine paradox for verificationism. The reasoning is simple: if “All truth are knowable”[ (a)] entails that “All truths are known” [(b)] then a basic verificationist claim entails a blatant absurdity. Hence, verificationism is debatable on a simply logical ground.
A number of different logical solutions has since then been presented to counter this argument or show its limits. These solutions mostly fall into three categories. (1) Restriction strategies, that limit the universal scope of (a), viz. – in logical words – instances of (a) should not be substitution free. (2) Weakening strategies, which block the derivation of the paradox by invalidating some inference rules of classical logic. (3) Reformulation strategies, that deny that p Kp is indeed an adequate formal rendering of the verificationist thesis and claim that the apparent paradox only follows from propositional (bi)modal logic being too weak to correctly express such thesis.
Here I intend to investigate the rationale behind solutions of kind (3) and to open the formulation of the verification thesis to a wider range of possibilities allowed by first order modal logic. Secondly, I intend to analize the more frequent objections to reformulation, paying particular attention to a “metaphysical” objection, according to which non-actual knowledge of actual truths – that solutions of kind (3) seem to entail – is a problematic notion.
References
Edgington, D. (1985). The paradox of knowability. Mind, 94 :557–568.
Fitch, F. B. (1963). A logical analysis of some value concepts. Journal of Symbolic Logic, 28 :135–142.
Proietti, C. and Sandu, G. (2010). 'Fitch's Paradox and Ceteris Paribus Modalities', Synthese 173 (1), pp. 75‐87.
Rabinowicz, W. and Segerberg, K. (1994). Actual Truth, Possible Knowledge. In Fagin, R., editor, Proceedings of the 5th Conference on Theoretical Aspects of Reasoning about Knowledge, Pacific Grove, CA, USA, March 1994, pages 122–137. Morgan Kaufmann.
Williamson, T. (1987). On the Paradox of Knowability. Mind, 96 :256–261.
A number of different logical solutions has since then been presented to counter this argument or show its limits. These solutions mostly fall into three categories. (1) Restriction strategies, that limit the universal scope of (a), viz. – in logical words – instances of (a) should not be substitution free. (2) Weakening strategies, which block the derivation of the paradox by invalidating some inference rules of classical logic. (3) Reformulation strategies, that deny that p Kp is indeed an adequate formal rendering of the verificationist thesis and claim that the apparent paradox only follows from propositional (bi)modal logic being too weak to correctly express such thesis.
Here I intend to investigate the rationale behind solutions of kind (3) and to open the formulation of the verification thesis to a wider range of possibilities allowed by first order modal logic. Secondly, I intend to analize the more frequent objections to reformulation, paying particular attention to a “metaphysical” objection, according to which non-actual knowledge of actual truths – that solutions of kind (3) seem to entail – is a problematic notion.
References
Edgington, D. (1985). The paradox of knowability. Mind, 94 :557–568.
Fitch, F. B. (1963). A logical analysis of some value concepts. Journal of Symbolic Logic, 28 :135–142.
Proietti, C. and Sandu, G. (2010). 'Fitch's Paradox and Ceteris Paribus Modalities', Synthese 173 (1), pp. 75‐87.
Rabinowicz, W. and Segerberg, K. (1994). Actual Truth, Possible Knowledge. In Fagin, R., editor, Proceedings of the 5th Conference on Theoretical Aspects of Reasoning about Knowledge, Pacific Grove, CA, USA, March 1994, pages 122–137. Morgan Kaufmann.
Williamson, T. (1987). On the Paradox of Knowability. Mind, 96 :256–261.
- Rasmus K. Rendsvig
"Transition Rules for Dynamic Epistemic Logic"
"Transition Rules for Dynamic Epistemic Logic"
In this talk, I will present the notion of "transition rules" for dynamic epistemic logic as well as three applications of such rules. A transition rules is a method for picking the next model transformer (public announcement, action model, etc.) to be applied, picked as a function of satisfied formulas of some epistemic state model. Three applications of transitions rules will be discussed: 1) the use of transition rules for specifying model sequences, i.e. used as localized protocols, 2) the use of transition rules in combination with model transformers that invoke factual change as a method for modelling agent types and their choices and actions, and 3) using transition rules as measure for model transformer strength. The talk is based on ongoing research.
Jakub Szymanik
"Using logic to predict behavior in turn-taking games"
Inspired by the logical analysis of backward induction we study structural properties of a turn-based game called the Marble Drop Game, which is an experimental paradigm designed to investigate higher-order social reasoning. We provide a semantic analysis of the complexity of particular game trials which takes into account alternation type of the game and pay-offs distribution. We show that the cognitive complexity of game trials, measured with respect to reaction time, can be predicted by looking at the structural properties of the game instances. Our predictions of reaction times and reasoning strategies, based on the theoretical analysis of complexity of Marble Drop game instances, are compared to subjects' actual reaction times. This research illustrates how formal methods of logic and computer science can be used to identify the inherent complexity of cognitive tasks. Such analyses can be located between Marr's computational and algorithmic levels.
References:
Jakub Szymanik, Ben Meijering, Rineke Verbrugge. Using intrinsic complexity of turn-taking games to predict participants' reaction times, Proceedings of the 35th Annual Conference of the Cognitive Science Society, forthcoming. (see http://jakubszymanik.com/papers/AlternationsMDGfinal.pdf )
References:
Jakub Szymanik, Ben Meijering, Rineke Verbrugge. Using intrinsic complexity of turn-taking games to predict participants' reaction times, Proceedings of the 35th Annual Conference of the Cognitive Science Society, forthcoming. (see http://jakubszymanik.com/papers/AlternationsMDGfinal.pdf )