LFCS'07: Symposium on Logical Foundations of Computer Science

List of Accepted LFCS`07 Papers.

1. Justified and Common Knowledge: limited conservativity.
   Evangelia Antonakos (City University of New York).
   abstract
   We consider the relative strengths of three formal approaches to public knowledge: “any fool” knowledge by McCarthy (1970), Common Knowledge by Halpern and Moses (1990), and Justified Knowledge by Artemov (2004). Specifically, we show that epistemic systems with the Common Knowledge modality C are conservative with respect to Justified Knowledge systems on formulas χ∧ Cφ→ψ, where χ, φ, and ψ are C-free.
2. The Intensional Lambda Calculus.
   Sergei Artemov (City University of New York) and Eduardo Bonelli (National University of Argentina).
   abstract
   We introduce a natural deduction formulation for the Logic of Proofs, a refinement of modal logic S4 in which the assertion □A is replaced by 〚s〛A whose intended reading is “s is a proof of A”. A term calculus for this formulation yields a typed lambda calculus λ^I that internalises intensional information on how a term is computed. In the same way that the Logic of Proofs internalises its own derivations, λ^I internalises its own computations. Confluence and strong normalisation of λ^I is proved. This system serves as the basis for the study of type theories that internalise intensional aspects of computation.
3. (n,k)-ary Quantifiers in Canonical Systems.
   Arnon Avron and Anna Zamansky (Tel Aviv University).
   abstract
   An (n,k)-ary quantifier is a generalized logical connective, binding k variables and connecting n formulas. Canonical Gentzen-type systems with (n,k)-ary quantifiers are systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of an (n,k)-ary quantifier is introduced. The semantics of such systems for the case of k∈{0,1} are provided in [Zamansky and Avron, 2006] using two-valued non-deterministic matrices (2Nmatrices). A constructive syntactic coherence criterion for the existence of a 2Nmatrix for which a canonical system is strongly sound and complete, is formulated there. In this paper we extend these results from the case of k∈{0,1} to the general case of k≥0. We show that the interpretation of quantifiers in the framework of Nmatrices is not sufficient for the case of k>1 and introduce generalized Nmatrices which allow for a more complex treatment of quantifiers. Then we show that (i) a canonical calculus G is coherent iff there is a 2GNmatrix, for which G is strongly sound and complete, and (ii) any coherent canonical calculus admits cut-elimination.
4. The Universal Modality, the Center of a Heyting Algebra, and the Blok-Esakia Theorem.
   Guram Bezhanishvili (New Mexico State University).
   abstract
   <<<no abstract available>>>
5. Elementary Differential Calculus on Discrete and Hybrid Structures.
   Howard Blair, David Jakel, Robert Irwin, and Angel Rivera (Syracuse University).
   abstract
   We set up differential calculi in the Cartesian-closed category CONV of convergence spaces. The central idea is to uniformly define the 3-place relation __ is a differential of __ at __ for each pair of convergence spaces X,Y in the category, where the first and second arguments are elements of Hom(X,Y) and the third argument is an element of X, in such a way as to (1) obtain the chain rule, (2) have the relation be in agreement with standard definitions from real and complex analysis, and (3) depend only on the convergence structures native to the spaces X and Y. All topological spaces and all reflexive directed graphs (i.e. discrete structures) are included in CONV. Accordingly, ramified hybridizations of discrete and continuous spaces occur in CONV. Moreover, the convergence structure within each space local to each point, individually, can be discrete, continuous, or hybrid.
6. Weighted Distributed Systems and Their Logics.
   Benedikt Bollig (ENS de Cachan) and Ingmar Meinecke (Universität Leipzig).
   abstract
   We provide a model of weighted distributed systems and give a logical characterization thereof. Distributed systems are represented as weighted asynchronous cellular automata. Running over directed acyclic graphs, Mazurkiewicz traces, or (lossy) message sequence charts, they allow for modeling several communication paradigms in a unifying framework, among them probabilistic shared-variable and probabilistic lossy-channel systems. We show that any such system can be described by a weighted existential MSO formula and, vice versa, any formula gives rise to a weighted asynchronous cellular automaton.
7. Weighted O-Minimal Hybrid Systems Are More Decidable Than Weighted Timed Automata!
   Patricia Bouyer, Thomas Brihaye, and Fabrice Chevalier (LSV - CNRS & ENS de Cachan).
   abstract
   We consider weighted o-minimal hybrid systems, which extend classical o-minimal hybrid systems with cost functions. These cost functions are “observer variables” which increase while the system evolves but do not constrain the behaviour of the system. In this paper, we prove two main results: (i) optimal o-minimal hybrid games are decidable; (ii) the model-checking of WCTL, an extension of CTL which can constrain the cost variables, is decidable over that model. This has to be compared with the same problems in the framework of timed automata where both problems are undecidable in general, while they are decidable for the restricted class of one-clock timed automata.
8. On Decidability and Expressiveness of Propositional Interval Neighborhood Logics.
   Davide Bresolin (Università degli Studi di Udine), Valentin Goranko (University of the Witwatersrand), Angelo Montanari (Università degli Studi di Udine), and Guido Sciavicco (University of Murcia).
   abstract
   Interval-based temporal logics are an important research area in computer science and artificial intelligence. In this paper we investigate decidability and expressiveness issues for Propositional Neighborhood Logics (PNLs). We begin by comparing the expressiveness of the different PNLs. Then, we focus on the most expressive one, namely, PNL^π+, and we show that it is decidable over various classes of linear orders by reducing its satisfiability problem to that of the two-variable fragment of first-order logic with binary relations over linearly ordered domains, due to Otto. Next, we prove that PNL^π+ is expressively complete with respect to such a fragment. We conclude the paper by comparing PNL^π+ expressiveness with that of other interval-based temporal logics.
9. Reasoning about Sequences of Memory States.
   Rémi Brochenin, Stéphane Demri, and Étienne Lozes (ENS de Cachan).
   abstract
   In order to verify programs with pointer variables, we introduce a temporal logic LTL^mem whose underlying assertion language is the quantifier-free fragment of separation logic and the temporal logic on the top of it is the standard linear-time temporal logic LTL^mem. We analyze the complexity of various model-checking and satisfiability problems for LTL^mem, considering various fragments of separation logic (including pointer arithmetic), various classes of models (with or without constant heap), and the influence of fixing the initial memory state. We provide a complete picture based on these criteria. Our main decidability result is PSPACE-completeness of the satisfiability problems on the record fragment and on a classical fragment allowing pointer arithmetic. Σ⁰₁-completeness or Σ¹₁-completeness results are established for various problems by reducing standard problems for Minsky machines, and underline the tightness of our decidability results.
10. Cut Elimination in Deduction Modulo by Abstract Completion.
    Guillaume Burel (Université Nancy 1 - LORIA) and Claude Kirchner (INRIA - LORIA).
    abstract
    Deduction Modulo implements Poincaré's principle by identifying deduction and computation as different paradigms and making their interaction possible. This leads to logical systems like the sequent calculus or natural deduction modulo. Even if deduction modulo is logically equivalent to first-order logic, proofs in such systems are quite different and dramatically simpler with one cost: cut elimination may not hold anymore. We prove first that it is even undecidable to know, given a congruence over propositions, if cuts can be eliminated in the sequent calculus modulo this congruence.
    Second, to recover the cut admissibility, we show how computation rules can be added following the classical idea of completion a la Knuth and Bendix. Because in deduction modulo, rewriting acts on terms as well as on propositions, the objects are much more elaborated than for standard completion. Under appropriate hypothesis, we prove that the sequent calculus modulo is an instance of the powerful framework of abstract canonical systems and that therefore, cuts correspond to critical proofs that abstract completion allows us to eliminate.
    In addition to an original and deep understanding of the interactions between deduction and computation and of the expressivity of abstract canonical systems, this provides a mechanical way to transform a sequent calculus modulo into an equivalent one admitting the cut rule, therefore extending in a significant way the applicability of mechanized proof search in deduction modulo.
11. Density Elimination and Rational Completeness for First-Order Logics.
    Agata Ciabattoni (Vienna University of Technology) and George Metcalfe (Vanderbilt University).
    abstract
    Density elimination by substitutions is introduced as a uniform method for removing applications of the Takeuti-Titani density rule from proofs in first-order hypersequent calculi. For a large class of calculi, density elimination by this method is guaranteed by known sufficient conditions for cut-elimination. Moreover, adding the density rule to any axiomatic extension of a simple first-order logic gives a logic that is rational complete; i.e., complete with respect to linearly and densely ordered algebras: a precursor to showing that it is a fuzzy logic (complete for algebras with a real unit interval lattice reduct). Hence the sufficient conditions for cut-elimination guarantee rational completeness for a large class of first-order substructural logics.
12. Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus.
    Robert Constable and Wojciech Moczydłowski (Cornell University).
    abstract
    We prove constructively that for any propositional formula φ in Conjunctive Normal Form, we can either find a satisfying assignment of true and false to its variables, or a refutation of φ showing that it is unsatisfiable. This refutation is a resolution proof of ¬φ. From the formalization of our proof in Coq, we extract Robinson's famous resolution algorithm as a Haskell program correct by construction. The account is an example of the genre of highly readable formalized mathematics.
13. Topological Semantics and Bisimulations for Intuitionistic Modal Logics, and their Classical Companion Logics.
    Jen Davoren (The University of Melbourne).
    abstract
    We take the well-known intuitionistic modal logic of Fischer Servi with semantics in bi-relational Kripke frames, and give the natural extension to topological Kripke frames. Fischer Servi's two interaction conditions relating the intuitionistic pre-order (or partial-order) with the modal accessibility relation generalise to the requirement that the relation and its inverse be lower semi-continuous with respect to the topology. We then investigate the notion of topological bisimulation relations between topological Kripke frames, as introduced by Aiello and van Benthem, and show that their topology-preserving conditions are equivalent to the properties that the inverse-relation and the relation are lower semi-continuous with respect to the topologies on the two models. Our first main result is that this notion of topological bisimulation yields semantic preservation w.r.t. topological Kripke models for both intuitionistic tense logics, and for their classical companion multi-modal logics in the setting of the Gödel translation. After giving canonical topological Kripke models for the Hilbert-style axiomatizations of the Fischer Servi logic and its classical multi-modal companion logic, we show that the syntactic Gödel translation induces a natural semantic map from the intuitionistic canonical model into the canonical model of the classical companion logic, and this map is itself a topological bisimulation.
14. Decidable Temporal Logic with Repeating Values.
    Stéphane Demri (LSV, ENS de Cachan), Deepak D'Souza (IISC, Bangalore), and Régis Gascon (LSV, ENS de Cachan).
    abstract
    Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this paper, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets. This is a surprising result since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier.
15. Model Checking Knowledge and Linear Time: PSPACE Cases.
    Kai Engelhardt, Peter Gammie, and Ron van der Meyden (University of New South Wales, Australia).
    abstract
    We present a general algorithm scheme for model checking logics of knowledge, common knowledge and linear time, based on bisimulations to a class of structures that capture the way that agents update their knowledge. We show that the scheme leads to PSPACE implementations of model checking the logic of knowledge and linear time in several special cases: perfect recall systems with a single agent or in which all communication is by synchronous broadcast, and systems in which knowledge is interpreted using either the agents' current observation only or its current observation and clock value. In all these results, common knowledge operators may be included in the language. Matching lower bounds are provided, and it is shown that although the complexity bound matches the PSPACE complexity of the linear time temporal logic LTL, as a function of the model size the problems considered have a higher complexity than LTL.
16. Realizations and LP.
    Melvin Fitting (City University of New York).
    abstract
    LP can be seen as a logic of knowledge with justifications. Artemov's Realization Theorem says justifications can be extracted from validities in the Hintikka-style logic of knowledge S4, where they are not explicitly present. We provide tools for reasoning about justifications directly. Among other things, we provide machinery for combining two realizations of the same formula, and for replacing subformulas by equivalent subformulas. The results are algorithmic in nature—semantics for LP plays no role. We apply our results to provide a new algorithmic proof of Artemov's Realization Theorem itself.
17. Successive Abstractions of Hybrid Automata for Monotonic CTL Model Checking.
    Raffaella Gentilini (University of Kaiserslautern), Klaus Schneider (TU Kaiserslautern), and Bud Mishra (New York University).
    abstract
    Current symbolic techniques for the automated reasoning over undecidable hybrid automata, force one to choose between the refinement of either an overapproximation or an underapproximation of the set of reachable states. When the analysis of branching time temporal properties is considered, the literature has developed a number of abstractions techniques based on the simulation preorder, that allow the preservation of only true universally quantified formulæ.
    This paper suggests a way to surmount these difficulties by defining a succession of abstractions of hybrid automata, which not only (1) allow the detection and the refinement of both over- and under-approximated reachable sets symmetrically, but also (2) preserves the full set of branching time temporal properties (when interpreted on a dense time domain). Moreover, our approach imposes on the corresponding set of abstractions a desirable monotonicity property with respect to the set of model-checked formulæ.
18. Explicit Proofs in Formal Provability Logic.
    Evan Goris (City University of New York).
    abstract
    In this paper we answer the question what implicit proof assertions in the provability logic GL can be realized by explicit proof terms. In particular we show that the fragment of GL which can be realized by generalized proof terms of GLA is exactly S4∩GL and equals the fragment that can be realized by proof-terms of LP. In the final sections of this paper we establish the disjunction property for GLA and give an axiomatization for S4∩GL.
19. A Synthesis Algorithm for Hybrid Systems.
    Srikanth Gottipati (City University of New York) and Anil Nerode (Cornell University).
    abstract
    Hybrid systems are systems of continuous plants, subject to disturbances, interacting with sequential automata in a network. By the synthesis problem for hybrid systems we mean extracting a finite state digital controller automaton from the system equations, constraints, and cost function which define the hybrid system. This automaton senses system state, and on the basis of its state, changes state and issues a chattering control to the actuators to control the system with epsilon optimal control for a fixed epsilon in real time. We address this problem by extracting a local cost function for the control system which transforms the infinite-dimensional optimization problem into a finite-dimensional problem.
20. Including the Past in ‘Topologic’.
    Bernhard Heinemann (FernUniversität in Hagen).
    abstract
    In this paper, we extend Moss and Parikh's topo-logical view of knowledge. We incorporate a further modality, denoted P, into the original system. This operator describes the increase of sets. Regarding the usual logic of knowledge, P corresponds to no learning of agents. In the context of ‘topologic’, however, P represents the reverse effort operator and is related to the past therefore. It is our objective to prove nice properties of the accompanying logic like soundness and completeness with respect to the intended class of structures, or decidability. To this end, we take up a hybrid logic point of view, among other things. This not only yields the desired results, but also has some interesting consequences with regard to applications.
21. A Note on Rewriting Proofs and Fibonacci Numbers.
    Max Kanovich (University of London).
    abstract
    One basic activity in combinatorics is to establish combinatorial identities by so-called ‘bijective proofs,’ which amounts to constructing explicit bijections between two types of the combinatorial objects in question. The aim of this paper is to show how techniques from the formal logic world can be applied directly to such problems studied completely independently in the world of combinatorics. The basic idea is to characterize equinumerous partition ideals in terms of the minimal elements generating the order filters, the complements to the original ideals. For the case where the minimal elements of each of these order filters are disjoint, we have developed a general automated method to remove the mystery of certain known results and establish new results in the theory of integer partitions: Kanovich [Finding direct partition bijections by two-directional rewriting techniques. Discrete Math., 285 (1-3) (2004) 151-166], and Kanovich [The two-way rewriting in action: Removing the mystery of Euler-Glaisher's map. Discrete Math., (2006), doi:10.1016/j.disc.2006.10.005]. Here we address the case of filters having overlapping minimal elements. Essentially this is a case study related to the Fibonacci numeration system. In addition to a ‘bijective proof’ for Zeckendorf's theorem - that every positive integer is uniquely representable within the Fibonacci numeration system, we establish ‘bijective proofs’ for a new series of partition identities related to Fibonacci and Lucas numbers. The main result is proved using the idea of filter supports, and rewriting systems on multisets having overlapping patterns. The main technical step is a suitable construction of such a rewriting system and then a proof that this rewriting system and the system consisting of its reverse rewriting rules, both have the Church-Rosser property, with providing the bijections we are looking for.
22. On Complexity of Ehrenfeucht-Fraïssé Games.
    Bakhadyr Khoussainov and Jiamou Liu (The University of Auckland).
    abstract
    In this paper we initiate the study of Ehrenfeucht-Fraïssé games for some standard finite structures. Examples of such standard structures are equivalence relations, trees, unary relation structures, Boolean algebras, and some of their natural expansions. The paper concerns the following question that we call Ehrenfeucht-Fraïssé problem. Given n∈ω as a parameter, two relational structures A and B from one of the classes of structures mentioned above, how efficient is it to decide if Duplicator wins the n-round EF game G_n(A,B)? We provide algorithms for solving the Ehrenfeucht-Fraïssé problem for the mentioned classes of structures. The running times of all the algorithms are bounded by constants. We obtain the values of these constants as functions of n.
23. The Law of the Iterated Logarithm for Algorithmically Random Brownian Motion.
    Bjørn Kjos-Hanssen and Anil Nerode (Cornell University).
    abstract
    Algorithmic randomness is most often studied in the setting of the fair-coin measure on the Cantor space, or equivalently Lebesgue measure on the unit interval. It has also been considered for the Wiener measure on the space of continuous functions. Answering a question of Fouché, we show that Khintchine's law of the iterated logarithm holds at almost all points for each Martin-Löf random path of Brownian motion. In the terminology of Fouché, these are the complex oscillations. The main new idea of the proof is to take advantage of the Wiener-Carathéodory measure algebra isomorphism theorem.
24. Hypersequent Calculus for Intuitionistic Logic with Classical Atoms.
    Hidenori Kurokawa (City University of New York).
    abstract
    We introduce a hypersequent calculus for intuitionistic logic with classical atoms, i.e. intuitionistic logic augmented with a special class of propositional variables for which we postulate the decidability property. This system combines classical logical reasoning with constructive and computationally oriented intuitionistic logic in one system. Our main result is the cut-elimination theorem with the subformula property for this system. We show this by a semantic method, namely via proving the completeness theorem of the hypersequent calculus without the cut rule. The cut-elimination theorem gives a semantic completeness of the system, decidability, and some form of the disjunction property.
25. Proof Identity for Classical Logic: Generalizing to Normality.
    Roman Kuznets (City University of New York).
    abstract
    The problem of the identity criteria for proofs can be traced to Hilbert and Prawitz. One of the approaches, which uses the concept of generality of proofs, was suggested in 1968 by Lambek. Following his ideas, we propose a language and a logic to represent Hilbert-style proofs for classical propositional logic by adapting the Logic of Proofs LP introduced by Artemov in 1994. We prove that proof polynomials, the objects representing Hilbert derivations in LP, are sufficient to realize all propositional derivations, with or without hypotheses. We also show that proof polynomials respect the ideas of generality and provide an algorithm for determining whether two given proof polynomials represent the same proof. These results naturally extend similar properties of combinatory logic demonstrated by Hindley. The language of LP allows us to formally capture more structure of Hilbert-style proofs. In particular, we show how the well-known phenomenon of proof composition in classical logic manifests itself in the case of Hilbert proofs.
26. On the Constructive Dedekind Reals.
    Robert Lubarsky (Florida Atlantic University) and Michael Rathjen (University of Leeds).
    abstract
    In order to built the collection of Cauchy reals as a set in constructive set theory, the only Power Set-like principle needed is Exponentiation. In contrast, the proof that the Dedekind reals form a set has seemed to require more than that. The main purpose here is to show that Exponentiation alone does not suffice for the latter, by furnishing a Kripke model of constructive set theory, CZF with Subset Collection replaced by Exponentiation, in which the Cauchy reals form a set while the Dedekind reals constitute a proper class.
27. Verifying Balanced Trees.
    Zohar Manna, Henny Sipma (Stanford University), and Ting Zhang (Microsoft Research Asia)
    abstract
    Balanced search trees provide guaranteed worst-case time performance and hence they form a very important class of data structures. However, the self-balancing ability comes at a price; balanced trees are more complex than their unbalanced counterparts both in terms of data structure themselves and related manipulation operations. In this paper we present a framework to model balanced trees in decidable first-order theories of term algebras with Presburger arithmetic. In this framework, a theory of term algebras (i.e., a theory of finite trees) is extended with Presburger arithmetic and with certain connecting functions that map terms (trees) to integers. Our framework is flexible in the sense that we can obtain a variety of decidable theories by tuning the connecting functions. By adding maximal path and minimal path functions, we obtain a theory of red-black trees in which the transition relation of tree self-balancing (rotation) operations is expressible. We then show how to reduce the verification problem of the red-black tree algorithm to constraint satisfiability problems in the extended theory.
28. Compactness Properties for Stable Semantics of Logic Programs.
    Victor Marek (University of Kentucky) and Jeffrey Remmel (University of California San Diego).
    abstract
    Logic programming with stable logic semantics (SLP) is a logical formalism that assigns to sets of clauses in the language admitting negations in the bodies a special kind of models, called stable models. This formalism does not have the compactness property. We show a number of conditions that entail a form of compactness for SLP.
29. Uniform Circuits, & Boolean Proof Nets.
    Virgile Mogbil and Vincent Rahli (Université Paris 13).
    abstract
    The relationship between Boolean proof nets of multiplicative linear logic APN and Boolean circuits has been studied [Terui, 2004] in a non-uniform setting. We refine this results by taking care of uniformity: the relationship can be expressed in term of the (Turing) polynomial hierarchy. We give a proofs-as-programs correspondence between proof nets and deterministic as well as non-deterministic Boolean circuits with a uniform depth-preserving simulation of each other. The Boolean proof nets class m&BN(poly) is built on multiplicative and additive linear logic with a polynomial amount of additive connectives as the non-deterministic circuit class NNC(poly) is with non-deterministic variables. We obtain uniform-APN=NC and m&BN(poly)=NNC(poly)=NP.
30. Finite Automata Presentable Abelian Groups.
    André Nies and Pavel Semukhin (The University of Auckland).
    abstract
    We give new examples of FA presentable torsion-free abelian groups. Namely, for every n≥2, we construct a rank n indecomposable torsion-free abelian group which has an FA presentation. We also construct an FA presentation of the group (Z,+)² in which every nontrivial cyclic subgroup is not FA recognizable.
31. Embeddings into Free Heyting Algebras and Translations into Intuitionistic Propositional Logic.
    Michael O'Connor (Cornell University).
    abstract
    We find a translation with particularly nice properties from intuitionistic propositional logic in countably many variables to intuitionistic propositional logic in two variables. In addition, the existence of a possibly-not-as-nice translation from any countable logic into intuitionistic propositional logic in two variables is shown. The nonexistence of a translation from classical logic into intuitionistic propositional logic which preserves ∧ and ∨ but not necessarily Τ is proven. These results about translations follow from additional results about embeddings into free Heyting algebras.
32. Some Puzzles about Probability and Probabilistic Conditionals.
    Rohit Parikh (City University of New York).
    abstract
    We examine some old and new paradoxes of probability, give a rough account of probabilistic conditionals, and prove a new result about non-monotonicity in probabilistic conditionals. It is well known that such conditionals are not monotonic – a conditional which is true can become false when additional hypotheses are added. We show that nonetheless, the conditionals are usually, monotonic, or roughly speaking that we do not actually have to worry about non-monotonicity in practice.
33. A Temporal Dynamic Logic for Verifying Hybrid System Invariants.
    André Platzer (University of Oldenburg).
    abstract
    We combine first-order dynamic logic for reasoning about possible behaviour of hybrid systems with temporal logic for reasoning about the temporal behaviour during their operation. Our logic supports verification of hybrid programs with first-order definable flows and provides a uniform treatment of discrete and continuous evolution. For our combined logic, we generalise the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of dynamic logic. On this basis, we provide a modular verification calculus that reduces correctness of temporal behaviour of hybrid systems to non-temporal reasoning. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints.
34. Multiplexor Categories and Models of Soft Linear Logic.
    Brian Redmond (University of Ottawa).
    abstract
    We give a categorical interpretation of Lafont's Soft Linear Logic, a logical system complete for polynomial time computation, in terms of multiplexor categories. We present two main classes of models and methods for constructing examples in each case. As a concrete example of the first type, we introduce a simple game semantics for Multiplicative Soft Linear Logic. To illustrate the second type, we give a realizability model and a new proof of the polytime soundness of Soft Linear Logic. These results further our semantic understanding of Soft Linear Logic and polynomial time.
35. Until-Since Temporal Logic Based on Parallel Time with Common Past. Deciding Algorithms.
    Vladimir Rybakov (Manchester Metropolitan University).
    abstract
    We present a framework for constructing algorithms recognizing admissible inference rules (consecutions) in temporal logics with Until and Since based on Kripke/Hintikka structures modeling parallel time with common past. Logics PTL_α with various branching factor α∈N∪{ω} after common past are considered. The offered technique looks rather flexible, for instance, with similar approach we showed [Rybakov, 2006] that temporal logic based on sheafs of integer numbers with common origin is decidable by admissibility. In this paper we extend obtained algorithms to logics PTL_α. We prove that any logic PTL_α is decidable w.r.t. admissible consecutions (inference rules), as a consequence, we solve satisfiability problem and show that any PTL_α itself is decidable.
36. Total Public Announcements.
    David Steiner and Thomas Studer (University of Bern).
    abstract
    We present a dynamic epistemic logic for knowledge change of rational agents. Existing approaches only deal with partial public announcements, that means an announcement may lead to an inconsistent state. We introduce an extension of the multi-modal logic S5_n featuring total public announcements where an update cannot result in an inconsistency. We also study total public announcements in the context of common knowledge and relativized common knowledge.