Nie jesteś zalogowany |
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
- 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.
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.
