Prover9

Prover9 — это автоматизированное средство доказательства теорем для логики первого порядка и эквациональной логики, разработанное Уильямом МакКьюном .

Описание

Prover9 является преемником средства доказательства теорем Оттера , также разработанного Уильямом МакКьюном . ^[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 могут быть выражены следующим образом:

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 иррационален , можно выразить следующим образом: ^[3]

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.

Ссылки

↑ Перейти обратно: Перейти обратно: ^а ^б Филлипс, доктор медицинских наук; Становский, Дэвид. «Автоматическое доказательство теорем в теории циклов» (PDF) . Карлов университет . Архивировано (PDF) из оригинала 28 марта 2018 года . Проверено 15 ноября 2018 г.
^ Бергаммер, Рудольф; Струт, Георг (21 июня 2010 г.). «Об автоматизированном построении и верификации программ» (PDF) . В Болдуке, Клод; Дешарне, Жюль; Ктари, Бечир (ред.). Математика построения программ: Труды . 10-я Международная конференция MPC 2010. Квебек . дои : 10.1007/978-3-642-13321-3 . ISBN 978-3-642-13320-6 . S2CID 6962311 . Архивировано из оригинала (PDF) 19 ноября 2018 года . Проверено 19 ноября 2018 г.
^ Уилер, Дэвид А. "sqrt2.in" . Персональная домашняя страница Дэвида А. Уиллера . Проверено 14 марта 2016 г.

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

[ATPLT-JDP-DS-1] Перейти обратно: Перейти обратно: ^а ^б Филлипс, доктор медицинских наук; Становский, Дэвид. «Автоматическое доказательство теорем в теории циклов» (PDF) . Карлов университет . Архивировано (PDF) из оригинала 28 марта 2018 года . Проверено 15 ноября 2018 г.

[RB-GS-2] Бергаммер, Рудольф; Струт, Георг (21 июня 2010 г.). «Об автоматизированном построении и верификации программ» (PDF) . В Болдуке, Клод; Дешарне, Жюль; Ктари, Бечир (ред.). Математика построения программ: Труды . 10-я Международная конференция MPC 2010. Квебек . дои : 10.1007/978-3-642-13321-3 . ISBN 978-3-642-13320-6 . S2CID 6962311 . Архивировано из оригинала (PDF) 19 ноября 2018 года . Проверено 19 ноября 2018 г.

[3] Уилер, Дэвид А. "sqrt2.in" . Персональная домашняя страница Дэвида А. Уиллера . Проверено 14 марта 2016 г.

[1]

[2]

[3]