Samara State Aerospace University

PDF, 426 kB

Full text of article: Russian language.

DOI: 10.18287/0134-2452-2014-38-3-550-554

Pages: 550-554.

Abstract:
AIn this paper a new efficient algorithm is proposed for testing the truth of assertions for real numbers expressed in relational signatures. In contrast to the well known Tarski algorithm, the proposed algorithm reduces the search problem of checking the truth of any assertion for real numbers to the optimization problem. The new version of the algorithm can be used for algebraic and transcendental functions.

Key words:
predicate derivation, Tarski theorem, closed formula, the proof of the truth, global optimization, algorithm complexity.

References:

1. Kovartsev, A.N. Automating the development and testing of software / A.N. Kovartsev. – Samara: “SSAU” Publisher, 1999. – 150 p. – (In Russian).
2. Vereshchagin, N.K. Languages and calculus / N.K. Vereshchagin, A. Shen. – Moscow: “MCCME_PUBL”, – 2012. – 240 p. – (In Russian).
3. Matiyasevich, Y. Tarski algorithm / Y. Matiyasevich // Computer Tools in Education. – 2008. – Vol. 6. – P. 4-14. – (In Russian).
4. Kovartsev, A.N On efficiently of parallel algorithms for global optimization of functions of several variables / A.N. Kovartsev, D.A. Popova-Kovartseva // Computer Optics. – 2011. – Vol. 35(2). – P. 256-261. – (In Russian).
5. Mostovoi, J.A. Simulation mathematical model of the external ambience in life cycle of on-board software of management cosmic platform / J.A. Mostovoi // Computer Optics. – 2012. – V. 36(3). – P. 412-418.
6. Vazirani, Vijay V. Approximation Algorithms // Vijay V. Va­zirani. – Berlin: Springer, 2003. – 375 p.

   ---

   © 2009, IPSI RAS
   Institution of Russian Academy of Sciences, Image Processing Systems Institute of RAS, Russia, 443001, Samara, Molodogvardeyskaya Street 151; e-mail: ko@smr.ru; Phones: +7 (846 2) 332-56-22, Fax: +7 (846 2) 332-56-20