Эффективный алгоритм определения истинности утверждений о действительных числах в сигнатуре отношений порядка
Коварцев А.Н.

Аннотация:
В статье предлагается новый эффективный алгоритм определения истинности утверждений о действительных числах в сигнатуре отношений порядка. В отличие от известного алгоритма А. Тарского, предложенный алгоритм сводит переборную задачу проверки истинности любого утверждения о вещественных числах к оптимизационной задаче. В новой версии алгоритма могут использоваться не только алгебраические, но и трансцендентные функции.

Ключевые слова :
разрешимость предиката, теорема Тарского, замкнутая формула, доказательство истинности, глобальная оптимизация, сложность алгоритмов.

Литература:

  1. Коварцев, А.Н. Автоматизация разработки и тестирования программных средств / А.Н. Коварцев. – Самара: Самарский государственный аэрокосмический университет, 1999. – 150 с.
  2. Верещагин, Н.К. Языки и исчисления / Н.К. Верещагин, А. Шень. – М.: МЦНМО, 2012. – 240 с.
  3. Матиясевич, Ю.В. Алгоритм Тарского / Ю.В. Матия­севич // Компьютерные инструменты в образовании. – 2008. – № 6. – С. 4-14.
  4. Коварцев, А.Н. К вопросу об эффективности параллельных алгоритмов глобальной оптимизации функций многих переменных / А.Н. Коварцев, Д.А. Попова-Коварцева // Компьютерная оптика. – 2011. – Т. 35, № 2. – С. 256-261.
  5. Мостовой, Я.А. Имитационная математическая модель внешней среды в жизненном цикле бортового программного обеспечения управления космической платформой / Я.А. Мостовой // Компьютерная оптика. – 2012. – Т. 36, № 3. – С. 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) 332-56-22, Fax: +7 (846) 332-56-20