Volume
LIPIcs, Volume 23
Computer Science Logic 2013 (CSL 2013)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Event
CSL 2013, September 2-5, 2013, Torino, ItalyEditor
Publication Details
- published at: 2013-09-02
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-60-6
- DBLP: db/conf/csl/csl2013
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 23, CSL'13, Complete Volume
Abstract
LIPIcs, Volume 23, CSL'13, Complete Volume
Cite as
Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@Proceedings{ronchidellarocca:LIPIcs.CSL.2013,
title = {{LIPIcs, Volume 23, CSL'13, Complete Volume}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013},
URN = {urn:nbn:de:0030-drops-42618},
doi = {10.4230/LIPIcs.CSL.2013},
annote = {Keywords: Conference Proceedings, Theory of Computation, Distributed Systems, Software/ Programs Verifications, Formal Definitions and Theory Languages Constructs and Features, Knowledge Representations Formalisms and Methods}
}
Document
Front Matter
Frontmatter, Table of Contents, Preface, Conference Organization
Abstract
Frontmatter, Table of Contents, Preface, Conference Organization
Cite as
Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. i-xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{ronchidellarocca:LIPIcs.CSL.2013.i,
author = {Ronchi Della Rocca, Simona},
title = {{Frontmatter, Table of Contents, Preface, Conference Organization}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {i--xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.i},
URN = {urn:nbn:de:0030-drops-41821},
doi = {10.4230/LIPIcs.CSL.2013.i},
annote = {Keywords: Frontmatter, Table of Contents, Preface, Conference Organization}
}
Document
The Ackermann Award 2013
Abstract
Report on the Ackermann Award 2013.
Cite as
Anuj Dawar, Thomas A. Henzinger, and Damian Niwiński. The Ackermann Award 2013. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{dawar_et_al:LIPIcs.CSL.2013.1,
author = {Dawar, Anuj and Henzinger, Thomas A. and Niwi\'{n}ski, Damian},
title = {{The Ackermann Award 2013}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {1--4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.1},
URN = {urn:nbn:de:0030-drops-41837},
doi = {10.4230/LIPIcs.CSL.2013.1},
annote = {Keywords: Ackermann award}
}
Document
Invited Talk
Res Publica: The Universal Model of Computation (Invited Talk)
Abstract
We proffer a model of computation that encompasses a broad variety of contemporary generic models, such as cellular automata---including dynamic ones, and abstract state machines---incorporating, as they do, interaction and parallelism. We ponder what it means for such an intertwined system to be effective and note that the suggested framework is ideal for representing continuous-time and asynchronous systems.
Cite as
Nachum Dershowitz. Res Publica: The Universal Model of Computation (Invited Talk). In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 5-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{dershowitz:LIPIcs.CSL.2013.5,
author = {Dershowitz, Nachum},
title = {{Res Publica: The Universal Model of Computation}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {5--10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.5},
URN = {urn:nbn:de:0030-drops-41844},
doi = {10.4230/LIPIcs.CSL.2013.5},
annote = {Keywords: Models of computation, cellular automata, abstract state machines, causal dynamics, interaction}
}
Document
Invited Talk
Three lightings of logic (Invited Talk)
Abstract
Whether we deal with foundations or computation, logic relates questions and answers, typically formulas and proofs: a very entangled relation due to the abuse of presuppositions.
In order to analyse syntax, we should step out from language, which is quite impossible. However, it is enough to step out from meaning: this is why our first lighting of logic is that of answers: it is possible to deal with them as meaningless artifacts assuming two basic states, implicit and explicit. The process of explicitation (a.k.a. normalisation, execution), which aims at making explicit what is only implicit, is fundamentally hazardous.
The second light is that of questions whose choice involves a formatting ensuring the convergence of explicitation, i.e., the existence of "normal forms". This formatting can be seen as the emergence of meaning. It is indeed a necessary nuisance; either too laxist or too coercitive, there is no just format. Logic should avoid the pitfall of Prussian, axiomatic, formats by trying to understand which deontic dialogue is hidden behind logical restrictions.
The third lighting, certainty deals with the adequation between answers and questions: how do we know that an answer actually matches a question? Apodictic certainty -- beyond a reasonable doubt -- is out of reach: we can only hope for epidictic, i.e., limited, reasonable, certainty. Under the second light (questions), we see that the format is made of two opposite parts, namely rights and duties, and that logical deduction relies on a strict balance between these two opposite terms, expressed by the identity group "A is A and conversely". The issue of certainty thus becomes the interrogation: "Can we afford the rights of our duties?"
Cite as
Jean-Yves Girard. Three lightings of logic (Invited Talk). In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 11-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{girard:LIPIcs.CSL.2013.11,
author = {Girard, Jean-Yves},
title = {{Three lightings of logic}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {11--23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.11},
URN = {urn:nbn:de:0030-drops-41852},
doi = {10.4230/LIPIcs.CSL.2013.11},
annote = {Keywords: Proof theory}
}
Document
Invited Talk
From determinism, non-determinism and alternation to recursion schemes for P, NP and Pspace (Invited Talk)
Abstract
Our goal is to approach the classes of computational complexity P, NP, and Pspace in a recursion-theoretic manner. Here we emphasize the connection between the structure of the recursion schemes and the underlying models of computation.
Cite as
Isabel Oitavem. From determinism, non-determinism and alternation to recursion schemes for P, NP and Pspace (Invited Talk). In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 24-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{oitavem:LIPIcs.CSL.2013.24,
author = {Oitavem, Isabel},
title = {{From determinism, non-determinism and alternation to recursion schemes for P, NP and Pspace}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {24--27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.24},
URN = {urn:nbn:de:0030-drops-41865},
doi = {10.4230/LIPIcs.CSL.2013.24},
annote = {Keywords: Computational complexity, Recursion schemes, P, NP, Pspace}
}
Document
Invited Talk
Means and Limits of Decision (Invited Talk)
Abstract
In this talk we survey recent work in the quest for expressive logics with good algorithmic properties, starting from the two-variable fragment of first-order logic and the guarded fragment. While tracing the boundary between decidable and undecidable fragments we describe their power, limitations, similarities and differences in order to stress out key properties responsible for their good or bad behaviour. We also highlight tools and techniques that have proven most effective for designing optimal algorithms, special attention giving to the more universal ones.
Cite as
Lidia Tendera. Means and Limits of Decision (Invited Talk). In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 28-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{tendera:LIPIcs.CSL.2013.28,
author = {Tendera, Lidia},
title = {{Means and Limits of Decision}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {28--29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.28},
URN = {urn:nbn:de:0030-drops-41870},
doi = {10.4230/LIPIcs.CSL.2013.28},
annote = {Keywords: classical decision problem, decidability, computational complexity, two-variable first-order logic, guarded logic}
}
Document
On closure ordinals for the modal mu-calculus
Abstract
The closure ordinal of a formula of modal mu-calculus mu X phi is the least ordinal kappa, if it exists, such that the denotation of the formula and the kappa-th iteration of the monotone operator induced by phi coincide across all transition systems (finite and infinite). It is known that for every alpha < omega^2 there is a formula phi of modal logic such that mu X phi has closure ordinal alpha (Czarnecki 2010). We prove that the closure ordinals arising from the alternation-free fragment of modal mu-calculus (the syntactic class capturing Sigma_2 \cap Pi_2) are bounded by omega^2. In this logic satisfaction can be characterised in terms of the existence of tableaux, trees generated by systematically breaking down formulae into their constituents according to the semantics of the calculus. To obtain optimal upper bounds we utilise the connection between closure ordinals of formulae and embedded order-types of the corresponding tableaux.
Cite as
Bahareh Afshari and Graham E. Leigh. On closure ordinals for the modal mu-calculus. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 30-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{afshari_et_al:LIPIcs.CSL.2013.30,
author = {Afshari, Bahareh and Leigh, Graham E.},
title = {{On closure ordinals for the modal mu-calculus}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {30--44},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.30},
URN = {urn:nbn:de:0030-drops-41889},
doi = {10.4230/LIPIcs.CSL.2013.30},
annote = {Keywords: Closure ordinals, Modal mu-calculus, Tableaux}
}
Document
Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1
Abstract
We present a new Curry-Howard correspondence for HA + EM_1, constructive Heyting Arithmetic with the excluded middle on \Sigma^0_1-formulas. We add to the lambda calculus an operator ||_a which represents, from the viewpoint of programming, an exception operator with a delimited scope, and from the viewpoint of logic, a restricted version of the excluded middle. We motivate the restriction of the excluded middle by its use in proof mining; we introduce new techniques to prove strong normalization for HA + EM_1 and the witness property for simply existential statements. One may consider our results as an application of the ideas of Interactive realizability, which we have adapted to the new setting and used to prove our main theorems.
Cite as
Federico Aschieri, Stefano Berardi, and Giovanni Birolo. Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 45-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{aschieri_et_al:LIPIcs.CSL.2013.45,
author = {Aschieri, Federico and Berardi, Stefano and Birolo, Giovanni},
title = {{Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {45--60},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.45},
URN = {urn:nbn:de:0030-drops-41894},
doi = {10.4230/LIPIcs.CSL.2013.45},
annote = {Keywords: Interactive realizability, classical Arithmetic, witness extraction, delimited exceptions}
}
Document
Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy
Abstract
Given two structures G and H distinguishable in FO^k (first-order logic with k variables), let A^k(G,H) denote the minimum alternation depth of a FO^k formula distinguishing G from H. Let A^k(n) be the maximum value of A^k(G,H) over n-element structures. We prove the strictness of the quantifier alternation hierarchy of FO^2 in a strong quantitative form, namely A^2(n) >= n/8-2, which is tight up to a constant factor. For each k >= 2, it holds that A^k(n) > log_(k+1) n-2 even over colored trees, which is also tight up to a constant factor if k >= 3. For k >= 3 the last lower bound holds also over uncolored trees, while the alternation hierarchy of FO^2 collapses even over all uncolored graphs.
We also show examples of colored graphs G and H on n vertices that can be distinguished in FO^2 much more succinctly if the alternation number is increased just by one: while in Sigma_i it is possible to distinguish G from H with bounded quantifier depth, in Pi_i this requires quantifier depth Omega(n2). The quadratic lower bound is best possible here because, if G and H can be distinguished in FO^k with i quantifier alternations, this can be done with quantifier depth n^(2k-2).
Cite as
Christoph Berkholz, Andreas Krebs, and Oleg Verbitsky. Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 61-80, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{berkholz_et_al:LIPIcs.CSL.2013.61,
author = {Berkholz, Christoph and Krebs, Andreas and Verbitsky, Oleg},
title = {{Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {61--80},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.61},
URN = {urn:nbn:de:0030-drops-41907},
doi = {10.4230/LIPIcs.CSL.2013.61},
annote = {Keywords: Alternation hierarchy, finite-variable logic}
}
Document
Unambiguity and uniformization problems on infinite trees
Abstract
A nondeterministic automaton is called unambiguous if it has at most one accepting run on every input. A regular language is called unambiguous if there exists an unambiguous automaton recognizing this language. Currently, the class of unambiguous languages of infinite trees is not well-understood. In particular, there is no known decision procedure verifying if a given regular tree language is unambiguous. In this work we study the self-dual class of bi-unambiguous languages - languages that are unambiguous and their complement is also unambiguous. It turns out that thin trees (trees with only countably many branches) emerge naturally in this context.
We propose a procedure P designed to decide if a given tree automaton recognizes a bi-unambiguous language. The procedure is sound for every input. It is also complete for languages recognisable by deterministic automata. We conjecture that P is complete for all inputs but this depends on a new conjecture stating that there is no MSO-definable choice function on thin trees. This would extend a result by Gurevich and Shelah on the undefinability of choice on the binary tree.
We provide a couple of equivalent statements to our conjecture, we also give several related results about uniformizability on thin trees. In particular, we provide a new example of a language that is not unambiguous, namely the language of all thin trees. The main tool in our studies are algebras that can be seen as an adaptation of Wilke algebras to the case of infinite trees.
Cite as
Marcin Bilkowski and Michał Skrzypczak. Unambiguity and uniformization problems on infinite trees. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 81-100, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{bilkowski_et_al:LIPIcs.CSL.2013.81,
author = {Bilkowski, Marcin and Skrzypczak, Micha{\l}},
title = {{Unambiguity and uniformization problems on infinite trees}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {81--100},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.81},
URN = {urn:nbn:de:0030-drops-41916},
doi = {10.4230/LIPIcs.CSL.2013.81},
annote = {Keywords: nondeterministic automata, infinite trees, MSO logic}
}
Document
A characterization of the Taylor expansion of lambda-terms
Abstract
The Taylor expansion of lambda-terms, as introduced by Ehrhard and Regnier, expresses a lambda-term as a series of multi-linear terms, called simple terms, which capture bounded computations. Normal forms of Taylor expansions give a notion of infinitary normal forms, refining the notion of Böhm trees in a quantitative setting.
We give the algebraic conditions over a set of normal simple terms which characterize the property of being the normal form of the Taylor expansion of a lambda-term. From this full completeness result, we give further conditions which semantically describe normalizable and total lambda-terms.
Cite as
Pierre Boudes, Fanny He, and Michele Pagani. A characterization of the Taylor expansion of lambda-terms. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 101-115, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{boudes_et_al:LIPIcs.CSL.2013.101,
author = {Boudes, Pierre and He, Fanny and Pagani, Michele},
title = {{A characterization of the Taylor expansion of lambda-terms}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {101--115},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.101},
URN = {urn:nbn:de:0030-drops-41925},
doi = {10.4230/LIPIcs.CSL.2013.101},
annote = {Keywords: Lambda-Calculus, B\"{o}hm trees, Differential Lambda-Calculus, Linear Logic}
}
Document
Team building in dependence
Abstract
Hintikka and Sandu's Independence-Friendly Logic was introduced as a logic for partially ordered quantification, in which the independence of (existential) quantifiers from previous (universal) quantifiers is written by explicit syntax. It was originally given a semantics by games of imperfect information; Hodges then gave a (necessarily) second-order Tarskian semantics. More recently, Väänänen (2007) has proposed that the many curious features of IF logic can be better understood in his Dependence Logic, in which the (in)dependence of variables is stated in atomic formula, rather than by changing the definition of quantifier; he gives semantics in Tarskian form, via imperfect information games, and via a routine second-order perfect information game. He then defines Team Logic, where classical negation is added to the mix, resulting in a full second-order expressive logic. He remarks that no game semantics appears possible (other than by playing at second order). In this article, we explore an alternative approach to game semantics for DL, where we avoid imperfect information, yet stay locally apparently first-order, by sweeping the second-order information into longer games (infinite games in the case of countable models). Extending the game to Team Logic is not possible in standard games, but we conjecture a move to transfinite games may achieve a 'natural' game for Team Logic.
Cite as
Julian Bradfield. Team building in dependence. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 116-128, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{bradfield:LIPIcs.CSL.2013.116,
author = {Bradfield, Julian},
title = {{Team building in dependence}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {116--128},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.116},
URN = {urn:nbn:de:0030-drops-41935},
doi = {10.4230/LIPIcs.CSL.2013.116},
annote = {Keywords: partially ordered quantification, independence-friendly logic, game semantics}
}
Document
Saturation-Based Model Checking of Higher-Order Recursion Schemes
Abstract
Model checking of higher-order recursion schemes (HORS) has recently been studied extensively and applied to higher-order program verification. Despite recent efforts, obtaining a scalable model checker for HORS remains a big challenge. We propose a new model checking algorithm for HORS, which combines two previous, independent approaches to higher-order model checking. Like previous type-based algorithms for HORS, it directly analyzes HORS and outputs intersection types as a certificate, but like Broadbent et al.'s saturation algorithm for collapsible pushdown systems (CPDS), it propagates information backward, in the sense that it starts with target configurations and iteratively computes their pre-images. We have implemented the new algorithm and confirmed that the prototype often outperforms TRECS and CSHORe, the state-of-the-art model checkers for HORS.
Cite as
Christopher Broadbent and Naoki Kobayashi. Saturation-Based Model Checking of Higher-Order Recursion Schemes. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 129-148, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{broadbent_et_al:LIPIcs.CSL.2013.129,
author = {Broadbent, Christopher and Kobayashi, Naoki},
title = {{Saturation-Based Model Checking of Higher-Order Recursion Schemes}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {129--148},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.129},
URN = {urn:nbn:de:0030-drops-41941},
doi = {10.4230/LIPIcs.CSL.2013.129},
annote = {Keywords: Model checking, higher-order recursion schemes, intersection types}
}
Document
Descriptive complexity of approximate counting CSPs
Abstract
Motivated by Fagin's characterization of NP, Saluja et al. have introduced a logic based frame- work for expressing counting problems. In this setting, a counting problem (seen as a mapping C from structures to non-negative integers) is `defined’ by a first-order sentence phi if for every instance A of the problem, the number of possible satisfying assignments of the variables of phi in A is equal to C(A). The logic RHPI_1 has been introduced by Dyer et al. in their study of the counting complexity class #BIS. The interest in the class #BIS stems from the fact that, it is quite plausible that the problems in #BIS are not #P-hard, nor they admit a fully polynomial randomized approximation scheme. In the present paper we investigate which counting constraint satisfaction problems #CSP(H) are definable in the monotone fragment of RHPI_1. We prove that #CSP(H) is definable in monotone RHPI_1 whenever H is invariant under meet and join operations of a distributive lattice. We prove that the converse also holds if H contains the equality relation. We also prove similar results for counting CSPs expressible by linear Datalog. The results in this case are very similar to those for monotone RHPI1, with the addition that H has, additionally, \top (the greatest element of the lattice) as a polymorphism.
Cite as
Andrei Bulatov, Victor Dalmau, and Marc Thurley. Descriptive complexity of approximate counting CSPs. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 149-164, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{bulatov_et_al:LIPIcs.CSL.2013.149,
author = {Bulatov, Andrei and Dalmau, Victor and Thurley, Marc},
title = {{Descriptive complexity of approximate counting CSPs}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {149--164},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.149},
URN = {urn:nbn:de:0030-drops-41955},
doi = {10.4230/LIPIcs.CSL.2013.149},
annote = {Keywords: Constraint Satisfaction Problems, Approximate Counting, Descriptive Complexity}
}
Document
What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives
Abstract
We consider partially observable Markov decision processes (POMDPs) with omega-regular conditions specified as parity objectives. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are known to be undecidable even for very special cases of parity objectives, we establish decidability (with optimal EXPTIME-complete complexity) of the qualitative analysis problems for POMDPs with all parity objectives under finite-memory strategies. We also establish optimal (exponential) memory bounds.
Cite as
Krishnendu Chatterjee, Martin Chmelik, and Mathieu Tracol. What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 165-180, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{chatterjee_et_al:LIPIcs.CSL.2013.165,
author = {Chatterjee, Krishnendu and Chmelik, Martin and Tracol, Mathieu},
title = {{What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {165--180},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.165},
URN = {urn:nbn:de:0030-drops-41962},
doi = {10.4230/LIPIcs.CSL.2013.165},
annote = {Keywords: POMDPs, Omega-regular objectives, Parity objectives, Qualitative analysis}
}
Document
Infinite-state games with finitary conditions
Abstract
We study two-player zero-sum games over infinite-state graphs equipped with omega-B and finitary conditions.
Our first contribution is about the strategy complexity, i.e the memory required for winning strategies: we prove that over general infinite-state graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory suffices for finitary parity games.
We then study pushdown games with boundedness conditions, with two contributions. First we prove a collapse result for pushdown games with omega-B-conditions, implying the decidability of solving these games. Second we consider pushdown games with finitary parity along with stack boundedness conditions, and show that solving these games is EXPTIME-complete.
Cite as
Krishnendu Chatterjee and Nathanaël Fijalkow. Infinite-state games with finitary conditions. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 181-196, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{chatterjee_et_al:LIPIcs.CSL.2013.181,
author = {Chatterjee, Krishnendu and Fijalkow, Nathana\"{e}l},
title = {{Infinite-state games with finitary conditions}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {181--196},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.181},
URN = {urn:nbn:de:0030-drops-41970},
doi = {10.4230/LIPIcs.CSL.2013.181},
annote = {Keywords: Two-player games, Infinite-state systems, Pushdown games, Bounds in omega-regularity, Synthesis}
}
Document
Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic
Abstract
Full Intuitionistic Linear Logic (FILL) is multiplicative intuitionistic linear logic extended with par. Its proof theory has been notoriously difficult to get right, and existing sequent calculi all involve inference rules with complex annotations to guarantee soundness and cut-elimination. We give a simple and annotation-free display calculus for FILL which satisfies Belnap’s generic cut-elimination theorem. To do so, our display calculus actually handles an extension of FILL, called Bi-Intuitionistic Linear Logic (BiILL), with an ‘exclusion’ connective defined via an adjunction with par. We refine our display calculus for BiILL into a cut-free nested sequent calculus with deep inference in which the explicit structural rules of the display calculus become admissible. A separation property guarantees that proofs of FILL formulae in the deep inference calculus contain no trace of exclusion. Each such rule is sound for the semantics of FILL, thus our deep inference calculus and display calculus are conservative over FILL. The deep inference calculus also enjoys the subformula property and terminating backward proof search, which gives the NP-completeness of BiILL and FILL.
Cite as
Ranald Clouston, Jeremy Dawson, Rajeev Goré, and Alwen Tiu. Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 197-214, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{clouston_et_al:LIPIcs.CSL.2013.197,
author = {Clouston, Ranald and Dawson, Jeremy and Gor\'{e}, Rajeev and Tiu, Alwen},
title = {{Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {197--214},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.197},
URN = {urn:nbn:de:0030-drops-41981},
doi = {10.4230/LIPIcs.CSL.2013.197},
annote = {Keywords: Linear logic, display calculus, nested sequent calculus, deep inference}
}
Document
Deciding the weak definability of Büchi definable tree languages
Abstract
Weakly definable languages of infinite trees are an expressive subclass of regular tree languages definable in terms of weak monadic second-order logic, or equivalently weak alternating automata. Our main result is that given a Büchi automaton, it is decidable whether the language is weakly definable. We also show that given a parity automaton, it is decidable whether the language is recognizable by a nondeterministic co-Büchi automaton.
The decidability proofs build on recent results about cost automata over infinite trees. These automata use counters to define functions from infinite trees to the natural numbers extended with infinity. We reduce to testing whether the functions defined by certain "quasi-weak" cost automata are bounded by a finite value.
Cite as
Thomas Colcombet, Denis Kuperberg, Christof Löding, and Michael Vanden Boom. Deciding the weak definability of Büchi definable tree languages. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 215-230, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{colcombet_et_al:LIPIcs.CSL.2013.215,
author = {Colcombet, Thomas and Kuperberg, Denis and L\"{o}ding, Christof and Vanden Boom, Michael},
title = {{Deciding the weak definability of B\"{u}chi definable tree languages}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {215--230},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.215},
URN = {urn:nbn:de:0030-drops-41998},
doi = {10.4230/LIPIcs.CSL.2013.215},
annote = {Keywords: Tree automata, weak definability, decidability, cost automata, boundedness}
}
Document
Innocent Game Semantics via Intersection Type Assignment Systems
Abstract
The aim of this work is to correlate two different approaches to the semantics of programming languages: game semantics and intersection type assignment systems (ITAS). Namely, we present an ITAS that provides the description of the semantic interpretation of a typed lambda calculus in a game model based on innocent strategies. Compared to the traditional ITAS used to describe the semantic interpretation in domain theoretic models, the ITAS presented in this paper has two main differences: the introduction of a notion of labelling on moves, and the omission of several rules, i.e. the subtyping rules and some structural rules.
Cite as
Pietro Di Gianantonio and Marina Lenisa. Innocent Game Semantics via Intersection Type Assignment Systems. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 231-247, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{digianantonio_et_al:LIPIcs.CSL.2013.231,
author = {Di Gianantonio, Pietro and Lenisa, Marina},
title = {{Innocent Game Semantics via Intersection Type Assignment Systems}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {231--247},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.231},
URN = {urn:nbn:de:0030-drops-42005},
doi = {10.4230/LIPIcs.CSL.2013.231},
annote = {Keywords: Game Semantics, Intersection Type Assignment System, Lambda Calculus}
}
Document
Cuts for circular proofs: semantics and cut-elimination
Abstract
One of the authors introduced in [Santocanale, FoSSaCS, 2002] a calculus of circular proofs for studying the computability arising from the following categorical operations: finite products, finite coproducts, initial algebras, final coalgebras. The calculus presented [Santocanale, FoSSaCS, 2002] is cut-free; even if sound and complete for provability, it lacked an important property for the semantics of proofs, namely fullness w.r.t. the class of intended categorical models (called mu-bicomplete categories in [Santocanale, ITA, 2002]).
In this paper we fix this problem by adding the cut rule to the calculus and by modifying accordingly the syntactical constraint ensuring soundness of proofs. The enhanced proof system fully represents arrows of the canonical model (a free mu-bicomplete category). We also describe a cut-elimination procedure as a a model of computation arising from the above mentioned categorical operations. The procedure constructs a cut-free proof-tree with possibly infinite branches out of a finite circular proof with cuts.
Cite as
Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 248-262, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{fortier_et_al:LIPIcs.CSL.2013.248,
author = {Fortier, J\'{e}r\^{o}me and Santocanale, Luigi},
title = {{Cuts for circular proofs: semantics and cut-elimination}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {248--262},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.248},
URN = {urn:nbn:de:0030-drops-42019},
doi = {10.4230/LIPIcs.CSL.2013.248},
annote = {Keywords: categorical proof-theory, fixpoints, initial and final (co)algebras, inductive and coinductive types}
}
Document
Hierarchies in independence logic
Abstract
We study the expressive power of fragments of inclusion and independence logic defined either by restricting the number of universal quantifiers or the arity of inclusion and independence atoms in formulas. Assuming the so-called lax semantics for these logics, we relate these fragments of inclusion and independence logic to familiar sublogics of existential second-order logic. We also show that, with respect to the stronger strict semantics, inclusion logic is equivalent to existential second-order logic.
Cite as
Pietro Galliani, Miika Hannula, and Juha Kontinen. Hierarchies in independence logic. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 263-280, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{galliani_et_al:LIPIcs.CSL.2013.263,
author = {Galliani, Pietro and Hannula, Miika and Kontinen, Juha},
title = {{Hierarchies in independence logic}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {263--280},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.263},
URN = {urn:nbn:de:0030-drops-42021},
doi = {10.4230/LIPIcs.CSL.2013.263},
annote = {Keywords: Existential second-order logic, Independence logic, Inclusion logic, Expressiveness hierarchies}
}
Document
Inclusion Logic and Fixed Point Logic
Abstract
We investigate the properties of Inclusion Logic, that is, First Order Logic with Team Semantics extended with inclusion dependencies. We prove that Inclusion Logic is equivalent to Greatest Fixed Point Logic, and we prove that all union-closed first-order definable properties of relations are definable in it. We also provide an Ehrenfeucht-Fraïssé game for Inclusion Logic, and give an example illustrating its use.
Cite as
Pietro Galliani and Lauri Hella. Inclusion Logic and Fixed Point Logic. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 281-295, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{galliani_et_al:LIPIcs.CSL.2013.281,
author = {Galliani, Pietro and Hella, Lauri},
title = {{Inclusion Logic and Fixed Point Logic}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {281--295},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.281},
URN = {urn:nbn:de:0030-drops-42031},
doi = {10.4230/LIPIcs.CSL.2013.281},
annote = {Keywords: Dependence Logic, Team Semantics, Fixpoint Logic, Inclusion}
}
Document
Theories for Subexponential-size Bounded-depth Frege Proofs
Abstract
This paper is a contribution to our understanding of the relationship between uniform and nonuniform proof complexity. The latter studies the lengths of proofs in various propositional proof systems such as Frege and bounded-depth Frege systems, and the former studies the strength of the corresponding logical theories such as VNC1 and V0 in [Cook/Nguyen, 2010]. A superpolynomial lower bound on the length of proofs in a propositional proof system for a family of tautologies expressing a result like the pigeonhole principle implies that the result is not provable in the theory associated with the propositional proof system.
We define a new class of bounded arithmetic theories n^epsilon-ioV^\infinity for epsilon < 1 and show that they correspond to complexity classes AltTime(O(1),O(n^epsilon)), uniform classes of subexponential-size bounded-depth circuits DepthSize(O(1),2^O(n^epsilon)). To accomplish this we introduce the novel idea of using types to control the amount of composition in our bounded arithmetic theories. This allows our theories to capture complexity classes that have weaker closure properties and are not closed under composition. We show that the proofs of Sigma^B_0-theorems in our theories translate to subexponential-size bounded-depth Frege proofs.
We use these theories to formalize the complexity theory result that problems in uniform NC1 circuits can be computed by uniform subexponential bounded-depth circuits in [Allender/Koucky, 2010]. We prove that our theories contain a variation of the theory VNC1 for the complexity class NC1. We formalize Buss's proof in [Buss, 1993] that the (unbalanced) Boolean Formula Evaluation problem is in NC1 and use it to prove the soundness of Frege systems. As a corollary, we obtain an alternative proof of [Filmus et al, ICALP, 2011] that polynomial-size Frege proofs can be simulated by subexponential-size bounded-depth Frege proofs.
Our results can be extended to theories corresponding to other nice complexity classes inside NTimeSpace(n^O(1), n^o(1)) such as NL. This is achieved by essentially formalizing the containment
NTimeSpace(n^O(1), n^o(1)) \subseteq AltTime(O(1), O(n^epsilon))
for all epsilon > 0.
Cite as
Kaveh Ghasemloo and Stephen A. Cook. Theories for Subexponential-size Bounded-depth Frege Proofs. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 296-315, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{ghasemloo_et_al:LIPIcs.CSL.2013.296,
author = {Ghasemloo, Kaveh and Cook, Stephen A.},
title = {{Theories for Subexponential-size Bounded-depth Frege Proofs}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {296--315},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.296},
URN = {urn:nbn:de:0030-drops-42044},
doi = {10.4230/LIPIcs.CSL.2013.296},
annote = {Keywords: Computational Complexity Theory, Proof Complexity, Bounded Arithmetic, NC1-Frege, AC0- Frege}
}
Document
The Structure of Interaction
Abstract
Interaction nets form a local and strongly confluent model of computation that is per se parallel. We introduce a Curry–Howard correspondence between well-formed interaction nets and a deep-inference deduction system based on linear logic. In particular, linear logic itself is easily expressed in the system and its computational aspects materialise though the correspondence. The system of interaction nets obtained is a typed variant of already well-known sharing graphs. Due to a strong confluence property, strong normalisation for this system follows from weak normalisation. The latter is obtained via an adaptation of Girard's reducibility method. The approach is modular, readily gives rise to generalisations (e.g. second order, known as polymorphism to the programmer) and could therefore be extended to various systems of interaction nets.
Cite as
Stéphane Gimenez and Georg Moser. The Structure of Interaction. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 316-331, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{gimenez_et_al:LIPIcs.CSL.2013.316,
author = {Gimenez, St\'{e}phane and Moser, Georg},
title = {{The Structure of Interaction}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {316--331},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.316},
URN = {urn:nbn:de:0030-drops-42052},
doi = {10.4230/LIPIcs.CSL.2013.316},
annote = {Keywords: Interaction Nets, Linear Logic, Curry–Howard Correspondence, Deep Inference, Calculus of Structures, Strong Normalisation, Reducibility}
}
Document
The Fixed-Parameter Tractability of Model Checking Concurrent Systems
Abstract
We study the fixed-parameter complexity of model checking temporal logics on concurrent systems that are modeled as the product of finite systems and where the size of the formula is the parameter. We distinguish between asynchronous product and synchronous product. Sometimes it is possible to show that there is an algorithm for this with running time (\sum_i T_i|)O(1) * f(|\phi|), where the T_i are the component systems and \phi is the formula and f is computable function, thus model checking is fixed-parameter tractable when the size of the formula is the parameter.
In this paper we concern ourselves with the question, provided fixed-parameter tractability is known, whether it holds for an elementary function f. Negative answers to this question are provided for modal logic and EF logic: Depending on the mode of synchronization we show the non-existence of such an elementary function f under different assumptions from (parameterized) complexity theory.
Cite as
Stefan Göller. The Fixed-Parameter Tractability of Model Checking Concurrent Systems. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 332-347, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{goller:LIPIcs.CSL.2013.332,
author = {G\"{o}ller, Stefan},
title = {{The Fixed-Parameter Tractability of Model Checking Concurrent Systems}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {332--347},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.332},
URN = {urn:nbn:de:0030-drops-42062},
doi = {10.4230/LIPIcs.CSL.2013.332},
annote = {Keywords: Model Checking, Concurrent Systems, Parameterized Complexity}
}
Document
One-variable first-order linear temporal logics with counting
Abstract
First-order temporal logics are notorious for their bad computational behaviour. It is known that even the two-variable monadic fragment is highly undecidable over various timelines. However, following the introduction of the monodic formulas (where temporal operators can be applied only to subformulas with at most one free variable), there has been a renewed interest in understanding extensions of the one-variable fragment and identifying those that are decidable. Here we analyse the one-variable fragment of temporal logic extended with counting (to two), interpreted in models with constant, decreasing, and expanding first-order domains. We show that over most classes of linear orders these logics are (sometimes highly) undecidable, even without constant and function symbols, and with the sole temporal operator 'eventually'. A more general result says that the bimodal logic of commuting linear and pseudo-equivalence relations is undecidable. The proofs are by reductions of various counter machine problems.
Cite as
Christopher Hampson and Agi Kurucz. One-variable first-order linear temporal logics with counting. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 348-362, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{hampson_et_al:LIPIcs.CSL.2013.348,
author = {Hampson, Christopher and Kurucz, Agi},
title = {{One-variable first-order linear temporal logics with counting}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {348--362},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.348},
URN = {urn:nbn:de:0030-drops-42072},
doi = {10.4230/LIPIcs.CSL.2013.348},
annote = {Keywords: modal and temporal logic, counting, decision procedures}
}
Document
On the locality of arb-invariant first-order logic with modulo counting quantifiers
Abstract
We study Gaifman and Hanf locality of an extension of first-order logic with modulo p counting quantifiers (FO+MODp, for short) with arbitrary numerical predicates. We require that the validity of formulas is independent of the particular interpretation of the numerical predicates and refer to such formulas as arb-invariant formulas. This paper gives a detailed picture of locality and non-locality properties of arb-invariant FO+MODp. For example, on the class of all finite structures, for any p >= 2, arb-invariant FO+MODp is neither Hanf nor Gaifman local with respect to a sublinear locality radius. However, in case that p is an odd prime power, it is weakly Gaifman local with a polylogarithmic locality radius. And when restricting attention to the class of string structures, for odd prime powers p, arb-invariant FO+MODp is both Hanf and Gaifman local with a polylogarithmic locality radius. Our negative results build on examples of order-invariant FO+MODp formulas presented in Niemistö's PhD thesis. Our positive results make use of the close connection between FO+MODp and Boolean circuits built from NOT-gates and AND-, OR-, and MODp-gates of arbitrary fan-in.
Cite as
Frederik Harwath and Nicole Schweikardt. On the locality of arb-invariant first-order logic with modulo counting quantifiers. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 363-379, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{harwath_et_al:LIPIcs.CSL.2013.363,
author = {Harwath, Frederik and Schweikardt, Nicole},
title = {{On the locality of arb-invariant first-order logic with modulo counting quantifiers}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {363--379},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.363},
URN = {urn:nbn:de:0030-drops-42086},
doi = {10.4230/LIPIcs.CSL.2013.363},
annote = {Keywords: finite model theory, Gaifman and Hanf locality, first-order logic with modulo counting quantifiers, order-invariant and arb-invariant formulas, lower}
}
Document
When is Metric Temporal Logic Expressively Complete?
Abstract
A seminal result of Kamp is that over the reals Linear Temporal Logic (LTL) has the same expressive power as first-order logic with binary order relation < and monadic predicates. A key question is whether there exists an analogue of Kamp's theorem for Metric Temporal Logic (MTL) - a generalization of LTL in which the Until and Since modalities are annotated with intervals that express metric constraints. Hirshfeld and Rabinovich gave a negative answer, showing that first-order logic with binary order relation < and unary function +1 is strictly more expressive than MTL with integer constants. However, a recent result of Hunter, Ouaknine and Worrell shows that when rational timing constants are added to both languages, MTL has the same expressive power as first-order logic, giving a positive answer. In this paper we generalize these results by giving a precise characterization of those sets of constants for which MTL and first-order logic have the same expressive power. We also show that full first-order expressiveness can be recovered with the addition of counting modalities, strongly supporting the assertion of Hirshfeld and Rabinovich that Q2MLO is one of the most expressive decidable fragments of FO(<,+1).
Cite as
Paul Hunter. When is Metric Temporal Logic Expressively Complete?. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 380-394, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{hunter:LIPIcs.CSL.2013.380,
author = {Hunter, Paul},
title = {{When is Metric Temporal Logic Expressively Complete?}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {380--394},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.380},
URN = {urn:nbn:de:0030-drops-42092},
doi = {10.4230/LIPIcs.CSL.2013.380},
annote = {Keywords: Metric Temporal Logic, Expressive power, First-order logic}
}
Document
Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus
Abstract
In this paper we present strong normalisation proofs using a technique of non-deterministic translations into Klop's extended lambda-calculus. We first illustrate the technique by showing strong normalisation of a typed calculus that corresponds to natural deduction with general elimination rules. Then we study its explicit substitution version, the type-free calculus of which does not satisfy PSN with respect to reduction of the original calculus; nevertheless it is shown that typed terms are strongly normalising with respect to reduction of the explicit substitution calculus. In the same framework we prove strong normalisation of Sørensen and Urzyczyn's cut-elimination system in intuitionistic sequent calculus.
Cite as
Kentaro Kikuchi. Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 395-414, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{kikuchi:LIPIcs.CSL.2013.395,
author = {Kikuchi, Kentaro},
title = {{Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {395--414},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.395},
URN = {urn:nbn:de:0030-drops-42108},
doi = {10.4230/LIPIcs.CSL.2013.395},
annote = {Keywords: Strong normalisation, Klop's extended lambda-calculus, Explicit substitution, Cut-elimination}
}
Document
Kleene Algebra with Products and Iteration Theories
Abstract
We develop a typed equational system that subsumes both iteration theories and typed Kleene algebra in a common framework. Our approach is based on cartesian categories endowed with commutative strong monads to handle nondeterminism.
Cite as
Dexter Kozen and Konstantinos Mamouras. Kleene Algebra with Products and Iteration Theories. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 415-431, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{kozen_et_al:LIPIcs.CSL.2013.415,
author = {Kozen, Dexter and Mamouras, Konstantinos},
title = {{Kleene Algebra with Products and Iteration Theories}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {415--431},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.415},
URN = {urn:nbn:de:0030-drops-42111},
doi = {10.4230/LIPIcs.CSL.2013.415},
annote = {Keywords: Kleene algebra, typed Kleene algebra, iteration theories}
}
Document
Internalizing Relational Parametricity in the Extensional Calculus of Constructions
Abstract
We give the first relationally parametric model of the extensional calculus of constructions. Our model remains as simple as traditional PER models of types, but unlike them, it additionally permits the relating of terms that implement abstract types in different ways. Using our model, we can validate the soundness of quotient types, as well as derive strong equality axioms for Church-encoded data, such as the usual induction principles for Church naturals and booleans, and the eta law for strong dependent pair types. Furthermore, we show that such equivalences, justified by relationally parametric reasoning, may soundly be internalized (i.e., added as equality axioms to our type theory). Thus, we demonstrate that it is possible to interpret equality in a dependently-typed setting using parametricity. The key idea behind our approach is to interpret types as so-called quasi-PERs (or zigzag-complete relations), which enable us to model the symmetry and transitivity of equality while at the same time allowing abstract types with different representations to be equated.
Cite as
Neelakantan R. Krishnaswami and Derek Dreyer. Internalizing Relational Parametricity in the Extensional Calculus of Constructions. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 432-451, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{krishnaswami_et_al:LIPIcs.CSL.2013.432,
author = {Krishnaswami, Neelakantan R. and Dreyer, Derek},
title = {{Internalizing Relational Parametricity in the Extensional Calculus of Constructions}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {432--451},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.432},
URN = {urn:nbn:de:0030-drops-42125},
doi = {10.4230/LIPIcs.CSL.2013.432},
annote = {Keywords: Relational parametricity, dependent types, quasi-PERs}
}
Document
Modal Logic and Distributed Message Passing Automata
Abstract
In a recent article, Lauri Hella and co-authors identify a canonical connection between modal logic and deterministic distributed constant-time algorithms. The paper reports a variety of highly natural logical characterizations of classes of distributed message passing automata that run in constant time. The article leaves open the question of identifying related logical characterizations when the constant running time limitation is lifted. We obtain such a characterization for a class of finite message passing automata in terms of a recursive bisimulation invariant logic which we call modal substitution calculus (MSC). We also give a logical characterization of the related class A of infinite message passing automata by showing that classes of labelled directed graphs recognizable by automata in A are exactly the classes co-definable by a modal theory. A class C is co-definable by a modal theory if the complement of C is definable by a possibly infinite set of modal formulae. We also briefly discuss expressivity and decidability issues concerning MSC. We establish that MSC contains the Sigma^\mu_1 fragment of the modal \mu-calculus in the finite. We also observe that the single variable fragment MSC^1 of MSC is not contained in MSO, and that the SAT and FINSAT problems of MSC^1 are complete for PSPACE.
Cite as
Antti Kuusisto. Modal Logic and Distributed Message Passing Automata. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 452-468, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{kuusisto:LIPIcs.CSL.2013.452,
author = {Kuusisto, Antti},
title = {{Modal Logic and Distributed Message Passing Automata}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {452--468},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.452},
URN = {urn:nbn:de:0030-drops-42132},
doi = {10.4230/LIPIcs.CSL.2013.452},
annote = {Keywords: Modal logic, message passing automata, descriptive characterizations, distributed computing}
}
Document
Global semantic typing for inductive and coinductive computing
Abstract
Common data-types, such as N, can be identified with term algebras. Thus each type can be construed as a global set; e.g. for N this global set is instantiated in each structure S to the denotations in S of the unary numerals. We can then consider each declarative program as an axiomatic theory, and assigns to it a semantic (Curry-style) type in each structure. This leads to the intrinsic theories of [Leivant, 2002], which provide a purely logical framework for reasoning about programs and their types. The framework is of interest because of its close fit with syntactic, semantic, and proof theoretic fundamentals of formal logic.
This paper extends the framework to data given by coinductive as well as inductive declarations. We prove a Canonicity Theorem, stating that the denotational semantics of an equational program P, understood operationally, has type \tau over the canonical model iff P, understood as a formula has type \tau in every "data-correct" structure. In addition we show that every intrinsic theory is interpretable in a conservative extension of first-order arithmetic.
Cite as
Daniel Leivant. Global semantic typing for inductive and coinductive computing. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 469-483, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{leivant:LIPIcs.CSL.2013.469,
author = {Leivant, Daniel},
title = {{Global semantic typing for inductive and coinductive computing}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {469--483},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.469},
URN = {urn:nbn:de:0030-drops-42142},
doi = {10.4230/LIPIcs.CSL.2013.469},
annote = {Keywords: Inductive and coinductive types, equational programs, intrinsic theories, global model theory}
}
Document
Two-Variable Logic on 2-Dimensional Structures
Abstract
This paper continues the study of the two-variable fragment of first-order logic (FO^2) over two- dimensional structures, more precisely structures with two orders, their induced successor relations and arbitrarily many unary relations. Our main focus is on ordered data words which are finite sequences from the set \Sigma x D where \Sigma is a finite alphabet and D is an ordered domain. These are naturally represented as labelled finite sets with a linear order <=_l and a total preorder <=_p.
We introduce ordered data automata, an automaton model for ordered data words. An ordered data automaton is a composition of a finite state transducer and a finite state automaton over the product Boolean algebra of finite and cofinite subsets of N. We show that ordered data automata are equivalent to the closure of FO^2(+1_l,<=_p,+1_p) under existential quantification of unary relations. Using this automaton model we prove that the finite satisfiability problem for this logic is decidable on structures where the <=_p-equivalence classes are of bounded size. As a corollary, we obtain that finite satisfiability of FO^2 is decidable (and it is equivalent to the reachability problem of vector addition systems) on structures with two linear order successors and a linear order corresponding to one of the successors. Further we prove undecidability of FO^2 on several other two-dimensional structures.
Cite as
Amaldev Manuel and Thomas Zeume. Two-Variable Logic on 2-Dimensional Structures. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 484-499, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{manuel_et_al:LIPIcs.CSL.2013.484,
author = {Manuel, Amaldev and Zeume, Thomas},
title = {{Two-Variable Logic on 2-Dimensional Structures}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {484--499},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.484},
URN = {urn:nbn:de:0030-drops-42159},
doi = {10.4230/LIPIcs.CSL.2013.484},
annote = {Keywords: FO2, Data words, Satisfiability, Decidability, Automata}
}
Document
Categorical Duality Theory: With Applications to Domains, Convexity, and the Distribution Monad
Abstract
Utilising and expanding concepts from categorical topology and algebra, we contrive a moderately general theory of dualities between algebraic, point-free spaces and set-theoretical, point-set spaces, which encompasses infinitary Stone dualities, such as the well-known duality between frames (aka. locales) and topological spaces, and a duality between \sigma-complete Boolean algebras and measurable spaces, as well as the classic finitary Stone, Gelfand, and Pontryagin dualities. Among different applications of our theory, we focus upon domain-convexity duality in particular: from the theory we derive a duality between Scott's continuous lattices and convexity spaces, and exploit the resulting insights to identify intrinsically the dual equivalence part of a dual adjunction for algebras of the distribution monad; the dual adjunction was uncovered by Bart Jacobs, but with no characterisation of the induced equivalence, which we do give here. In the Appendix, we place categorical duality in a wider context, and elucidate philosophical underpinnings of duality.
Cite as
Yoshihiro Maruyama. Categorical Duality Theory: With Applications to Domains, Convexity, and the Distribution Monad. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 500-520, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{maruyama:LIPIcs.CSL.2013.500,
author = {Maruyama, Yoshihiro},
title = {{Categorical Duality Theory: With Applications to Domains, Convexity, and the Distribution Monad}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {500--520},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.500},
URN = {urn:nbn:de:0030-drops-42168},
doi = {10.4230/LIPIcs.CSL.2013.500},
annote = {Keywords: duality, monad, categorical topology, domain theory, convex structure}
}
Document
Axiomatizing Subtyped Delimited Continuations
Abstract
We present direct equational axiomatizations of the call-by-value lambda calculus with the control operators shift_0 and reset_0 that generalize Danvy and Filinski's shift and reset in that they allow for abstracting control beyond the top-most delimited continuation. We address an untyped version of the calculus as well as a typed version with effect subtyping. For each of the calculi we present a set of axioms that we prove sound and complete with respect to the corresponding CPS translation.
Cite as
Marek Materzok. Axiomatizing Subtyped Delimited Continuations. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 521-539, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{materzok:LIPIcs.CSL.2013.521,
author = {Materzok, Marek},
title = {{Axiomatizing Subtyped Delimited Continuations}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {521--539},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.521},
URN = {urn:nbn:de:0030-drops-42178},
doi = {10.4230/LIPIcs.CSL.2013.521},
annote = {Keywords: Delimited Continuations, Continuation Passing Style, Axiomatization}
}
Document
On dialogue games and coherent strategies
Abstract
We explain how to see the set of positions of a dialogue game as a coherence space in the sense of Girard or as a bistructure in the sense of Curien, Plotkin and Winskel. The coherence structure on the set of positions results from a Kripke translation of tensorial logic into linear logic extended with a necessity modality. The translation is done in such a way that every innocent strategy defines a clique or a configuration in the resulting space of positions. This leads us to study the notion of configuration designed by Curien, Plotkin and Winskel for general bistructures in the particular case of a bistructure associated to a dialogue game. We show that every such configuration may be seen as an interactive strategy equipped with a backward as well as a forward dynamics based on the interplay between the stable order and the extensional order. In that way, the category of bistructures is shown to include a full subcategory of games and coherent strategies of an interesting nature.
Cite as
Paul-André Melliès. On dialogue games and coherent strategies. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 540-562, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{mellies:LIPIcs.CSL.2013.540,
author = {Melli\`{e}s, Paul-Andr\'{e}},
title = {{On dialogue games and coherent strategies}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {540--562},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.540},
URN = {urn:nbn:de:0030-drops-42181},
doi = {10.4230/LIPIcs.CSL.2013.540},
annote = {Keywords: Game semantics, Stable order, Extensional order, Bistructures, Tensorial logic, Innocent strategies}
}
Document
Elementary Modal Logics over Transitive Structures
Abstract
We show that modal logic over universally first-order definable classes of transitive frames is decidable. More precisely, let K be an arbitrary class of transitive Kripke frames definable by a universal first-order sentence. We show that the global and finite global satisfiability problems of modal logic over K are decidable in NP, regardless of choice of K. We also show that the local satisfiability and the finite local satisfiability problems of modal logic over K are decidable in NExpTime.
Cite as
Jakub Michaliszyn and Jan Otop. Elementary Modal Logics over Transitive Structures. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 563-577, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{michaliszyn_et_al:LIPIcs.CSL.2013.563,
author = {Michaliszyn, Jakub and Otop, Jan},
title = {{Elementary Modal Logics over Transitive Structures}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {563--577},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.563},
URN = {urn:nbn:de:0030-drops-42195},
doi = {10.4230/LIPIcs.CSL.2013.563},
annote = {Keywords: Modal logic, Transitive frames, Elementary modal logics, Decidability}
}
Document
A Fully Abstract Game Semantics for Parallelism with Non-Blocking Synchronization on Shared Variables
Abstract
We present a fully abstract game semantics for an Algol-like parallel language with non-blocking synchronization primitive. Elaborating on Harmer's game model for nondeterminism, we develop a game framework appropriate for modeling parallelism. The game is a sophistication of the wait-notify game proposed in a previous work, which makes the signals for thread scheduling explicit with a certain set of extra moves. The extra moves induce a Kleisli category of games, on which we develop a game semantics of the Algol-like parallel language and establish the full abstraction result with a significant use of the non-blocking synchronization operation.
Cite as
Susumu Nishimura. A Fully Abstract Game Semantics for Parallelism with Non-Blocking Synchronization on Shared Variables. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 578-596, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{nishimura:LIPIcs.CSL.2013.578,
author = {Nishimura, Susumu},
title = {{A Fully Abstract Game Semantics for Parallelism with Non-Blocking Synchronization on Shared Variables}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {578--596},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.578},
URN = {urn:nbn:de:0030-drops-42201},
doi = {10.4230/LIPIcs.CSL.2013.578},
annote = {Keywords: shared variable parallelism, non-blocking synchronization, full abstraction, game semantics}
}
Document
Extracting Herbrand trees in classical realizability using forcing
Abstract
Krivine presented in [Krivine, 2011] a methodology to combine Cohen's forcing with the theory of classical realizability and showed that the forcing condition can be seen as a reference that is not subject to backtracks. The underlying classical program transformation was then analyzed by Miquel [Miquel, 2011] in a fully typed setting in classical higher-order arithmetic (PA-omega^+).
As a case study of this methodology, we present a method to extract a Herbrand tree from a classical realizer of inconsistency, following the ideas underlying the completeness theorem and the proof of Herbrand's theorem. Unlike the traditional proof based on König's lemma (using a fixed enumeration of atomic formulas), our method is based on the introduction of a particular Cohen real. It is formalized as a proof in PA-omega^+, making explicit the construction of generic sets in this framework in the particular case where the set of forcing conditions is arithmetical. We then analyze the algorithmic content of this proof.
Cite as
Lionel Rieg. Extracting Herbrand trees in classical realizability using forcing. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 597-614, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{rieg:LIPIcs.CSL.2013.597,
author = {Rieg, Lionel},
title = {{Extracting Herbrand trees in classical realizability using forcing}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {597--614},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.597},
URN = {urn:nbn:de:0030-drops-42212},
doi = {10.4230/LIPIcs.CSL.2013.597},
annote = {Keywords: classical realizability, forcing, Curry-Howard correspondence, Herbrand trees}
}
Document
The Complexity of Abduction for Equality Constraint Languages
Abstract
Abduction is a form of nonmonotonic reasoning that looks for an explanation for an observed manifestation according to some knowledge base. One form of the abduction problem studied in the literature is the propositional abduction problem parameterized by a structure \Gamma over the two-element domain. In that case, the knowledge base is a set of constraints over \Gamma, the manifestation and explanation are propositional formulas.
In this paper, we follow a similar route. Yet, we consider abduction over infinite domain. We study the equality abduction problem parameterized by a relational first-order structure \Gamma over the natural numbers such that every relation in \Gamma is definable by a Boolean combination of equalities, a manifestation is a literal of the form (x = y) or (x != y), and an explanation is a set of such literals. Our main contribution is a complete complexity characterization of the equality abduction problem. We prove that depending on \Gamma, it is \Sigma^P_2-complete, or NP-complete, or in P.
Cite as
Johannes Schmidt and Michał Wrona. The Complexity of Abduction for Equality Constraint Languages. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 615-633, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{schmidt_et_al:LIPIcs.CSL.2013.615,
author = {Schmidt, Johannes and Wrona, Micha{\l}},
title = {{The Complexity of Abduction for Equality Constraint Languages}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {615--633},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.615},
URN = {urn:nbn:de:0030-drops-42229},
doi = {10.4230/LIPIcs.CSL.2013.615},
annote = {Keywords: Abduction, infinite structures, equality constraint languages, computational complexity, algebraic approach}
}
Document
A New Type Assignment for Strongly Normalizable Terms
Abstract
We consider an operator definable in the intuitionistic theory of monadic predicates and we axiomatize some of its properties in a definitional extension of that monadic logic. The axiomatization lends itself to a natural deduction formulation to which the Curry-Howard isomorphism can be applied. The resulting Church style type system has the property that an untyped term is typable if and only if it is strongly normalizable.
Cite as
Rick Statman. A New Type Assignment for Strongly Normalizable Terms. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 634-652, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{statman:LIPIcs.CSL.2013.634,
author = {Statman, Rick},
title = {{A New Type Assignment for Strongly Normalizable Terms}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {634--652},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.634},
URN = {urn:nbn:de:0030-drops-42233},
doi = {10.4230/LIPIcs.CSL.2013.634},
annote = {Keywords: lambda calculus}
}
Document
Semantics of Intensional Type Theory extended with Decidable Equational Theories
Abstract
Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions (CC) provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensionality generally leads to undecidable type-checking, it seems a reasonable trade-off to extend intensional equality with a decidable first-order theory, as experimented in earlier work on CoqMTU and its implementation CoqMT.
In this work, CoqMTU is extended with strong eliminations. The meta-theoretical study, particularly the part relying on semantic arguments, is more complex. A set-theoretical model of the equational theory is the key ingredient to derive the logical consistency of the formalism. Strong normalization, the main lemma from which type-decidability follows, is proved by attaching realizability information to the values of the model.
The approach we have followed is to first consider an abstract notion of first-order equational theory, and then instantiate it with a particular instance, Presburger Arithmetic. These results have been formalized using Coq.
Cite as
Qian Wang and Bruno Barras. Semantics of Intensional Type Theory extended with Decidable Equational Theories. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 653-667, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@InProceedings{wang_et_al:LIPIcs.CSL.2013.653,
author = {Wang, Qian and Barras, Bruno},
title = {{Semantics of Intensional Type Theory extended with Decidable Equational Theories}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {653--667},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Ronchi Della Rocca, Simona},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.653},
URN = {urn:nbn:de:0030-drops-42241},
doi = {10.4230/LIPIcs.CSL.2013.653},
annote = {Keywords: Calculus of Constructions, Extensional Type Theory, Intensional Type Theory, Model, Meta-theory, Consistency, Strong Normalization, Presburger Arithme}
}