Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

SPASS - это автоматическое средство доказательства теорем для логики первого порядка с равенством, разработанное в Институте информатики Макса Планка и использующее исчисление суперпозиции . Первоначально это название расшифровывалось как Synergetic Prover, увеличивающая суперпозицию с сортировками . Система доказательства теорем выпущена под лицензией FreeBSD . [1]

Расширение SPASS под названием SPASS-XDB добавило поддержку оперативного извлечения положительных аксиом единиц из внешних источников. [2] SPASS-XDB, таким образом, может включать факты, поступающие из реляционных баз данных , веб-сервисов или связанных серверов данных . Также была добавлена поддержка арифметики с использованием Mathematica . [3]

Ссылки [ править ]

  1. ^ "Max-Planck-Institut für Informatik - Автоматизация логики: Spass" . Spass-prover.org . 2010-05-28 . Проверено 10 августа 2016 . CS1 maint: обескураженный параметр ( ссылка )
  2. ^ "Спас-Xdb" . Cs.miami.edu . DOI : 10.1007 / 978-3-642-04617-9_36 . Проверено 10 августа 2016 . CS1 maint: обескураженный параметр ( ссылка )
  3. ↑ Дэвид Становский; Мартин Суда; Джефф Сатклифф. «SPASS-XDB становится математическим» (PDF) . Karlin.mff.cuni.cz . Проверено 10 августа 2016 . CS1 maint: обескураженный параметр ( ссылка )

Источники [ править ]

  • Вайденбах, Кристоф; Димова, Диляна; Фицке, Арно; Кумар, Рохит; Суда, Мартин; Вишневски, Патрик (2009), «SPASS Version 3.5», CADE-22: 22-я международная конференция по автоматизированному дедуктивному переводу , Springer, стр. 140–145..

Внешние ссылки [ править ]