Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 17 Issue 4, November 2016

Automated Verification of Equivalence Properties of Cryptographic Protocols
Rohit Chadha, Vincent Cheval, Ştefan Ciobâcă, Steve Kremer
Article No.: 23
DOI: 10.1145/2926715

Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality, and resistance against offline guessing attacks....

Index Problems for Game Automata
Alessandro Facchini, Filip Murlak, Michał Skrzypczak
Article No.: 24
DOI: 10.1145/2946800

For a given regular language of infinite trees, one can ask about the minimal number of priorities needed to recognize this language with a nondeterministic, alternating, or weak alternating parity automaton. These questions are known as,...

Where First-Order and Monadic Second-Order Logic Coincide
Michael Elberfeld, Martin Grohe, Till Tantau
Article No.: 25
DOI: 10.1145/2946799

We study on which classes of graphs first-order logic (fo) and monadic second-order logic (mso) have the same expressive power. We show that for all classes C of graphs that are closed under taking subgraphs, fo...

On the Proof Complexity of Paris-Harrington and Off-Diagonal Ramsey Tautologies
Lorenzo Carlucci, Nicola Galesi, Massimo Lauria
Article No.: 26
DOI: 10.1145/2946801

We study the proof complexity of Paris-Harrington’s Large Ramsey Theorem for bi-colorings of graphs and of off-diagonal Ramsey’s Theorem. For Paris-Harrington, we prove a non-trivial conditional lower bound in Resolution and a...

On Well-Founded Set-Inductions and Locally Monotone Operators
Bart Bogaerts, Joost Vennekens, Marc Denecker
Article No.: 27
DOI: 10.1145/2963096

In the past, compelling arguments in favour of the well-founded semantics for autoepistemic logic have been presented. In this article, we show that for certain classes of theories, this semantics fails to identify the unique intended model. We...

Taming Multirelations
Hitoshi Furusawa, Georg Struth
Article No.: 28
DOI: 10.1145/2964907

Binary multirelations generalise binary relations by associating elements of a set to its subsets. We study the structure and algebra of multirelations under the operations of union, intersection, sequential, and parallel composition, as well as...

The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory
Kristina Sojakova
Article No.: 29
DOI: 10.1145/2992783

Homotopy type theory is a new branch of mathematics that merges insights from abstract homotopy theory and higher category theory with those of logic and type theory. It allows us to represent a variety of mathematical objects as basic...

How Hard Is Positive Quantification?
Aleksy Schubert, Paweł Urzyczyn, Daria Walukiewicz-Chrząszcz
Article No.: 30
DOI: 10.1145/2981544

We show that the constructive predicate logic with positive (covariant) quantification is hard for doubly exponential universal time, that is, for the class co-2-Nexptime. Our approach is to represent proof-search as computation...

Two-Variable Logic with Counting and Trees
Witold Charatonik, Piotr Witkowski
Article No.: 31
DOI: 10.1145/2983622

We consider the two-variable logic with counting quantifiers (C2) interpreted over finite structures that contain two forests of ranked trees. This logic is strictly more expressive than standard C2 and it is no longer a...

Complexity of Two-Variable Logic on Finite Trees
Saguy Benaim, Michael Benedikt, Witold Charatonik, Emanuel Kieroński, Rastislav Lenhardt, Filip Mazowiecki, James Worrell
Article No.: 32
DOI: 10.1145/2996796

Verification of properties expressed in the two-variable fragment of first-order logic FO2 has been investigated in a number of contexts. The satisfiability problem for FO2 over arbitrary structures is known to be...