Русская Википедия:NQTHM

Материал из Онлайн справочника
Перейти к навигацииПерейти к поиску

NQTHM это средство автоматического доказательства теорем, которое иногда называют средством доказательства теорем Бойера — Мура. Он был предшественником Шаблон:Не переведено 5[1].

История

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

Определения

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

Это пример доказательства простой арифметической теоремы. Функция TIMES является частью 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 существуют макросы, которые могут преобразовать структуру Lisp в более или менее читаемый математический язык.

Дайте гипотезе имя *1.
Обратимся к индукции. Термины гипотезы предполагают две индукции, обе ошибочны.
Мы ограничиваем наше рассмотрение двумя, предложенными наибольшим числом непримитивных 
рекурсивных функций в гипотезе. Поскольку оба варианта одинаково вероятны, мы выберем произвольно.
Мы будем проводить индукцию по следующей схеме: 
       (AND (IMPLIES (ZEROP X) (p X Z))
          (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Z))
                   (p X Z))).
Линейная арифметика, лемма COUNT-NUMBERP и определение ZEROP сообщают нам, что мера (COUNT X) убывает 
согласно хорошо обоснованному отношению LESSP на каждом шаге индукции схемы.Приведенная выше схема индукции 
приводит к следующим двум новым гипотезам:
Случай 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))).
Это упрощает, расширяя определения ZEROP, TIMES, PLUS и EQUAL до: 
        T.
Это завершает доказательство * 1.1, которое также завершает доказательство * 1.
Q.E.D.
[ 0.0 1.2 0.5 ]
COMMUTATIVITY-OF-TIMES

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

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

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

PC-NQTHM

Более мощная версия под названием PC-NQTHM(Proof-checker NQTHM) была разработана Шаблон:Не переведено 5 . Это предоставило пользователю инструменты доказательства, которые система использует автоматически, так что можно дать больше указаний по доказательству. Это очень помогает, поскольку система имеет непродуктивную тенденцию блуждать по бесконечным цепочкам индуктивных доказательств.

Литература

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

Награды

В 2005 году Шаблон:Не переведено 5 , Шаблон:Не переведено 5 и Шаблон:Не переведено 5 получил награду Шаблон:Не переведено 5 за свою работу над средством доказательства теорем NQTHM[3].

Примечания

Шаблон:Примечания

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


Партнерские ресурсы
Криптовалюты
Магазины
Хостинг
Разное

  1. ↑ Шаблон:Cite web
  2. ↑ Hunt jr., Warren A. (1986), FM8501: A Verified Microprocessor, Technical Report, 47, University of Texas at Austin
  3. ↑ Association for Computing Machinery, "ACM: Press Release, March 15, 2006", campus.acm.org, accessed December 27, 2007.
Источник — http://wikihandbk.com/ruwiki/index.php?title=Русская_Википедия:NQTHM&oldid=8750005