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