joint work with Witold Charatonik and Emanuel Kieroński

Speaker(s)

Filip Mazowiecki

Affiliation

Uniwersytet Warszawski

Date

June 25, 2014, 2:15 p.m.

Room

room 5870

Title in Polish

Decidability of Weak Logics with Deterministic Transitive Closure

Seminar

Seminar Automata Theory

---

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.

---