Volume
LIPIcs, Volume 16
Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Event
CSL 2012, September 3-6, 2012, Fontainebleau, FranceEditors
Publication Details
- published at: 2012-09-03
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-42-2
- DBLP: db/conf/csl/csl2012
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 16, CSL'12, Complete Volume
Abstract
LIPIcs, Volume 16, CSL'12, Complete Volume
Cite as
Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@Proceedings{cegielski_et_al:LIPIcs.CSL.2012,
title = {{LIPIcs, Volume 16, CSL'12, Complete Volume}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2013},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012},
URN = {urn:nbn:de:0030-drops-41106},
doi = {10.4230/LIPIcs.CSL.2012},
annote = {Keywords: Conference Proceedings; Software; Theory of Computation; Graph Theory; Probability and Statistics; Artificial Intelligence}
}
Document
Front Matter
Frontmatter, Table of Contents, Preface, Conference Organization
Abstract
Frontmatter, Table of Contents, Preface, Conference Organization
Cite as
Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. i-xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{cegielski_et_al:LIPIcs.CSL.2012.i,
author = {C\'{e}gielski, Patrick and Durand, Arnaud},
title = {{Frontmatter, Table of Contents, Preface, Conference Organization}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {i--xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.i},
URN = {urn:nbn:de:0030-drops-36559},
doi = {10.4230/LIPIcs.CSL.2012.i},
annote = {Keywords: Frontmatter, Table of Contents, Preface, Conference Organization}
}
Document
The Ackermann Award 2012
Abstract
Report on the Ackermann Award 2012.
Cite as
Thierry Coquand, Anuj Dawar, and Damian Niwinski. The Ackermann Award 2012. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{coquand_et_al:LIPIcs.CSL.2012.1,
author = {Coquand, Thierry and Dawar, Anuj and Niwinski, Damian},
title = {{The Ackermann Award 2012}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {1--5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.1},
URN = {urn:nbn:de:0030-drops-36575},
doi = {10.4230/LIPIcs.CSL.2012.1},
annote = {Keywords: Ackermann Award 2012}
}
Document
Invited Talk
Sharing Distributed Knowledge on the Web (Invited Talk)
Abstract
To share information, we propose to see the Web as a knowledge base consisting of distributed logical facts and rules. Our objective is to help Web users finding information, as well as controlling their own, using automated reasoning over this knowledge base towards improving the quality of service and of data. For this, we introduce Webdamlog, a Datalog-style language with rule delegation. We mention the implementation of a system to support this language as well as standard communications and security protocols.
Cite as
Serge Abiteboul. Sharing Distributed Knowledge on the Web (Invited Talk). In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 6-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{abiteboul:LIPIcs.CSL.2012.6,
author = {Abiteboul, Serge},
title = {{Sharing Distributed Knowledge on the Web}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {6--8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.6},
URN = {urn:nbn:de:0030-drops-36584},
doi = {10.4230/LIPIcs.CSL.2012.6},
annote = {Keywords: Knowledge base, distributed data, world wide web, deduction}
}
Document
Invited Talk
Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems (Invited Talk)
Abstract
This is a survey talk explaining the connection between the three items mentioned in the title.
Cite as
Stephen A. Cook. Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems (Invited Talk). In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 9-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{cook:LIPIcs.CSL.2012.9,
author = {Cook, Stephen A.},
title = {{Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {9--11},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.9},
URN = {urn:nbn:de:0030-drops-36594},
doi = {10.4230/LIPIcs.CSL.2012.9},
annote = {Keywords: Complexity Classes, Weak Formal Theories, Propositional Proof Systems}
}
Document
Invited Talk
Satisfiability: where Theory meets Practice (Invited Talk)
Abstract
Propositional Satisfiability (SAT) is a keystone in the history of computer science. SAT was the first problem shown to be NP-complete in 1971 by Stephen Cook. Having passed more than 40 years from then, SAT is now a lively research field where theory and practice have a natural intermixing. In this talk, we overview the use of SAT in practical domains, where SAT is thought in a broad sense, i.e. including SAT extensions such as Maximum Satisfiability (MaxSAT), Pseudo-Boolean Optimization (PBO) and Quantified Boolean Formulas (QBF).
Cite as
Inês Lynce. Satisfiability: where Theory meets Practice (Invited Talk). In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 12-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{lynce:LIPIcs.CSL.2012.12,
author = {Lynce, In\^{e}s},
title = {{Satisfiability: where Theory meets Practice}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {12--13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.12},
URN = {urn:nbn:de:0030-drops-36600},
doi = {10.4230/LIPIcs.CSL.2012.12},
annote = {Keywords: Propositional Satisfiability, SAT solvers, Applications}
}
Document
Invited Talk
Definability and Complexity of Graph Parameters (Invited Talk)
Abstract
In this talk we survey definability and complexity results of graph parameters which take values in some ring or field R.
Cite as
Johann A. Makowsky. Definability and Complexity of Graph Parameters (Invited Talk). In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 14-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{makowsky:LIPIcs.CSL.2012.14,
author = {Makowsky, Johann A.},
title = {{Definability and Complexity of Graph Parameters}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {14--15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.14},
URN = {urn:nbn:de:0030-drops-36612},
doi = {10.4230/LIPIcs.CSL.2012.14},
annote = {Keywords: Model theory, finite model theory, graph invariants}
}
Document
A Syntactical Approach to Weak omega-Groupoids
Abstract
When moving to a Type Theory without proof-irrelevance the notion of a setoid has to be generalized to the notion of a weak omega-groupoid. As a first step in this direction we study the formalisation of weak omega-groupoids in Type Theory. This is motivated by Voevodsky's proposal of univalent type theory which is incompatible with proof-irrelevance and the results by Lumsdaine and Garner/van de Berg showing that the standard eliminator for equality gives rise to a weak omega-groupoid.
Cite as
Thorsten Altenkirch and Ondrej Rypacek. A Syntactical Approach to Weak omega-Groupoids. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 16-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{altenkirch_et_al:LIPIcs.CSL.2012.16,
author = {Altenkirch, Thorsten and Rypacek, Ondrej},
title = {{A Syntactical Approach to Weak omega-Groupoids}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {16--30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.16},
URN = {urn:nbn:de:0030-drops-36561},
doi = {10.4230/LIPIcs.CSL.2012.16},
annote = {Keywords: Type Theory, Category Theory, Higher dimensional structures}
}
Document
Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms
Abstract
Interactive realizability is a computational semantics of classical Arithmetic. It is based on interactive learning and was originally designed to interpret excluded middle and Skolem axioms for simple existential formulas. A realizer represents a proof/construction depending on some state, which is an approximation of some Skolem functions. The realizer interacts with the environment, which may provide a counter-proof, a counterexample invalidating the current construction of the realizer. But the realizer is always able to turn such a negative outcome into a positive information, which consists in some new piece of knowledge learned about the mentioned Skolem functions. The aim of this work is to extend Interactive realizability to a system which includes classical first-order Peano Arithmetic with Skolem axioms. For witness extraction, the learning capabilities of realizers will be exploited according to the paradigm of learning by levels. In particular, realizers of atomic formulas will be update procedures in the sense of Avigad and thus will be understood as stratified-learning algorithms.
Cite as
Federico Aschieri. Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 31-45, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{aschieri:LIPIcs.CSL.2012.31,
author = {Aschieri, Federico},
title = {{Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {31--45},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.31},
URN = {urn:nbn:de:0030-drops-36629},
doi = {10.4230/LIPIcs.CSL.2012.31},
annote = {Keywords: Interactive realizability, learning, classical Arithmetic, witness extraction}
}
Document
Relational Parametricity for Higher Kinds
Abstract
Reynolds' notion of relational parametricity has been extremely
influential and well studied for polymorphic programming languages and
type theories based on System F. The extension of relational
parametricity to higher kinded polymorphism, which allows
quantification over type operators as well as types, has not received
as much attention. We present a model of relational parametricity for
System Fomega, within the impredicative Calculus of Inductive
Constructions, and show how it forms an instance of a general class of
models defined by Hasegawa. We investigate some of the consequences of
our model and show that it supports the definition of inductive types,
indexed by an arbitrary kind, and with reasoning principles provided
by initiality.
Cite as
Robert Atkey. Relational Parametricity for Higher Kinds. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 46-61, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{atkey:LIPIcs.CSL.2012.46,
author = {Atkey, Robert},
title = {{Relational Parametricity for Higher Kinds}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {46--61},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.46},
URN = {urn:nbn:de:0030-drops-36638},
doi = {10.4230/LIPIcs.CSL.2012.46},
annote = {Keywords: Relational Parametricity, Higher Kinds, Polymorphism}
}
Document
Higher-Order Interpretations and Program Complexity
Abstract
Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of first-order functional languages to design criteria ensuring statically some
complexity bounds on programs. This fits in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. In this paper, we extend this approach to the higher-order setting. For that we consider the notion of simply-typed term rewriting systems, we define higher-order polynomial interpretations for them and give a criterion ensuring that a program can be executed in polynomial time. In order to obtain a criterion flexible enough to validate interesting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations, coupled with a simple termination criterion based on linear types and path-like orders.
Cite as
Patrick Baillot and Ugo Dal Lago. Higher-Order Interpretations and Program Complexity. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 62-76, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{baillot_et_al:LIPIcs.CSL.2012.62,
author = {Baillot, Patrick and Dal Lago, Ugo},
title = {{Higher-Order Interpretations and Program Complexity}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {62--76},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.62},
URN = {urn:nbn:de:0030-drops-36641},
doi = {10.4230/LIPIcs.CSL.2012.62},
annote = {Keywords: implicit complexity, higher-order rewriting, quasi-interpretations}
}
Document
Knowledge Spaces and the Completeness of Learning Strategies
Abstract
We propose a theory of learning aimed to formalize some ideas underlying Coquand's game semantics and Krivine's realizability of classical logic. We introduce a notion of knowledge state together with a new topology, capturing finite positive and negative information that guides a learning strategy. We use a leading example to illustrate how non-constructive proofs lead to continuous and effective learning strategies over knowledge spaces, and prove that our learning semantics is sound and complete w.r.t. classical truth, as it is the case for Coquand's and Krivine's approaches.
Cite as
Stefano Berardi and Ugo de'Liguoro. Knowledge Spaces and the Completeness of Learning Strategies. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 77-91, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{berardi_et_al:LIPIcs.CSL.2012.77,
author = {Berardi, Stefano and de'Liguoro, Ugo},
title = {{Knowledge Spaces and the Completeness of Learning Strategies}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {77--91},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.77},
URN = {urn:nbn:de:0030-drops-36656},
doi = {10.4230/LIPIcs.CSL.2012.77},
annote = {Keywords: Classical Logic, Proof Mining, Game Semantics, Learning, Realizability}
}
Document
Bounded Satisfiability for PCTL
Abstract
While model checking PCTL for Markov chains is decidable in polynomial-time, the decidability of PCTL satisfiability is a long standing open problem. While general satisfiability is an intriguing challenge from a purely theoretical point of view, we argue that general solutions would not be of interest to practitioners: such solutions could be too big to be implementable or even infinite. Inspired by bounded synthesis techniques, we turn to the more applied
problem of seeking models of a bounded size: we restrict our search to
implementable - and therefore reasonably simple - models. We propose a
procedure to decide whether or not a given PCTL formula has an implementable model by reducing it to an SMT problem. We have implemented our techniques and found that they can be applied to the practical problem of sanity checking - a procedure that allows a system designer to check whether their formula has an unexpectedly small model.
Cite as
Nathalie Bertrand, John Fearnley, and Sven Schewe. Bounded Satisfiability for PCTL. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 92-106, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{bertrand_et_al:LIPIcs.CSL.2012.92,
author = {Bertrand, Nathalie and Fearnley, John and Schewe, Sven},
title = {{Bounded Satisfiability for PCTL}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {92--106},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.92},
URN = {urn:nbn:de:0030-drops-36667},
doi = {10.4230/LIPIcs.CSL.2012.92},
annote = {Keywords: Satisfiability, Temporal Logic, Probabilistic Logic}
}
Document
A Concurrent Logical Relation
Abstract
We present a logical relation for showing the correctness of program
transformations based on a new type-and-effect system for a concurrent
extension of an ML-like language with higher-order functions,
higher-order store and dynamic memory allocation.
We show how to use our model to verify a number of interesting program
transformations that rely on effect annotations. In particular, we
prove a Parallelization Theorem, which expresses when it is sound to
run two expressions in parallel instead of sequentially. The
conditions are expressed solely in terms of the types and effects of
the expressions. To the best of our knowledge, this is the first such
result for a concurrent higher-order language with higher-order store
and dynamic memory allocation.
Cite as
Lars Birkedal, Filip Sieczkowski, and Jacob Thamsborg. A Concurrent Logical Relation. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 107-121, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{birkedal_et_al:LIPIcs.CSL.2012.107,
author = {Birkedal, Lars and Sieczkowski, Filip and Thamsborg, Jacob},
title = {{A Concurrent Logical Relation}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {107--121},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.107},
URN = {urn:nbn:de:0030-drops-36671},
doi = {10.4230/LIPIcs.CSL.2012.107},
annote = {Keywords: verification, logical relation, concurrency, type and effect system}
}
Document
Equivalence Constraint Satisfaction Problems
Abstract
The following result for finite structures Gamma has been conjectured to hold for all countably infinite omega-categorical structures Gamma: either the model-complete core Delta of Gamma has an expansion by finitely many constants such that the pseudovariety generated by its polymorphism algebra contains a two-element algebra all of whose operations are projections, or there is a homomorphism f from Delta^k to Delta, for some finite k, and an automorphism alpha of Delta satisfying f(x1,...,xk) = alpha(f(x2,...,xk,x1)). This conjecture has been confirmed for all infinite structures Gamma that have a first-order definition over (Q;<), and for all structures that are definable over the random graph. In this paper, we verify the conjecture for all structures that are definable over an equivalence relation with a countably infinite number of countably infinite classes.
Our result implies a complexity dichotomy (into NP-complete and P) for a family of constraint satisfaction problems (CSPs) which we call equivalence constraint satisfaction problems. The classification for equivalence CSPs can also be seen as a first step towards a classification of the CSPs for all relational structures that are first-order definable over Allen's interval algebra, a well-known constraint calculus in temporal reasoning.
Cite as
Manuel Bodirsky and Michal Wrona. Equivalence Constraint Satisfaction Problems. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 122-136, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{bodirsky_et_al:LIPIcs.CSL.2012.122,
author = {Bodirsky, Manuel and Wrona, Michal},
title = {{Equivalence Constraint Satisfaction Problems}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {122--136},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.122},
URN = {urn:nbn:de:0030-drops-36689},
doi = {10.4230/LIPIcs.CSL.2012.122},
annote = {Keywords: Constraint satisfaction problems, universal algebra, model theory, Ram- sey theory, temporal reasoning, computational complexity}
}
Document
A Negative Conjunctive Query is Easy if and only if it is Beta-Acyclic
Abstract
It is known that the data complexity of a Conjunctive Query (CQ) is determined *only* by the way its variables are shared between atoms, reflected by its hypergraph. In particular, Yannakakis [Yannakakis VLDB'81,Beeri/Fagin/Maier/Yannakakis JACM'83] proved that a CQ is decidable in linear time when it is alpha-acyclic, i.e. its hypergraph is alpha-acyclic; Bagan et al. [Bagan/Durand/Grandjean CSL'07] even state:
* Any CQ is decidable in linear time iff it is alpha-acyclic. (under certain hypotheses)
(By linear time, we mean a query on a structure S can be decided in time O(|S|))
A natural question is: since the complexity of a *Negative* Conjunctive Query (NCQ), a conjunctive query where *all* atoms are negated, also only depends on its hypergraph, can we find a similar dichotomy in this case?
To answer this question, we revisit a result of Ordyniak et al. --- that states that satisfiability of a beta-acyclic CNF formula is decidable in polynomial time --- by proving that some part of their procedure can be done in linear time. This implies, under an algorithmic hypothesis that is likely true: (precisely: one cannot decide whether a graph is triangle-free in time O(n²log n) where n is the number of vertices.)
* Any NCQ is decidable in quasi-linear time iff it is beta-acyclic.
(By quasi-linear time, we mean a query on a structure S can be decided in time O(|S|log|S|))
We extend the easiness result to 'Signed' Conjunctive Query (SCQ) where 'some' atoms are negated. This has great interest since using some negated atoms is natural in the frameworks of databases and CSP. Furthermore, it implies straightforwardly the following:
* Any beta-acyclic existential first-order query is decidable in quasi-linear time.
Cite as
Johann Brault-Baron. A Negative Conjunctive Query is Easy if and only if it is Beta-Acyclic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 137-151, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{braultbaron:LIPIcs.CSL.2012.137,
author = {Brault-Baron, Johann},
title = {{A Negative Conjunctive Query is Easy if and only if it is Beta-Acyclic}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {137--151},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.137},
URN = {urn:nbn:de:0030-drops-36697},
doi = {10.4230/LIPIcs.CSL.2012.137},
annote = {Keywords: conjunctive query, hypergraph, beta-acyclicity, data complexity, Davis-Putnam procedure}
}
Document
On the equational consistency of order-theoretic models of the lambda-calculus
Abstract
Answering a question by Honsell and Plotkin, we show that there are two equations between lambda terms, the so-called subtractive equations, consistent with lambda calculus but not satisfied in any partially ordered model with bottom element. We also relate the subtractive equations to the open problem of the order-incompleteness of lambda calculus.
Cite as
Alberto Carraro and Antonino Salibra. On the equational consistency of order-theoretic models of the lambda-calculus. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 152-166, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{carraro_et_al:LIPIcs.CSL.2012.152,
author = {Carraro, Alberto and Salibra, Antonino},
title = {{On the equational consistency of order-theoretic models of the lambda-calculus}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {152--166},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.152},
URN = {urn:nbn:de:0030-drops-36703},
doi = {10.4230/LIPIcs.CSL.2012.152},
annote = {Keywords: Lambda calculus, order-incompleteness, partially ordered models}
}
Document
Faster Algorithms for Alternating Refinement Relations
Abstract
One central issue in the formal design and analysis of reactive systems is the notion of refinement that asks whether all behaviors of the implementation is allowed by the specification. The local interpretation of behavior leads to the notion of simulation. Alternating transition systems (ATSs) provide a general model for composite reactive systems, and the simulation relation for ATSs is known as alternating simulation. The simulation relation for fair transition systems is called fair simulation. In this work our main contributions are as follows: (1) We present an improved algorithm for fair simulation with Büchi fairness constraints; our algorithm requires O(n^3 * m) time as compared to the previous known O(n^6)-time algorithm, where n is the number of states and m is the number of transitions. (2) We present a game based algorithm for alternating simulation that requires O(m^2)-time as compared to the previous known O((n*m)^2)-time algorithm, where n is the number of states and m is the size of transition relation. (3) We present an iterative algorithm for alternating simulation that matches the time complexity of the game based algorithm, but is more space efficient than the game based algorithm.
Cite as
Krishnendu Chatterjee, Siddhesh Chaubal, and Pritish Kamath. Faster Algorithms for Alternating Refinement Relations. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 167-182, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{chatterjee_et_al:LIPIcs.CSL.2012.167,
author = {Chatterjee, Krishnendu and Chaubal, Siddhesh and Kamath, Pritish},
title = {{Faster Algorithms for Alternating Refinement Relations}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {167--182},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.167},
URN = {urn:nbn:de:0030-drops-36713},
doi = {10.4230/LIPIcs.CSL.2012.167},
annote = {Keywords: Simulation and fair simulation, Alternating simulation, Graph games}
}
Document
A Systematic Approach to Canonicity in the Classical Sequent Calculus
Abstract
The sequent calculus is often criticized for requiring proofs to
contain large amounts of low-level syntactic details that can obscure the essence of a given proof. Because each inference rule introduces only a single connective, sequent proofs can separate closely related steps-such as instantiating a block of quantifiers-by irrelevant noise. Moreover, the sequential nature of sequent proofs forces proof steps that are syntactically non-interfering and permutable to nevertheless be written in some arbitrary order. The sequent calculus thus lacks a notion of canonicity: proofs that should be considered essentially the same may not have a common syntactic form. To fix this problem, many researchers have proposed replacing the sequent calculus with proof structures that are more parallel or geometric. Proof-nets, matings, and atomic flows are examples of such revolutionary formalisms. We propose, instead, an evolutionary approach to recover canonicity within the sequent calculus, which we illustrate for classical first-order logic. The essential element of our approach is the use of a multi-focused sequent calculus as the means of abstracting away the details from classical cut-free sequent proofs. We show that, among the multi-focused proofs, the maximally multi-focused proofs that make the foci as parallel as possible are canonical. Moreover, such proofs are isomorphic to expansion proofs - a well known, minimalistic, and parallel generalization of Herbrand
disjunctions - for classical first-order logic. This technique is a
systematic way to recover the desired essence of any sequent proof
without abandoning the sequent calculus.
Cite as
Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A Systematic Approach to Canonicity in the Classical Sequent Calculus. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 183-197, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{chaudhuri_et_al:LIPIcs.CSL.2012.183,
author = {Chaudhuri, Kaustuv and Hetzl, Stefan and Miller, Dale},
title = {{A Systematic Approach to Canonicity in the Classical Sequent Calculus}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {183--197},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.183},
URN = {urn:nbn:de:0030-drops-36723},
doi = {10.4230/LIPIcs.CSL.2012.183},
annote = {Keywords: Sequent Calculus, Canonicity, Classical Logic, Expansion Trees}
}
Document
ML with PTIME complexity guarantees
Abstract
Implicit Computational Complexity is a line of research where the possibility to inference a valid property for a program implies that the program runs in particular complexity class. Soft type systems are one of the research threads within the field. We present here a soft type system with ML-like polymorphism that enjoys decidable typechecking, type inference and typability problems and gives polynomial time computational guarantees for the running time of typed
programs.
Cite as
Jacek Chrzaszcz and Aleksy Schubert. ML with PTIME complexity guarantees. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 198-212, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{chrzaszcz_et_al:LIPIcs.CSL.2012.198,
author = {Chrzaszcz, Jacek and Schubert, Aleksy},
title = {{ML with PTIME complexity guarantees}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {198--212},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.198},
URN = {urn:nbn:de:0030-drops-36738},
doi = {10.4230/LIPIcs.CSL.2012.198},
annote = {Keywords: implicit computational complexity, polymorphism, soft type assignment}
}
Document
Definability of linear equation systems over groups and rings
Abstract
Motivated by the quest for a logic for PTIME and recent insights that the descriptive complexity of problems from linear algebra is a crucial aspect of this problem, we study the solvability of linear equation systems over finite groups and rings from the viewpoint of logical (inter-)definability. All problems that we consider are decidable in polynomial time, but not expressible in fixed-point logic with counting. They also provide natural candidates for a separation of polynomial time from rank logics, which extend fixed-point logics by operators for determining the rank of definable matrices and which are sufficient for solvability problems over fields.
Based on the structure theory of finite rings, we establish logical reductions among various solvability problems. Our results indicate that all solvability problems for linear equation systems that separate fixed-point logic with counting from PTIME can be reduced to solvability over commutative rings. Further, we prove closure properties for classes of queries that reduce to solvability over rings. As an application, these closure properties provide normal forms for logics extended with solvability operators.
Cite as
Anuj Dawar, Erich Grädel, Bjarki Holm, Eryk Kopczynski, and Wied Pakusa. Definability of linear equation systems over groups and rings. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 213-227, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{dawar_et_al:LIPIcs.CSL.2012.213,
author = {Dawar, Anuj and Gr\"{a}del, Erich and Holm, Bjarki and Kopczynski, Eryk and Pakusa, Wied},
title = {{Definability of linear equation systems over groups and rings}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {213--227},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.213},
URN = {urn:nbn:de:0030-drops-36749},
doi = {10.4230/LIPIcs.CSL.2012.213},
annote = {Keywords: inite model theory, logics with algebraic operators}
}
Document
Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication
Abstract
Prior work has shown that intuitionistic linear logic can be seen as a
session-type discipline for the pi-calculus, where cut reduction in
the sequent calculus corresponds to synchronous process reduction. In
this paper, we exhibit a new process assignment from the asynchronous,
polyadic pi-calculus to exactly the same proof rules. Proof-theoretically, the difference between these interpretations can
be understood through permutations of inference rules that preserve
observational equivalence of closed processes in the synchronous case.
We also show that, under this new asynchronous interpretation, cut
reductions correspond to a natural asynchronous buffered session
semantics, where each session is allocated a separate communication
buffer.
Cite as
Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 228-242, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{deyoung_et_al:LIPIcs.CSL.2012.228,
author = {DeYoung, Henry and Caires, Lu{\'\i}s and Pfenning, Frank and Toninho, Bernardo},
title = {{Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {228--242},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.228},
URN = {urn:nbn:de:0030-drops-36753},
doi = {10.4230/LIPIcs.CSL.2012.228},
annote = {Keywords: linear logic, cut reduction, asynchronous pi-calculus, session types}
}
Document
Bounded Combinatory Logic
Abstract
In combinatory logic one usually assumes a fixed set of basic combinators (axiom schemes), usually K and S. In this setting the set of provable formulas (inhabited types) is PSPACE-complete in simple types and undecidable in intersection types. When arbitrary sets of axiom schemes are considered, the inhabitation problem is undecidable even in simple types (this is known as Linial-Post theorem).
k-bounded combinatory logic with intersection types arises from combinatory logic by imposing the bound k on the depth of types (formulae) which may be substituted for type variables in axiom schemes. We consider the inhabitation (provability) problem for k-bounded combinatory logic: Given an arbitrary set of typed combinators and a type tau, is there a combinatory term of type tau in k-bounded combinatory logic?
Our main result is that the problem is (k+2)-EXPTIME complete for k-bounded combinatory logic with intersection types, for every fixed k
(and hence non-elementary when k is a parameter). We also show that the problem is EXPTIME-complete for simple types, for all k.
Theoretically, our results give new insight into the expressive power of intersection types. From an application perspective, our results are useful as a foundation for composition synthesis based on combinatory logic.
Cite as
Boris Düdder, Moritz Martens, Jakob Rehof, and Pawel Urzyczyn. Bounded Combinatory Logic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 243-258, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{dudder_et_al:LIPIcs.CSL.2012.243,
author = {D\"{u}dder, Boris and Martens, Moritz and Rehof, Jakob and Urzyczyn, Pawel},
title = {{Bounded Combinatory Logic}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {243--258},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.243},
URN = {urn:nbn:de:0030-drops-36763},
doi = {10.4230/LIPIcs.CSL.2012.243},
annote = {Keywords: Intersection types, Inhabitation, Composition synthesis}
}
Document
Collapsing non-idempotent intersection types
Abstract
We proved recently that the extensional collapse of the relational model of linear logic coincides with its Scott model, whose objects are preorders and morphisms are downwards closed relations. This result is obtained by the construction of a new model whose objects can be understood as preorders equipped with a realizability predicate. We present this model, which features a new duality, and explain how to use it for reducing normalization results in idempotent intersection types (usually proved by reducibility) to purely combinatorial methods. We illustrate this approach in the case of the call-by-value lambda-calculus, for which we introduce a new resource calculus, but it can be applied in the same way to many different calculi.
Cite as
Thomas Ehrhard. Collapsing non-idempotent intersection types. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 259-273, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{ehrhard:LIPIcs.CSL.2012.259,
author = {Ehrhard, Thomas},
title = {{Collapsing non-idempotent intersection types}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {259--273},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.259},
URN = {urn:nbn:de:0030-drops-36776},
doi = {10.4230/LIPIcs.CSL.2012.259},
annote = {Keywords: Linear logic, lambda-calculus, denotational semantics}
}
Document
Descriptive complexity for pictures languages
Abstract
This paper deals with logical characterizations of picture languages of any dimension by syntactical fragments of existential second-order logic. Two classical classes of picture languages are studied:
- the class of "recognizable" picture languages, i.e. projections of languages defined by local constraints (or tilings): it is known as the most robust class extending the class of regular languages to any dimension;
- the class of picture languages recognized on "nondeterministic cellular automata in linear time" : cellular automata are the simplest and most natural model of parallel computation and linear time is the minimal time-bounded class allowing synchronization of nondeterministic cellular automata.
We uniformly generalize to any dimension the characterization by Giammarresi et al. (1996) of the class of "recognizable" picture languages in existential monadic second-order logic.
We state several logical characterizations of the class of picture languages recognized in linear time on nondeterministic cellular automata. They are the first machine-independent characterizations of complexity classes of cellular automata.
Our characterizations are essentially deduced from normalization results we prove for first-order and existential second-order logics over pictures. They are obtained in a general and uniform framework that allows to extend them to other "regular" structures.
Cite as
Etienne Grandjean and Frédéric Olive. Descriptive complexity for pictures languages. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 274-288, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{grandjean_et_al:LIPIcs.CSL.2012.274,
author = {Grandjean, Etienne and Olive, Fr\'{e}d\'{e}ric},
title = {{Descriptive complexity for pictures languages}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {274--288},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.274},
URN = {urn:nbn:de:0030-drops-36783},
doi = {10.4230/LIPIcs.CSL.2012.274},
annote = {Keywords: Picture languages, locality and tiling, recognizability, linear time, cellular automata, logical characterizations, second-order logic}
}
Document
Pebble Games and Linear Equations
Abstract
We give a new, simplified and detailed account of the correspondence
between levels of the Sherali-Adams relaxation of graph isomorphism
and levels of pebble-game equivalence with counting (higher-dimensional Weisfeiler-Lehman colour refinement). The correspondence between basic colour refinement and fractional isomorphism, due to Ramana, Scheinerman and Ullman, is re-interpreted as the base level of Sherali-Adams and generalised to higher levels in this sense by Atserias and Maneva, who prove that the two resulting hierarchies interleave.
In carrying this analysis further, we here give (a) a precise characterisation of the level-k Sherali-Adams relaxation in terms of a modified counting pebble game; (b) a variant of the Sherali-Adams levels that precisely match the k-pebble counting game; (c) a proof that the interleaving between these two hierarchies is strict.
We also investigate the variation based on boolean arithmetic instead
of real/rational arithmetic and obtain analogous correspondences and
separations for plain k-pebble equivalence (without counting). Our
results are driven by considerably simplified accounts of the
underlying combinatorics and linear algebra.
Cite as
Martin Grohe and Martin Otto. Pebble Games and Linear Equations. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 289-304, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{grohe_et_al:LIPIcs.CSL.2012.289,
author = {Grohe, Martin and Otto, Martin},
title = {{Pebble Games and Linear Equations}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {289--304},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.289},
URN = {urn:nbn:de:0030-drops-36790},
doi = {10.4230/LIPIcs.CSL.2012.289},
annote = {Keywords: Finite model theory, finite variable logics, graph isomorphism, Weisfeiler- Lehman algorithm, linear programming, Sherali–Adams hierarchy}
}
Document
Banach-Mazur Games with Simple Winning Strategies
Abstract
We discuss several notions of "simple" winning strategies for
Banach-Mazur games on graphs, such as positional strategies,
move-counting or length-counting strategies, and strategies with a
memory based on finite appearance records (FAR). We investigate
classes of Banach-Mazur games that are determined via these kinds of
winning strategies.
Banach-Mazur games admit stronger determinacy results than classical
graph games. For instance, all Banach-Mazur games with omega-regular
winning conditions are positionally determined. Beyond the
omega-regular winning conditions, we focus here on Muller conditions
with infinitely many colours. We investigate the infinitary Muller
conditions that guarantee positional determinacy for Banach-Mazur
games. Further, we determine classes of such conditions that require
infinite memory but guarantee determinacy via move-counting
strategies, length-counting strategies, and FAR-strategies. We also
discuss the relationships between these different notions of determinacy.
Cite as
Erich Grädel and Simon Leßenich. Banach-Mazur Games with Simple Winning Strategies. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 305-319, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{gradel_et_al:LIPIcs.CSL.2012.305,
author = {Gr\"{a}del, Erich and Le{\ss}enich, Simon},
title = {{Banach-Mazur Games with Simple Winning Strategies}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {305--319},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.305},
URN = {urn:nbn:de:0030-drops-36806},
doi = {10.4230/LIPIcs.CSL.2012.305},
annote = {Keywords: Banach-Mazur games, winning strategies, positional determinacy, Muller winning conditions}
}
Document
Herbrand-Confluence for Cut Elimination in Classical First Order Logic
Abstract
We consider cut-elimination in the sequent calculus for classical
first-order logic. It is well known that this system, in its most
general form, is neither confluent nor strongly normalizing. In this
work we take a coarser (and mathematically more realistic) look at
cut-free proofs. We analyze which witnesses they choose for which
quantifiers, or in other words: we only consider the
Herbrand-disjunction of a cut-free proof. Our main theorem is a
confluence result for a natural class of proofs: all (possibly
infinitely many) normal forms of the non-erasing reduction lead to the
same Herbrand-disjunction.
Cite as
Stefan Hetzl and Lutz Straßburger. Herbrand-Confluence for Cut Elimination in Classical First Order Logic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 320-334, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{hetzl_et_al:LIPIcs.CSL.2012.320,
author = {Hetzl, Stefan and Stra{\ss}burger, Lutz},
title = {{Herbrand-Confluence for Cut Elimination in Classical First Order Logic}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {320--334},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.320},
URN = {urn:nbn:de:0030-drops-36815},
doi = {10.4230/LIPIcs.CSL.2012.320},
annote = {Keywords: proof theory, first-order logic, tree languages, term rewriting, semantics of proofs}
}
Document
A Computational Interpretation of the Axiom of Determinacy in Arithmetic
Abstract
We investigate the computational content of the axiom of determinacy (AD) in the setting of classical arithmetic in all finite types with the principle of dependent choices (DC). By employing the notion of realizability interpretation for arithmetic given by Berardi, Bezem and Coquand (1998), we interpret the negative translation of AD. Consequently, the combination of the negative translation with this realizability semantics can be seen as a model of DC, AD and the negation of the axiom of choice at higher types. In order to understand the computational content of AD, we explain, employing Coquand's game theoretical semantics, how our realizer behaves.
Cite as
Takanori Hida. A Computational Interpretation of the Axiom of Determinacy in Arithmetic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 335-349, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{hida:LIPIcs.CSL.2012.335,
author = {Hida, Takanori},
title = {{A Computational Interpretation of the Axiom of Determinacy in Arithmetic}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {335--349},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.335},
URN = {urn:nbn:de:0030-drops-36828},
doi = {10.4230/LIPIcs.CSL.2012.335},
annote = {Keywords: The axiom of determinacy, Gale-Stewart’s theorem, Syntactic continuity, Realizability interpretation, Coquand’s game semantics}
}
Document
Church-Rosser Properties of Normal Rewriting
Abstract
We prove a general purpose abstract Church-Rosser result that captures most existing such results that rely on termination of computations. This is achieved by studying abstract normal rewriting in a way that allows to incorporate positions at the abstract level. New concrete Church-Rosser results are obtained, in particular for higher-order rewriting at higher types.
Cite as
Jean-Pierre Jouannaud and Jianqi Li. Church-Rosser Properties of Normal Rewriting. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 350-365, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{jouannaud_et_al:LIPIcs.CSL.2012.350,
author = {Jouannaud, Jean-Pierre and Li, Jianqi},
title = {{Church-Rosser Properties of Normal Rewriting}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {350--365},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.350},
URN = {urn:nbn:de:0030-drops-36839},
doi = {10.4230/LIPIcs.CSL.2012.350},
annote = {Keywords: abstract normal rewriting, Church-Rosser property}
}
Document
A Counting Logic for Structure Transition Systems
Abstract
Quantitative questions such as "what is the maximum number of tokens
in a place of a Petri net?" or "what is the maximal reachable height
of the stack of a pushdown automaton?" play a significant role in
understanding models of computation. To study such problems in a
systematic way, we introduce structure transition systems on which
one can define logics that mix temporal expressions (e.g. reachability) with properties of a state (e.g. the height of the stack). We propose a counting logic Qmu[#MSO] which allows to express questions like the ones above, and also many boundedness problems studied so far. We show that Qmu[#MSO] has good algorithmic properties, in particular we generalize two standard methods in model checking, decomposition on trees and model checking through parity games, to this quantitative logic. These properties are used to prove decidability of Qmu[#MSO] on tree-producing pushdown systems, a generalization of both pushdown systems and regular tree grammars.
Cite as
Lukasz Kaiser and Simon Leßenich. A Counting Logic for Structure Transition Systems. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 366-380, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{kaiser_et_al:LIPIcs.CSL.2012.366,
author = {Kaiser, Lukasz and Le{\ss}enich, Simon},
title = {{A Counting Logic for Structure Transition Systems}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {366--380},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.366},
URN = {urn:nbn:de:0030-drops-36848},
doi = {10.4230/LIPIcs.CSL.2012.366},
annote = {Keywords: Logic in Computer Science, Quantitative Logics, Model Checking}
}
Document
Parametricity in an Impredicative Sort
Abstract
Reynold's abstraction theorem is now a well-established result for a
large class of type systems. We propose here a definition of relational parametricity and a proof of the abstraction theorem in the Calculus of Inductive Constructions (CIC), the underlying formal language of Coq, in which parametricity relations' codomain is the impredicative sort of propositions. To proceed, we need to refine this calculus by splitting the sort hierarchy to separate informative terms from non-informative terms. This refinement is very close to CIC, but with the property that typing judgments can distinguish informative terms. Among many applications, this natural encoding of parametricity inside CIC serves both theoretical purposes (proving the independence of propositions with respect to the logical system) as well as practical aspirations (proving properties of finite algebraic structures). We finally discuss how we can simply build, on top of our calculus, a new reflexive Coq tactic that constructs proof terms by parametricity.
Cite as
Chantal Keller and Marc Lasson. Parametricity in an Impredicative Sort. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 381-395, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{keller_et_al:LIPIcs.CSL.2012.381,
author = {Keller, Chantal and Lasson, Marc},
title = {{Parametricity in an Impredicative Sort}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {381--395},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.381},
URN = {urn:nbn:de:0030-drops-36851},
doi = {10.4230/LIPIcs.CSL.2012.381},
annote = {Keywords: Calculus of Inductive Constructions, parametricity, impredicativity, Coq, universes}
}
Document
Two-Variable Universal Logic with Transitive Closure
Abstract
We prove that the satisfiability problem for the two-variable, universal fragment of first-order logic with constants (or, alternatively phrased, for the Bernays-Schönfinkel class with two universally quantified variables) remains decidable after augmenting the fragment by the transitive closure of a single binary relation. We give a 2-NExpTime-upper bound and a 2-ExpTime-lower bound for the complexity of the problem. We also study the cases in which the number of constants is restricted. It appears that with two constants the considered fragment has the finite model property and NExpTime-complete satisfiability problem. Adding a third constant does not change the complexity but allows to construct infinity axioms. A fourth constant lifts the lower complexity bound to TwoExpTime. Finally, we observe that we are close to the border between decidability and undecidability: adding a third variable or the transitive closure of a second binary relation lead to undecidability.
Cite as
Emanuel Kieronski and Jakub Michaliszyn. Two-Variable Universal Logic with Transitive Closure. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 396-410, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{kieronski_et_al:LIPIcs.CSL.2012.396,
author = {Kieronski, Emanuel and Michaliszyn, Jakub},
title = {{Two-Variable Universal Logic with Transitive Closure}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {396--410},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.396},
URN = {urn:nbn:de:0030-drops-36860},
doi = {10.4230/LIPIcs.CSL.2012.396},
annote = {Keywords: two-variable logic, transitive closure, decidability}
}
Document
Connection Matrices and the Definability of Graph Parameters
Abstract
In this paper we extend the Finite Rank Theorem for connection matrices of graph parameters definable in Monadic Second Order Logic with modular counting CMSOL of B. Godlin, T. Kotek and J.A. Makowsky (2008 and 2009), and demonstrate its vast applicability in simplifying known and new non-definability results of graph properties and finding new non-definability results for graph parameters. We also prove a Feferman-Vaught Theorem for the logic CFOL, First Order Logic with the modular counting quantifiers.
Cite as
Tomer Kotek and Johann A. Makowsky. Connection Matrices and the Definability of Graph Parameters. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 411-425, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{kotek_et_al:LIPIcs.CSL.2012.411,
author = {Kotek, Tomer and Makowsky, Johann A.},
title = {{Connection Matrices and the Definability of Graph Parameters}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {411--425},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.411},
URN = {urn:nbn:de:0030-drops-36871},
doi = {10.4230/LIPIcs.CSL.2012.411},
annote = {Keywords: Model theory, finite model theory, graph invariants}
}
Document
The FO2 alternation hierarchy is decidable
Abstract
We consider the two-variable fragment FO2[<] of first-order
logic over finite words. Numerous characterizations of this class are
known. Therien and Wilke have shown that it is decidable whether a
given regular language is definable in FO2[<]. From a practical
point of view, as shown by Weis, FO2[<] is interesting since its
satisfiability problem is in NP. Restricting the number of
quantifier alternations yields an infinite hierarchy inside the class
of FO2[<]-definable languages. We show that each level of this
hierarchy is decidable. For this purpose, we relate each level of the
hierarchy with a decidable variety of finite monoids.
Our result implies that there are many different ways of climbing up
the FO2[<]-quantifier alternation hierarchy: deterministic and
co-deterministic products, Mal'cev products with definite and reverse
definite semigroups, iterated block products with J-trivial
monoids, and some inductively defined omega-term identities. A
combinatorial tool in the process of ascension is that of condensed
rankers, a refinement of the rankers of Weis and Immerman and the
turtle programs of Schwentick, Therien, and Vollmer.
Cite as
Manfred Kufleitner and Pascal Weil. The FO2 alternation hierarchy is decidable. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 426-439, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{kufleitner_et_al:LIPIcs.CSL.2012.426,
author = {Kufleitner, Manfred and Weil, Pascal},
title = {{The FO2 alternation hierarchy is decidable}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {426--439},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.426},
URN = {urn:nbn:de:0030-drops-36888},
doi = {10.4230/LIPIcs.CSL.2012.426},
annote = {Keywords: first-order logic, regular language, automata theory, semigroup, ranker}
}
Document
Axiomatizing proof tree concepts in Bounded Arithmetic
Abstract
We construct theories of Cook-Nguyen style two-sort bounded arithmetic
whose provably total functions are exactly those in LOGCFL and LOGDCFL.
Axiomatizations of both theories are based on the proof tree size
characterizations of these classes. We also show that our theory for LOGCFL proves a certain formulation of the pumping lemma for context-free languages.
Cite as
Satoru Kuroda. Axiomatizing proof tree concepts in Bounded Arithmetic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 440-454, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{kuroda:LIPIcs.CSL.2012.440,
author = {Kuroda, Satoru},
title = {{Axiomatizing proof tree concepts in Bounded Arithmetic}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {440--454},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.440},
URN = {urn:nbn:de:0030-drops-36893},
doi = {10.4230/LIPIcs.CSL.2012.440},
annote = {Keywords: Bounded Arithmetic, LOGCFL, LOGDCFL, Proof tree}
}
Document
Isomorphisms of scattered automatic linear orders
Abstract
We prove the undecidability of the existence of an isomorphism between
scattered tree-automatic linear orders as well as the existence of
automorphisms of scattered word automatic linear orders. For the
existence of automatic automorphisms of word automatic linear orders,
we determine the exact level of undecidability in the arithmetical
hierarchy.
Cite as
Dietrich Kuske. Isomorphisms of scattered automatic linear orders. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 455-469, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{kuske:LIPIcs.CSL.2012.455,
author = {Kuske, Dietrich},
title = {{Isomorphisms of scattered automatic linear orders}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {455--469},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.455},
URN = {urn:nbn:de:0030-drops-36906},
doi = {10.4230/LIPIcs.CSL.2012.455},
annote = {Keywords: Automatic structures, isomorphism, automorphism}
}
Document
Undecidable First-Order Theories of Affine Geometries
Abstract
Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation (\beta) and a quaternary equidistance relation (\equiv). Tarski established, inter alia, that the first-order (FO) theory of (R^2,\beta,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,\beta) with unary predicates is decidable. We refute this conjecture by showing that for all n > 1, the FO-theory of monadic expansions of (R^n,\beta) is Pi^1_1-hard and therefore not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T,\beta), where T is a subset of R^n, and show that for each structure (T,\beta) in C, the FO-theory of the class of monadic expansions of (T,\beta) is undecidable. We then consider classes of expansions of structures (T,\beta) with restricted unary predicates, for example finite predicates, and establish a variety of related undecidability results. In addition to decidability questions, we briefly study the expressivity of universal MSO and weak universal MSO over expansions of (R^n,\beta). While the logics are incomparable in general, over expansions of (R^n,\beta), formulae of weak universal MSO translate into equivalent formulae of universal MSO. An extended version of this article can be found on the ArXiv (arXiv:1208.4930v1).
Cite as
Antti Kuusisto, Jeremy Meyers, and Jonni Virtema. Undecidable First-Order Theories of Affine Geometries. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 470-484, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{kuusisto_et_al:LIPIcs.CSL.2012.470,
author = {Kuusisto, Antti and Meyers, Jeremy and Virtema, Jonni},
title = {{Undecidable First-Order Theories of Affine Geometries}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {470--484},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.470},
URN = {urn:nbn:de:0030-drops-36910},
doi = {10.4230/LIPIcs.CSL.2012.470},
annote = {Keywords: Tarski’s geometry, undecidability, spatial logic, classical logic}
}
Document
Towards CERes in intuitionistic logic
Abstract
Cut-elimination, introduced by Gentzen, plays an important role in automating the analysis of mathematical proofs. The removal of cuts corresponds to the elimination of intermediate statements (lemmas), resulting in an analytic proof. CERes is a method of cut-elimination by resolution that relies on global proof transformations, in contrast to reductive methods, which use local proof-rewriting transformations. By avoiding redundant operations, it obtains a speed-up over Gentzen's traditional method (and its variations). CERes has been successfully implemented and applied to mathematical proofs, and it is fully developed for classical logic (first and higher order), multi-valued logics and Gödel logic. But when it comes to mathematical proofs, intuitionistic logic also plays an important role due to its constructive characteristics and computational interpretation.
This paper presents current developments on adapting the CERes method to intuitionistic sequent calculus LJ. First of all, we briefly describe the CERes method for classical logic and the problems that arise when extending the method to intuitionistic logic. Then, we present the solutions found for the mentioned problems for the subclass LJ- (the class of intuitionistic proofs of an end-sequent containing no strong quantifiers and no formula on the right). In addition, we explain, with an example, some ideas for improving the method and covering a bigger fragment of LJ proofs. Finally, we summarize the results and point the direction for future research.
Cite as
Alexander Leitsch, Giselle Reis, and Bruno Woltzenlogel Paleo. Towards CERes in intuitionistic logic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 485-499, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{leitsch_et_al:LIPIcs.CSL.2012.485,
author = {Leitsch, Alexander and Reis, Giselle and Woltzenlogel Paleo, Bruno},
title = {{Towards CERes in intuitionistic logic}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {485--499},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.485},
URN = {urn:nbn:de:0030-drops-36922},
doi = {10.4230/LIPIcs.CSL.2012.485},
annote = {Keywords: cut-elimination, resolution, LJ}
}
Document
Variants of Collapsible Pushdown Systems
Abstract
We analyze the relationship between three ways of generating trees using collapsible pushdown systems (CPS's): using deterministic CPS's, nondeterministic CPS's, and deterministic word-accepting CPS's. We prove that (for each level of the CPS and each input alphabet) the three classes of trees are equal. The nontrivial translations increase n-1 times exponentially the size of the level-n CPS. The same results stay true if we restrict ourselves to higher-order pushdown systems without collapse. As a second contribution we prove that the hierarchy of word languages recognized by nondeterministic CPS's is infinite. This is a consequence of a lemma which bounds the length of the shortest accepting run. It also implies that the hierarchy of epsilon-closures of configuration graphs is infinite (which was already known). As a side effect we obtain a new algorithm for the reachability problem for CPS's; it has the same complexity as previously known algorithms.
Cite as
Pawel Parys. Variants of Collapsible Pushdown Systems. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 500-515, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{parys:LIPIcs.CSL.2012.500,
author = {Parys, Pawel},
title = {{Variants of Collapsible Pushdown Systems}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {500--515},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.500},
URN = {urn:nbn:de:0030-drops-36937},
doi = {10.4230/LIPIcs.CSL.2012.500},
annote = {Keywords: collapsible pushdown systems, determinization, infinite hierarchy, shrink- ing lemma, reachability}
}
Document
A Proof of Kamp's theorem
Abstract
We provide a simple proof of Kamp's theorem.
Cite as
Alexander Rabinovich. A Proof of Kamp's theorem. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 516-527, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{rabinovich:LIPIcs.CSL.2012.516,
author = {Rabinovich, Alexander},
title = {{A Proof of Kamp's theorem}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {516--527},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.516},
URN = {urn:nbn:de:0030-drops-36945},
doi = {10.4230/LIPIcs.CSL.2012.516},
annote = {Keywords: Temporal Logic, Monadic Logic, Expressive Completeness}
}
Document
Commutative Data Automata
Abstract
Formalisms over infinite alphabets have recently received much focus in the community of theoretical computer science. Data automaton is a formal model for words over an infinite alphabet, that is, the product of a finite set of labels and an infinite set of data values, proposed by Bojanczyk, Muscholl, Schwentick et. al. in 2006.
A data automaton consists of two parts, a nondeterministic letter-to-letter transducer, and a class condition specified by a finite automaton, which acts as a condition on each subword of the outputs of the transducer in corresponding to a maximal set of positions with the same data value.
It is open whether the nonemptiness of data automata can be decided with elementary complexity, since this problem is equivalent to the reachability of petri nets. Very recently, a restriction of data automata with elementary complexity, called weak data automata, was proposed by Kara, Schwentick and Tan and its nonemptiness problem was shown to be in 2NEXPTIME.
In weak data automata, the class conditions are specified by some simple constraints on the number of occurrences of labels occurring in every class. The aim of this paper is to demonstrate that the commutativity of class conditions is the genuine reason accounting for the elementary complexity of weak data automata.
For this purpose, we define and investigate commutative data automata, which are data automata with class conditions restricted to commutative regular languages. We show that while the expressive power of commutative data automata is strictly stronger than that of weak data automata, the nonemptiness problem of this model can still be decided with elementary complexity, more precisely, in 3NEXPTIME. In addition, we extend the results to data omega-words and prove that the nonemptiness of commutative Büchi data automata can be decided in 4NEXPTIME. We also provide logical characterizations for commutative (Büchi) data automata, similar to those for weak (Büchi) data automata.
Cite as
Zhilin Wu. Commutative Data Automata. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 528-542, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{wu:LIPIcs.CSL.2012.528,
author = {Wu, Zhilin},
title = {{Commutative Data Automata}},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
pages = {528--542},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-42-2},
ISSN = {1868-8969},
year = {2012},
volume = {16},
editor = {C\'{e}gielski, Patrick and Durand, Arnaud},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.528},
URN = {urn:nbn:de:0030-drops-36953},
doi = {10.4230/LIPIcs.CSL.2012.528},
annote = {Keywords: Data Automata, Commutative regular languages, Presburger arithmetic, Existential Monadic Second-order logic, B\"{u}chi automata}
}