Search ACM DL

Search Issue

enter search term and/or author name

**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 (

**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-N

**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 (C^{2}) interpreted over finite structures that contain two forests of ranked trees. This logic is strictly more expressive than standard C^{2} 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 FO^{2} has been investigated in a number of contexts. The satisfiability problem for FO^{2} over arbitrary structures is known to be...