This article is cited in 2 papers

Theoretical Foundations of Computer Science

The Use Of The Transitive Closure Operator On Formulas With A Single Successor Function And Divisibility Predicates

A. S. Zolotov

Tver State University

Abstract: We investigate transitive closure operator on formulas with successor function and divisibility predicates. We prove that transitive closure operator on two or more pairs of vaiables makes theory undecidable. We build equivalent analog without transitive closure operator for fomulas containing only transitive closure operator on one pair of variables.

Keywords: decidability, transitive closure.

UDC: 510.652

Received: 10.02.2013
Revised: 15.02.2013