Исчисление суперпозиции
Исчисление суперпозиции — это исчисление для рассуждений в эквациональной логике . Он был разработан в начале 1990-х годов и сочетает в себе концепции разрешения первого порядка с обработкой равенства на основе порядка, разработанные в контексте (безошибочного) завершения Кнута – Бендикса . Его можно рассматривать как обобщение либо разрешения (до эквациональной логики), либо неизменного завершения (до полной клаузальной логики ). Как и большинство исчислений первого порядка , суперпозиция пытается показать невыполнимость набора предложений первого порядка , т.е. она выполняет доказательства путем опровержения . Суперпозиция — это полное опровержение: при наличии неограниченных ресурсов и справедливой стратегии вывода из любого невыполнимого набора предложений в конечном итоге будет получено противоречие.
Многие (современные) средства доказательства теорем для логики первого порядка основаны на суперпозиции (например, средство доказательства эквациональной теоремы E ), хотя лишь немногие реализуют чистое исчисление.
Реализации
[ редактировать ]Ссылки
[ редактировать ]- Доказательство теоремы уравнений на основе перезаписи с выбором и упрощением , Лео Бахмайр и Харальд Ганцингер , Журнал логики и вычислений 3 (4), 1994.
- Доказательство теорем на основе парамодуляции , Роберт Ньювенхейс и Альберто Рубио, Справочник по автоматизированному рассуждению I (7), Elsevier Science и MIT Press , 2001.
 | Эта математической логике статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее . |