Нктм

Nqthm — средство доказательства теорем, которое иногда называют средством доказательства теорем Бойера-Мура . Это был предшественник ACL2 . ^[1]

История

Система была разработана Робертом С. Бойером и Дж. Стротером Муром , профессорами информатики Техасского университета в Остине . Они начали работу над системой в 1971 году в Эдинбурге , Шотландия . Их целью было создать полностью автоматическое устройство для доказательства теорем, основанное на логике. они использовали вариант Pure LISP В качестве рабочей логики .

Определения

Определения формируются как полностью рекурсивные функции , система широко использует переписывание и эвристику индукции , которая используется при переписывании, и то, что они назвали символической оценкой, терпит неудачу.

Система была построена на основе Lisp и имела некоторые базовые знания о так называемом «нулевом уровне» — состоянии машины после ее загрузки в реализацию Common Lisp.

Это пример доказательства простой арифметической теоремы. Функция ТАЙМС является частью BOOT-STRAP (называемый «спутником») и определяется как

 (DEFN TIMES (X Y)
  (IF (ZEROP X)
      0
      (PLUS Y (TIMES (SUB1 X) Y))))

Формулировка теоремы

Формулировка теоремы также дана в синтаксисе, подобном Lisp:

 (prove-lemma commutativity-of-times (rewrite)
   (equal (times x z) (times z x)))

Если теорема окажется верной, она будет добавлена в базу знаний системы и может использоваться в качестве правила перезаписи для будущих доказательств.

Само доказательство дается в форме квазиестественного языка. Авторы случайным образом выбирают типичные математические фразы для включения шагов в математическое доказательство, что на самом деле делает доказательства вполне читабельными. Существуют макросы для LaTeX , способные преобразовать структуру Лиспа в более или менее читаемый математический язык.

Доказательство коммутативности времен продолжается:

 Give the conjecture the name *1.
 We will appeal to induction.  Two inductions are suggested by terms in the conjecture, 
 both of which are flawed.  We limit our consideration to the two suggested by the 
 largest number of nonprimitive recursive functions in the conjecture.  Since both of 
 these are equally likely, we will choose arbitrarily.  We will induct according to 
 the following scheme:
       (AND (IMPLIES (ZEROP X) (p X Z))
          (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Z))
                   (p X Z))).
 Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
 us that the measure (COUNT X) decreases according to the well-founded relation
 LESSP in each induction step of the scheme.  The above induction scheme
 produces the following two new conjectures:
 Case 2. (IMPLIES (ZEROP X)
                  (EQUAL (TIMES X Z) (TIMES Z X))).

и, проведя ряд индукционных доказательств, наконец приходит к выводу, что

Case 1. (IMPLIES (AND (NOT (ZEROP Z))
                      (EQUAL 0 (TIMES (SUB1 Z) 0)))
                 (EQUAL 0 (TIMES Z 0))).
This simplifies, expanding the definitions of ZEROP, TIMES, PLUS, and EQUAL, to:
     T.
That finishes the proof of *1.1, which also finishes the proof of *1.
Q.E.D.
[ 0.0 1.2 0.5 ]
COMMUTATIVITY-OF-TIMES

Доказательства

С помощью системы было проведено или подтверждено множество доказательств, в частности

(1971) объединение списков
(1973) сортировка вставками
(1974) двоичный сумматор
(1976) компилятор выражений для стековой машины
(1978) уникальность простых факторизаций
(1983) обратимость алгоритма шифрования RSA.
(1984) неразрешимость проблемы остановки для Pure Lisp
(1985) Микропроцессор FM8501 (Уоррен Хант) ^[2]
(1986) Теорема Гёделя о неполноте (Шанкар)
(1988) CLI Stack (Билл Бевьер, Уоррен Хант, Мэтт Кауфманн, Дж. Мур, Билл Янг)
(1990) Закон квадратичной взаимности Гаусса (Дэвид Руссинофф)
(1992) Византийские генералы и синхронизация часов (Бевьер и Янг)
(1992) Компилятор подмножества языка Nqthm (Артур Флатау)
(1993) Протокол асинхронной связи с двухфазной меткой
(1993) Motorola MC68020 и библиотека струн C Беркли (Юань Юй)
(1994) Теорема Пэрис-Харрингтона Рэмси ( Кеннет Кунен )
(1996) Эквивалентность NFSA и DFSA ( Дебора Вебер-Вульф )

ПК-Nqthm

Более мощная версия, получившая название PC-Nqthm (Proof-checker Nqthm), была разработана Мэттом Кауфманном . Это предоставило пользователю инструменты доказательства, которые система использует автоматически, так что можно дать больше указаний по доказательству. Это очень помогает, поскольку система имеет непродуктивную тенденцию блуждать по бесконечным цепочкам индуктивных доказательств.

Литература

Справочник по вычислительной логике, Р. С. Бойер и Дж. С. Мур, Academic Press (2-е издание), 1997.
Средство доказательства теорем Бойера-Мура и его интерактивное расширение, совместно с М. Кауфманом и Р. С. Бойером, Компьютеры и математика с приложениями, 29 (2), 1995, стр. 27–62.

Награды

В 2005 году Роберт С. Бойер , Мэтт Кауфманн и Дж. Стротер Мур получили премию ACM Software System Award за работу над средством доказательства теорем Nqthm. ^[3]

Ссылки

^ «Нктм, испытатель Бойера-Мура» .
^ Хант-младший, Уоррен А. (1986), FM8501: проверенный микропроцессор , технический отчет, том. 47 лет, Техасский университет в Остине {{citation}}: CS1 maint: отсутствует местоположение издателя ( ссылка )
^ Ассоциация вычислительной техники , «ACM: Пресс-релиз, 15 марта 2006 г.» , Campus.acm.org , по состоянию на 27 декабря 2007 г. ( английская версия ).

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

Автоматизированная система рассуждений, Nqthm
Средство доказательства теорем Бойера-Мура (NQTHM)
Несмотря на то, что система больше не поддерживается, она все еще доступна по адресу [1].
Запускаемая версия на GitHub : [2]

[1] «Нктм, испытатель Бойера-Мура» .

[2] Хант-младший, Уоррен А. (1986), FM8501: проверенный микропроцессор , технический отчет, том. 47 лет, Техасский университет в Остине {{citation}}: CS1 maint: отсутствует местоположение издателя ( ссылка )

[acmaward-3] Ассоциация вычислительной техники , «ACM: Пресс-релиз, 15 марта 2006 г.» , Campus.acm.org , по состоянию на 27 декабря 2007 г. ( английская версия ).

[1]

[2]

[3]