Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

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

История [ править ]

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

Определения [ править ]

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

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

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

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

Формулировка теоремы [ править ]

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

 ( Докажите-лемму  коммутативность времен  ( перепишите )  ( равно  ( умножить на  x  z )  ( умножить на  z  x )))

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

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

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

 Дайте гипотезе имя * 1. Обратимся к индукции. Термины гипотезы предполагают две индукции: оба из них ошибочны. Мы ограничиваем наше рассмотрение двумя предложенными наибольшее количество непримитивных рекурсивных функций в гипотезе. Поскольку оба они одинаково вероятны, мы выберем произвольно. Мы будем проводить индукцию в соответствии с следующая схема: (И (ПОДРАЗУМЕВАЕТ (НУЛЬ X) (p XZ)) (ПОДРАЗУМЕВАЕТ (И (НЕ (НУЛЬ X)) (p (SUB1 X) Z)) (p XZ))). Линейная арифметика, лемма COUNT-NUMBERP и определение ZEROP информируют нам, что мера (COUNT X) убывает согласно хорошо обоснованному соотношению LESSP на каждом индукционном шаге схемы. Приведенная выше индукционная схема приводит к следующим двум новым предположениям: Случай 2. (Подразумевается (НУЛЬ X) (РАВНО (ВРЕМЯ XZ) (ВРЕМЯ ZX))).

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

Случай 1. (ПОДРАЗУМЕВАЕТСЯ (И (НЕ (НУЛЬ Z)) (РАВНО 0 (ВРЕМЯ (SUB1 Z) 0))) (РАВНО 0 (ВРЕМЯ Z 0))).Это упрощает, расширяя определения ZEROP, TIMES, PLUS и EQUAL до: Т.Это завершает доказательство * 1.1, которое также завершает доказательство * 1.QED[0,0 1,2 0,5]ВРЕМЕННАЯ КОММУТИВНОСТЬ

Доказательства [ править ]

Многие доказательства были сделаны или подтверждены системой, в частности

  • (1971) конкатенация списков
  • (1973) сортировка вставкой
  • (1974) двоичный сумматор
  • (1976) компилятор выражений для стековой машины
  • (1978) единственность простых факторизаций
  • (1983) обратимость алгоритма шифрования RSA
  • (1984) неразрешимость проблемы остановки для Pure Lisp
  • (1985) Микропроцессор FM8501 (Уоррен Хант) [2]
  • (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. [3]

Ссылки [ править ]

  1. ^ "Nqthm, испытатель Бойера-Мура" .
  2. ^ Хант младший, Уоррен А. (1986), FM8501: проверенный микропроцессор , технический отчет, 47 , Техасский университет в Остине
  3. ^ Ассоциация вычислительной техники , «ACM: пресс-релиз, 15 марта 2006 г.» [ постоянная мертвая ссылка ] , campus.acm.org , просмотрено 27 декабря 2007 г. ( английская версия ).

Внешние ссылки [ править ]

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