Nqthm - Nqthm

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

История

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

Определения

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

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

Это пример доказательства простой арифметической теоремы. Функция TIMES является частью BOOT-STRAP (называемой "спутником") и определена как 

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

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

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

 (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 (Уоррен Хант)
  • (1986) Теорема Гёделя о неполноте (Шанкар)
  • (1988) Стек CLI (Билл Бевьер, Уоррен Хант, Мэтт Кауфманн, Дж. Мур, Билл Янг)
  • (1990) Закон квадратичной взаимности Гаусса (Дэвид Руссинофф)
  • (1992) Византийские генералы и синхронизация часов (Бевье и Янг)
  • (1992) Компилятор для подмножества языка Nqthm (Артур Флэтэу)
  • (1993) протокол асинхронной связи двухфазной метки
  • (1993) Motorola MC68020 и Библиотека строк Berkeley C (Юань Ю)
  • (1994) Теорема Пэрис – Харрингтона Рэмси ( Кеннет Кунен )
  • (1996) Эквивалентность NFSA и DFSA ( Дебора Вебер-Вульф )

PC-Nqthm

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

Литература

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

Награды

Награда

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

использованная литература

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