Prover9 - это автоматическое средство доказательства теорем для логики первого порядка и эквациональной логики, разработанное Уильямом МакКьюном .
Описание [ править ]
Prover9 является преемником средства доказательства теорем Otter, также разработанного Уильямом МакКьюном . [1] : 1 Prover9 известен тем, что дает относительно удобочитаемые доказательства и имеет мощную стратегию подсказок. [1] : 11
Prover9 намеренно объединен с Mace4 , который ищет конечные модели и контрпримеры. Оба могут быть запущены одновременно с одного и того же входа, [2] при этом Prover9 пытается найти доказательство, в то время как Mace4 пытается найти (опровергающий) контрпример. Prover9, Mace4 и многие другие инструменты построены на базовой библиотеке LADR («Библиотека для автоматизированного исследования дедукции»), чтобы упростить реализацию. Полученные доказательства могут быть перепроверены Ivy, инструментом проверки правок, который был отдельно проверен с помощью ACL2 .
В июле 2006 года язык ввода LADR / Prover9 / Mace4 претерпел серьезные изменения (что также отличает его от Otter). Ключевое различие между «предложениями» и «формулами» полностью исчезло; «формулы» теперь могут иметь свободные переменные ; и «пункты» теперь являются подмножеством «формул». Prover9 / Mace4 также поддерживает формулу «целевого» типа, которая автоматически отменяется для доказательства. Prover9 пытается автоматически сгенерировать доказательство по умолчанию; Напротив, автоматический режим Otter должен быть явно установлен.
Prover9 находился в стадии активной разработки, с выпуском новых выпусков каждый месяц или раз в два месяца до 2009 года. Prover9 - это бесплатное программное обеспечение и, следовательно, программное обеспечение с открытым исходным кодом ; он выпущен под лицензией GPL версии 2 или новее.
Примеры [ править ]
Сократ [ править ]
Традиционные утверждения «все люди смертны», «Сократ - человек», доказательство «Сократ смертен» могут быть выражены таким образом в Prover9:
формулы (предположения). человек (х) -> смертный (х). % открытая формула со свободной переменной x человек (сократ).end_of_list.
формулы (цели). смертный (сократ).end_of_list.
Это будет автоматически преобразовано в форму клауза (которую также принимает Prover9):
формулы (СОС). -человек (х) | смертный (х). человек (сократ). -смертный (сократ).end_of_list.
Квадратный корень из 2 иррационально [ править ]
Доказательство иррациональности квадратного корня из 2 можно выразить так: [3]
формулы (предположения). 1 * х = х. % личность х * у = у * х. % коммутативности х * (у * г) = (х * у) * г. % ассоциативности (x * y = x * z) -> y = z. % отмены (0 не допускается, поэтому x! = 0). % % Теперь давайте определим divides (x, y): x делит y. % Пример: divides (2,6) истинно, потому что 2 * 3 = 6. % делит (x, y) <-> (существует zx * z = y). делит (2, x * x) -> делит (2, x). % Если 2 делит x * x, оно делит x. а * а = 2 * (б * б). % a / b = sqrt (2), поэтому a ^ 2 = 2 * b ^ 2. (x! = 1) -> - (делит (x, a) & делит (x, b)). % a / b находится в самых низких сроках 2! = 1.% Оригинальный автор чуть не забыл об этом.end_of_list.
Ссылки [ править ]
- ^ a b Филлипс, JD; Становский, Давид. "Автоматизированное доказательство теорем в теории петель" (PDF) . Карлов университет . Архивировано 28 марта 2018 года (PDF) . Проверено 15 ноября 2018 года .
- ^ Бергаммер, Рудольф; Штрут, Георг (21 июня 2010 г.). «Об автоматизированном построении и верификации программ» (PDF) . В Болдаке, Клод; Дешарне, Жюль; Ктари, Бечир (ред.). Математика построения программ, Труды . 10-я Международная конференция, MPC 2010. Квебек . DOI : 10.1007 / 978-3-642-13321-3 . ISBN 978-3-642-13320-6. Архивировано 19 ноября 2018 года (PDF) . Проверено 19 ноября 2018 . CS1 maint: обескураженный параметр ( ссылка )
- ^ Уиллер, Дэвид А. "sqrt2.in" . Персональная домашняя страница Дэвида А. Уиллера . Проверено 14 марта +2016 . CS1 maint: обескураженный параметр ( ссылка )
Внешние ссылки [ править ]
- Домашняя страница Prover9
- Prover9 - Mace4 - форум LADR
- Формальные методы (квадратный корень из 2 примеров)
