Separation logic and logics with team semantics

Separation logic is a successful logical system for formal reasoning about programs that mutate their data structures. Team semantics, on the other side, is the basis of modern logics of dependence and independence. Separation logic and team semantics have been introduced with quite different motivations, and are investigated by research communities with rather different backgrounds and objectives. Nevertheless, there are obvious similarities between these formalisms. Both separation logic and logics with team semantics involve the manipulation of second-order objects, such as heaps and teams, by first-order syntax without reference to second-order variables. Moreover, these semantical objects are closely related; it is for instance obvious that a heap can be seen as a team, and the separating conjunction of separation logic is (essentially) the same as the team-semantical disjunction. Based on such similarities, the possible connections between separation logic and team semantics have been raised as a question at several occasions, and lead to informal discussions between these research communities. The objective of this paper is to make this connection precise, and to study its potential but also its obstacles and limitations.     

On elementary logics for quantitative dependencies

We define and study logics in the framework of probabilistic team semantics and over metafinite structures. Our work is paralleled by the recent development of novel axiomatizable and tractable logics in team semantics that are closed under the Boolean negation. Our logics employ new probabilistic atoms that resemble so-called extended atoms from the team semantics literature. We also define counterparts of our logics over metafinite structures and show that all of our logics can be translated into functional fixed point logic implying a polynomial time upper bound for data complexity with respect to BSS-computations.     

On the Presburger fragment of logics with multiteam semantics

In team semantics, which is the basis of modern logics of dependence and independence, formulae are evaluated on sets of assignments, called teams. Multiteam semantics instead takes mulitplicities of data into account and is based on multisets of assignments, called multiteams. Logics with multiteam semantics can be embedded into a two-sorted variant of existential second-order logics, with arithmetic operations on multiplicities. Here we study the Presburger fragment of such logics, permitting only addition, but not multiplication on multiplicities. It can be shown that this fragment corresponds to inclusion-exclusion logic in multiteam semantics, but, in contrast to the situation in team semantics, that it is strictly contained in independence logic. We give different characterisations of this fragment by various atomic dependency notions.     

Properties of Tense Logics

Based on the results of [11] this paper delivers uniform algorithms for deciding whether a finitely axiomatizable tense logic

• has the finite model property,
• is complete with respect to Kripke semantics,
• is strongly complete with respect to Kripke semantics,
• is d-persistent,
• is r-persistent.

It is also proved that a tense logic is strongly complete iff the corresponding variety of bimodal algebras is complex, and that a tense logic is d-persistent iff it is complete and its Kripke frames form a first order definable class. From this we obtain many natural non-d-persistent tense logics whose corresponding varieties of bimodal algebras are complex. Mathematics Subject Classification: 03B45, 03B25.     

Speech acts, commitment and multi-agent communication

The principle aim of this paper is to reconsider the suitability of Austin and Searle’s Speech Act theory as a basis for agent communication languages. Two distinct computational interpretations of speech acts are considered: the standard “mentalistic” approach associated with the work of Cohen and Levesque which involves attributing beliefs and intentions to artificial agents, and the “social semantics” approach originating (in the context of MAS) with Singh which aims to model commitments that agents undertake as a consequence of communicative actions. Modifications and extensions are proposed to current commitment-based analyses, drawing on recent philosophical studies by Brandom, Habermas and Heath. A case is made for adopting Brandom’s framework of normative pragmatics, modelling dialogue states as deontic scoreboards which keep track of commitments and entitlements that speakers acknowledge and hearers attribute to other interlocutors. The paper concludes by outlining an update semantics and protocol for selected locutions. Rodger Kibble is a Lecturer in the Department of Computing, Goldsmiths College, University of London. He has worked as a researcher at the Information Technology Research Institute, University of Brighton, and the School of Oriental and African Studies, University of London. He received his PhD from the Centre for Cognitive Science in the University of Edinburgh in 1997. He has published conference papers and journal articles in the formal semantics of natural language, natural language generation, anaphora resolution, dialogue modelling, argumentation and multi-agent communication; and coedited Information Sharing: Reference and Presupposition in Language Generation and Interpretation (CSLI, 2002).     

Tarski's theorem on intuitionistic logic,for polyhedra

In 1938, Tarski proved that a formula is not intuitionistically valid if, and only if, it has a counter-model in the Heyting algebra of open sets of some topological space. In fact, Tarski showed that any Euclidean space ${\mathbb{R}}^n$ with $n?1$ suffices, as does e.g. the Cantor space. In particular, intuitionistic logic cannot detect topological dimension in the Heyting algebra of all open sets of a Euclidean space. By contrast, we consider the lattice of open subpolyhedra of a given compact polyhedron $P?{\mathbb{R}}^n$, prove that it is a locally finite Heyting subalgebra of the (non-locally-finite) algebra of all open sets of P, and show that intuitionistic logic is able to capture the topological dimension of P through the bounded-depth axiom schemata. Further, we show that intuitionistic logic is precisely the logic of formulæ valid in all Heyting algebras arising from polyhedra in this manner. Thus, our main theorem reconciles through polyhedral geometry two classical results: topological completeness in the style of Tarski, and Ja?kowski's theorem that intuitionistic logic enjoys the finite model property. Several questions of interest remain open. E.g., what is the intermediate logic of all closed triangulable manifolds?     

Axiomatizations of team logics

In a modular approach, we lift Hilbert-style proof systems for propositional, modal and first-order logic to generalized systems for their respective team-based extensions. We obtain sound and complete axiomatizations for the dependence-free fragment FO(～) of Väänänen's first-order team logic TL, for propositional team logic PTL, quantified propositional team logic QPTL, modal team logic MTL, and for the corresponding logics of dependence, independence, inclusion and exclusion.As a crucial step in the completeness proof, we show that the above logics admit, in a particular sense, a semantics-preserving elimination of modalities and quantifiers from formulas.     

On the fuzzy team decision in a changing environment

This paper formulates a fuzzy team decision problem in a changing environment. The concept of a fuzzy set is introduced to formulate the team decision processes in a dynamic environment which contains fuzzy states, fuzzy information functions, fuzzy information signals, fuzzy decision functions and fuzzy actions.