NQTHM
NQTHM это средство автоматического доказательства теорем, которое иногда называют средством доказательства теорем Бойера — Мура. Он был предшественником ACL2[англ.][1].
История[править | править код]
Система была разработана Робертом С. Бойером[англ.] и Дж. Стротером Муром[англ.], профессорами информатики в Техасском университете, Остин . Они начали работу над системой в 1971 году в Эдинбурге, Шотландия . Их целью было создание полностью автоматического средства доказательства теорем, основанного на логике. В качестве рабочей логики они использовали вариант Pure LISP. Программа автоматического доказательства теорем Бойера-Мура применялась и дорабатывалась в течение многих лет.
Определения[править | править код]
Определения сформированы как полностью рекурсивные функции, система широко использует перезапись[англ.]* и индукционную эвристику, которая используется когда переписывание, и что-то, что они называют символической оценкой, терпит неудачу. Система была построена на основе 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) Теорема Гёделя о неполноте (Натарджан Шанкар[англ.])
- (1988) Стек CLI (Билл Бевьер, Уоррен Хант, Мэтт Кауфманн, Дж. Мур, Билл Янг)
- (1990) Закон квадратичной взаимности Гаусса (Дэвид Руссинофф)
- (1992) Византийские генералы и синхронизация часов (Бевье и Янг)
- (1992) Компилятор для подмножества языка Nqthm (Артур Флэтэу)
- (1993) Протокол асинхронной связи двухфазной метки
- (1993) Motorola MC68020 и Библиотека строк Berkeley C (Юань Юи)
- (1994) Теорема Пэрис – Харрингтона Рамси (Кеннет Кунен)
- (1996) Эквивалентность NFSA и DFSA
PC-NQTHM[править | править код]
Более мощная версия под названием PC-NQTHM(Proof-checker NQTHM) была разработана Мэттом Кауфманном[англ.] . Это предоставило пользователю инструменты доказательства, которые система использует автоматически, так что можно дать больше указаний по доказательству. Это очень помогает, поскольку система имеет непродуктивную тенденцию блуждать по бесконечным цепочкам индуктивных доказательств.
Литература[править | править код]
- Математическая логика и автоматическое доказательство теорем, Чень Ч. и Ли Р. , 1983.
- Справочник по вычислительной логике, Р.С. Бойер и Дж. С. Мур, Academic Press (2-е издание), 1997.
- Инструмент доказательства теорем Бойера-Мура и его интерактивное усовершенствование, с М. Кауфманном и Р.С. Бойером, «Компьютеры и математика с приложениями», 29 (2 ), 1995, стр. 27–62.
Награды[править | править код]
В 2005 году Роберт С. Бойер[англ.] , Мэтт Кауфманн[англ.] и Дж. Стротер Мур[англ.] получил награду ACM Software System Award[англ.] за свою работу над средством доказательства теорем NQTHM[3].
Примечания[править | править код]
- ↑ "Nqthm, the Boyer-Moore prover". (англ.). Дата обращения: 12 октября 2021. Архивировано 28 октября 2021 года.
- ↑ Hunt jr., Warren A. (1986), FM8501: A Verified Microprocessor, Technical Report, 47, University of Texas at Austin
- ↑ Association for Computing Machinery, "ACM: Press Release, March 15, 2006", campus.acm.org, accessed December 27, 2007.
Внешние ссылки[править | править код]
- The Automated Reasoning System, Nqthm Архивная копия от 17 февраля 2020 на Wayback Machine
- The Boyer-Moore Theorem Prover (NQTHM) Архивная копия от 28 октября 2021 на Wayback Machine
- Несмотря на то, что система больше не поддерживается, она по-прежнему доступна по адресу [1]
- Версия для запуска на GitHub: [https://web.archive.org/web/20211026232105/https://github.com/John-Nagle/nqthm Архивная копия от 26 октября 2021 на Wayback Machine [2]]