Prover9 - Prover9
Prover9 - это автоматическое средство доказательства теорем для логики первого порядка и эквациональной логики, разработанное Уильямом МакКьюном .
Описание
Prover9 является преемником средства доказательства теорем Otter, также разработанного Уильямом МакКьюном . Prover9 известен тем, что дает относительно удобочитаемые доказательства и имеет мощную стратегию подсказок.
Prover9 намеренно объединен с Mace4 , который ищет конечные модели и контрпримеры. Оба могут быть запущены одновременно с одного и того же входа, при этом Prover9 пытается найти доказательство, а Mace4 пытается найти (опровергающий) контрпример. Prover9, Mace4 и многие другие инструменты построены на базовой библиотеке LADR («Библиотека для автоматизированного исследования дедукции»), чтобы упростить реализацию. Полученные доказательства могут быть перепроверены Ivy, инструментом проверки правок, который был отдельно проверен с помощью ACL2 .
В июле 2006 года язык ввода LADR / Prover9 / Mace4 претерпел серьезные изменения (что также отличает его от Otter). Ключевое различие между «предложениями» и «формулами» полностью исчезло; «формулы» теперь могут иметь свободные переменные ; и «пункты» теперь являются подмножеством «формул». Prover9 / Mace4 также поддерживает формулу «целевого» типа, которая автоматически отменяется для доказательства. Prover9 пытается автоматически сгенерировать доказательство по умолчанию; Напротив, автоматический режим Otter должен быть явно установлен.
Prover9 находился в стадии активной разработки, с выпуском новых выпусков каждый месяц или раз в два месяца до 2009 года. Prover9 - это бесплатное программное обеспечение и, следовательно, программное обеспечение с открытым исходным кодом ; он выпущен под лицензией GPL версии 2 или новее.
Примеры
Сократ
Традиционные выражения «все люди смертны», «Сократ - человек», доказательство того, что «Сократ смертен», можно выразить таким образом в Prover9:
formulas(assumptions). man(x) -> mortal(x). % open formula with free variable x man(socrates). end_of_list.
formulas(goals). mortal(socrates). end_of_list.
Это будет автоматически преобразовано в форму клауза (которую также принимает Prover9):
formulas(sos). -man(x) | mortal(x). man(socrates). -mortal(socrates). end_of_list.
Квадратный корень из 2 иррационально
Доказательство иррациональности квадратного корня из 2 можно выразить так:
formulas(assumptions).
1*x = x. % identity
x*y = y*x. % commutativity
x*(y*z) = (x*y)*z. % associativity
( x*y = x*z ) -> y = z. % cancellation (0 is not allowed, so x!=0).
%
% Now let's define divides(x,y): x divides y.
% Example: divides(2,6) is true because 2*3=6.
%
divides(x,y) <-> (exists z x*z = y).
divides(2,x*x) -> divides(2,x). % If 2 divides x*x, it divides x.
a*a = 2*(b*b). % a/b = sqrt(2), so a^2 = 2 * b^2.
(x != 1) -> -(divides(x,a) &
divides(x,b)). % a/b is in lowest terms
2 != 1. % Original author almost forgot this.
end_of_list.