Atlas: Decidability Complexity of Quantifier-free Negationless Theory of Field of Rational Numbers by Nikolai Kossovski

Atlas home || Conferences | Abstracts | about Atlas

First St.Petersburg Days of Logic and Computability
May 26-29, 1999
Steklov Institute of Mathematics
St. Petersburg, Russia

Organizers
Evgeny Dantsin, Gennadii Davydov, Dima Grigoriev, Eduard Karavaev, Nickolai Kossovskii, Vladimir Lifschitz, Maurice Margenstern, Yuri Matiyasevich (chairman), Grigori Mints, Vladimir Orevkov, Anatol Slissenko, Maxim Vsemirnov

View Abstracts
Conference Homepage

Decidability Complexity of Quantifier-free Negationless Theory of Field of Rational Numbers
by
Nikolai Kossovski
Saint-Petersburg State University

DECIDABILITY COMPLEXITY OF QUANTIFIER-FREE

NEGATIONLESS THEORY OF FIELD 0F RATIONAL NUMBERS

N.K. Kossovski

Abstract

Any quantifier-free negationless theory of constructive objects coincides with the constructive one. Constructive mathematics is one of the main directions of investigations of N.A. Shanin and his disciples. Properties of constructive objects which have some continuous peculiarity are important to the mathematics in whole. Rational numbers may be regarded as such constructive objects.

The problem of decidability of an elementary theory of the field of rational numbers was formulated by A.I.Kokorin. Now we can not prove even decidability of a quantifier-free theory of the field of rational numbers. The following theorem establishes the decidability of a quantifier-free negationless theory of the field of rational numbers. Such a theory may be regarded as the simplest extension of the set of all identities which are nonstrict inequalities of polynomials under rational numbers.

Let negationless theory uses only conjunction and disjunction as logical connectives. Let T be a quantifier-free (universal) negationless elementary theory of signature <Q; |Q, |Pol, <= >, where Q - the set of all rational numbers, |Q - the list of all rational numbers, |Pol - the list of all polynomials with rational coefficients in which exponent of the polynomials and rational numbers are written in binary number system.

Theorem. Theory T is NP-hard and decidable by an algorithm which belongs to EXPTIME.

The signature of the theory T may be extended for example to <Q; |Q, |Pol, max, min, abs, <= >. In this case the assertion of the theorem is also true.

Such a theory may be interpretated as an extended fuzzy universal theory of field of rational numbers because we can use a-b as a fuzzy value of a <= b, conjunction as min and disjunction as max.

This result is a continuation of [1].

References

1. N.K.Kossovski, A.V.Tishkov. Mathematical reasoning for fuzzy propositions. // Proc. International Conference on Informatics and Control, v.2, St.-Petersburg. 1997. P. 522-529.

Date received: March 11, 1999