Decidability of Weak Logics with Deterministic Transitive Closure

Prelegent(ci)

Filip Mazowiecki

Afiliacja

Uniwersytet Warszawski

Termin

25 czerwca 2014 14:15

Pokój

p. 5870

Tytuł w języku angielskim

joint work with Witold Charatonik and Emanuel Kieroński

Seminarium

Seminarium „Teoria automatów”

---

The deterministic transitive closure operator, added to languages containing even only two variables, allows to express many
natural properties of a binary relation, including being a linear
order, a tree, a forest or a partial function. This makes it a
potentially attractive ingredient of computer science formalisms. We consider the extension of the two-variable fragment of
first-order logic by the deterministic transitive closure of a
single binary relation, and prove that the satisfiability and finite
satisfiability problems for the obtained logic are decidable and
EXPSPACE-complete. We also consider the class
of universal first-order formulas in prenex form.

---