ВЕСЕЛЬЕ

SPASS — это автоматизированное средство доказательства теорем для логики первого порядка с равенством, разработанное в Институте компьютерных наук Макса Планка и использующее исчисление суперпозиции . Первоначально это название означало Synergetic Prover Augmenting Superposition with Sorts . Система доказательства теорем распространяется под лицензией FreeBSD . ^{[ 1 ]}

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

Ссылки

^ «Институт компьютерных наук Макса Планка — автоматизация логики: развлечение» . Fun-prover.org . 28 мая 2010 г. Проверено 10 августа 2016 г.
^ «Спасс-Xdb» . Cs.miami.edu . дои : 10.1007/978-3-642-04617-9_36 . Проверено 10 августа 2016 г.
^ Дэвид Становский; Мартин Суда; Джефф Сатклифф. «SPASS-XDB становится математическим» (PDF) . Карлин.mff.cuni.cz . Проверено 10 августа 2016 г.

Источники

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

Внешние ссылки

Официальный сайт

[1] «Институт компьютерных наук Макса Планка — автоматизация логики: развлечение» . Fun-prover.org . 28 мая 2010 г. Проверено 10 августа 2016 г.

[2] «Спасс-Xdb» . Cs.miami.edu . дои : 10.1007/978-3-642-04617-9_36 . Проверено 10 августа 2016 г.

[3] Дэвид Становский; Мартин Суда; Джефф Сатклифф. «SPASS-XDB становится математическим» (PDF) . Карлин.mff.cuni.cz . Проверено 10 августа 2016 г.

[ 1 ]

[ 2 ]

[ 3 ]