Диссертация (1149226), страница 18
Текст из файла (страница 18)
Например, применив правилок секвенции номер 2, можновывести следующую секвенцию:2*..Боковая формула этого применения правилаимеет вид,поэтому данный случай попадает в число исключений, когда нельзя применятьстратегию упрощения. Предположим теперь, что это исключение отсутствует.Тогда сразу же после порождения секвенции 2 ее можно упростить, заменивсеквенцией 2*. Однако секвенция 2* не может участвовать в выводе формулычастности, эта секвенция принадлежит множеству(ви может быть105удалена по стратегии УСНФ), а к секвенции 1 нельзя применить никакое другоеправило, кроме уже примененного правила.Этот пример показывает, что стратегия упрощения не будет полной дляисчисления(как и для исчисления), если разрешить ее применение вовсех случаях, когда боковой формулой применения правилаявляется формула вида,,иилииз спискаявляется одним из правил,,.Пример 3.2. Рассмотрим следующую формулу:Эта формула взята из задачи SYN408+1 из библиотеки ILTP версии 1.1.2[144].
Построим ее вывод в исчисленииподформулывподформулы— отрицательным.. Заметим, что вхождение атомарнойявляется положительным, а вхождение атомарнойПосхемеаксиомполучаемединственную с точностью до переименования переменных аксиому:1..В секвенции 1— это новая переменная. К данной секвенции применимастратегия упрощения по правилу. Поэтому заменим секвенцию 1заключением применения этого правила (получим новую секвенцию номер 1):1..Эту секвенцию можно дальше упростить с применением правила1.:.Дальнейшие упрощения секвенции 1 невозможны.
Применим к этойсеквенции правило:2..Поскольку формулавходит в списокне содержит отрицательных вхождений , то правилодля исчислениясеквенции 2 стоит формула с главным символом. Но так как в сукцеденте, то эту секвенцию мы не106можем упростить с применениемправилу67. Поэтому получаем новую секвенцию по. Ограничение на собственную переменную в данном случаевыполняется: переменнаяне входит свободно в заключение.3..Полученную секвенцию уже можно упростить с применением3.:.Завершим доказательство, применив правилоподстановкойк секвенции 3 (с):4..Запишем полученный вывод формулы в виде дерева (в данном примере«дерево» состоит из одной ветви), содержащего «укрупненные» примененияправил, в соответствии со стратегией упрощения.Заметим, что кроме секвенций 1–4 мы могли бы ввести и некоторые другиесеквенции.
Например, применив к (упрощенной) секвенции 1 правилосдругой боковой формулой, можно получить следующую секвенцию:Однако эта секвенция не может участвовать в выводе формулыДействительно, эта секвенция принадлежит множеству., и по стратегииУСНФ ее можно удалить.67Вообще говоря, в данном случае такое упрощение допустимо, так как ни одна секвенция, выводимая изсеквенции 2, не может содержать вхождение формулыусловие в стратегии упрощения, чтобы учесть такие случаи.в антецедент. Можно видоизменить соответствующее107Пример 3.3. Покажем, что если формуласодержит отрицательныевхождения символа , то не всегда можно «упрощать» секвенции с применениемправила. Рассмотрим следующую формулу:Вывод этой формулы в исчислении(с применением стратегииупрощения) выглядит следующим образом:В применении правилаподстановокправилаив качестве наибольшего общего унификаторавзята подстановка.
В применениинаибольший общий унификатор. В обоих случаяхнеявно применяется правило нормализации, чтобы удалить лишние переменные вподстановках, возникающие после унификации.Правилоне входит в списокдля исчисления(формуласодержит отрицательное вхождение ), поэтому упрощения с этим правилом неприменяются. Если мы все же применим такое упрощение, то правая посылкаприменения правилабудет выглядеть так:этом к левой посылке правилособственнуюпеременную.Тогда.
Приприменять нельзя из-за ограничения наприменениеправилаизменитсяследующим образом (с учетом неявной нормализации):Обозначим заключение как . Видно, что теперь кнеприменимо правилоиз-за того, что эта секвенция содержит две формулы в сукцеденте. Болеетого,принадлежит множествунее уже нельзя вывести формулу ., поэтому согласно стратегии УСНФ из108Заметим также, что в исходном выводе формулыправила сокращения (обозначим это заключение как(обозначим ее какзаключение применения) поглощает его посылку). Поэтому можно применить к секвенциитривиального сокращения: сразу заменить ее секвенциейсэкономить на применении правиластратегиюи таким образом. Если бы к секвенциибылиприменимы другие правила вывода, кроме правила сокращения, то стратегиятривиального сокращения также позволила бы устранить соответствующиеизбыточные ветви дерева поиска вывода.В случае применения сингулярной стратегии вывод формулыодносукцедентном исчисленииприменение правилавыглядит так же, как и вывод взаменяется применением правилав, только:а применение правила сокращения удаляется.В следующих двух примерах мы рассмотрим две схожие по виду формулы:и.
Обе формулы (достаточнохорошо известные среди логиков) выводимы в классическом исчислениипредикатов, но в интуиционистском исчислении предикатов первая из нихвыводима, а вторая — нет.Пример 3.4. Рассмотрим следующую формулу:Эта формула выводима в интуиционистском исчислении предикатов.Построим ее вывод в исчислении. По схеме аксиомполучаемединственную с точностью до переименования переменных аксиому:1..В секвенции 1— это новая переменная. Применим к этой секвенциистратегию упрощения по правилув сукцеденте переменную, после чего переименуем возникающуюс помощью подстановкии применимправило нормализации, чтобы устранить лишние элементы в подстановках:1091..Так какне содержит отрицательных вхождений символавходит в списокдля исчисления, то правило.
Поэтому можно далее упроститьсеквенцию 1 с применением правила. Действительно, ограничение насобственную переменную выполняется:не входит свободно в заключение.После упрощения по правилуправиламивыполним дальнейшие упрощения по. В результате получим следующую секвенцию:1..Применим к полученной секвенции правиловозникающую в сукцеденте переменную, затем переименуемс помощью подстановки(также неявно применяется правило нормализации):2..Упростим секвенцию 2 по правилами,, а затем применимстратегию тривиального сокращения двух одинаковых формул в антецеденте:2..Осталось завершить доказательство, применив3.к секвенции 2:.Пример 3.5.
Рассмотрим следующую формулу:Эта формула невыводима в интуиционистском исчислении предикатов.Действительно, единственная (с точностью до переименования переменных)аксиома исчисленияпосле упрощения по правилувыглядит так:1..К этой секвенции нельзя применить правилособственнуюпеременную.Поэтомуксеквенциииз-за ограничения на1применимотолько110правило(используем унификатор, а к результатуприменяем неявную нормализацию):2..Секвенция 2 принадлежит множествузависима от переменной. При этом всеквенции 2, вместо переменныхпеременнойи. Действительно, переменная–формуле, входящей в сукцедентвыполняется подстановка одной и той же(т.
е. имеет место). Значит, в соответствии со стратегиейУСНП секвенцию 2 можно удалить. В данном случае даже без применениястратегии УСНП можно заметить, что из секвенции 2 нельзя вывести формулу ,потому что к этой секвенции неприменимы никакие правила вывода. Такимобразом, мы убедились, что формуланевыводима в исчислении.3.11.
ЗаключениеВ этой главе были рассмотрены следующие стратегии поиска вывода,применимые к исчислениямпоглощения,стратегияи их модификациям: стратегия,упрощения,стратегииудалениясеквенцийснедопустимыми подстановками и формулами (сокращенно УСНП и УСНФсоответственно), стратегия тривиального сокращения и сингулярная стратегия.Стратегияпоглощенияявляетсястандартной.Стратегииупрощения,тривиального сокращения и стратегия УСНП могут рассматриваться какадаптированные для исчисленийпредложенныхС. Ю.
Масловым,иварианты существующих стратегий,В. П. Оревковым,А. А. ВоронковымиТ. Тамметом для других исчислений обратного метода. Адаптация для каждойстратегии индивидуальна, например, в стратегии упрощения используетсяспецифический список «упрощающих» правил. В отличие от статьиА. А. Воронкова [157], полнота стратегии упрощения обосновывается с помощьютеоремы о перестановочности применений правил вывода. Новую стратегиюУСНФ можно рассматривать как обобщение стратегии «nesting strategy»111Т.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
