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
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....
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
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
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
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...
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
Article No.: 29
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...
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
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
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...