Cтраница 1
Переписывающие системы впервые были использованы Кнутом и Бендиксом [23] для решения проблемы тождества слов в эквациональных теориях. Для того чтобы процесс редукций в конце концов завершался, мы должны потребовать, чтобы терм г был нередуцируемым. [1]
Нетерова переписывающая система является конфлюэнтной ( и, стало быть, канонической) тогда и только тогда, когда не существует дивергентной критической пары для правил этой системы. [2]
Произвольная переписывающая система, вообще говоря, канонической не является, так как правила позволяют использовать равенства только в одном направлении. [3]
Определение 1.1. Пусть имеются переписывающая система R и два правила 1 - г и / 2 [ ] - г2 из R, причем и - не переменная. [4]
Мы получим теперь каноническую переписывающую систему для булевой алгебры, образовав сначала каноническую систему для булева кольца. [5]
Легко видеть, что если R - каноническая переписывающая система, то каждый терм имеет относительно R единственную нередуцируемую форму. Поэтому для проверки истинности равенства s Et нужно только привести s и / к их нередуцируемым формам и посмотреть, совпадают ли они. [6]
Когда происходит авост ( либо в процедуре пополнения Кнута - Бендикса, либо в ЯЫ - стратегии с неполной переписывающей системой), ситуация полностью меняется, поскольку само понятие переписывающих правил, по-видимому, больше неприменимо. [7]
Здесь следует сделать одно замечание, касающееся свойства нетеровости. Когда к переписывающей системе добавляются новые правила, должно изменяться также и упорядочение термов. Поэтому в ходе выполнения КМ - стратегии может возникнуть необходимость постоянно регулировать это упорядочение. В RN-стратегии это делать не обязательно, потому что авосты в ней никогда не случаются. [8]
Хотя во многих случаях для теории существует каноническая система, обратная ситуация также может иметь место. Поэтому требование наличия канонической переписывающей системы для данной теории представляется довольно сильным. Как было уже упомянуто, если процедура пополнения Кнута - Бендикса не дает канонической системы для эквациональной теории, то происходит это вследствие двух причин: зацикливания, когда алгоритм порождает бесконечно много правил, или авоста, когда он порождает критическую пару с несравнимыми термами. В данном разделе мы приведем стратегию для случая зацикливания, а случай авоста обсудим позднее. [9]
В данной статье мы предлагаем новый подход к доказательству теорем логики первого порядка, основанный на методе переписывающих правил для термов. Сначала рассматривается пропозициональное исчисление и вводится каноническая переписывающая система для булевой алгебры. Эта система позволяет преобразовать исчисление предикатов первого порядка в некоторую форму эквациональной логики и разработать для теорий первого порядка несколько полных стратегий ( работающих как с дизъюнктами, так и с формулами более общего вида), основанных на процедуре пополнения Кнута - Бендикса. Что более важно, наши стратегии могут единообразно и эффективно работать с логикой предикатов и встроенными ( эквациональными) теориями. Мы описываем также реализацию этих стратегий и сравниваем их с некоторыми другими методами доказательства теорем первого порядка. [10]