|
Читайте также: |
Сколемизация – замена каждой переменной, связанной квантором существования (
), функцией нескольких или всех имеющихся в предложении переменных, которые возвращают соответствующую константу. Для выражения:
(
Х) ( У) МАТЬ (Х,У)
поскольку значение У под зависит от значения Х, то У можно заменить сколемовской функцией f ' (x), тогда получим Х МАТЬ (x, f ‘ (x)).
Сколемизация – это процесс, который также позволяет связать переменные, стоящие под квантором всеобщности с константами. После удаления из логической БД переменных связанных квантором существования можно применить унификацию и привести предложение в форму необходимую для применения таких правил вывода как модус поненс.
1. modus ponens Согласно этому правилу, если предложение P->Q, то можно вывести Q (может быть применено к переменным).
2. modus tollens P->Q, если Q – ложно, то предложение позволяет вывести 
Р.
3. исключение «И» Позволяет вывести истинность обоих конъюнктов на основе истинности конъюнктивного предложения. P и Q – истинны => P^Q – истина.
4. универсальное инстанциирование Если любую переменную, стоящую под квантором всеобщности в истинном предложении, заменить любым соответствующим термином из области определения, то результирующее выражение истинно. Т.о. если А принадлежит той же области определения, что и Х, и ( Х),Р(Х), то можно вывести Р(А).
Дата добавления: 2015-07-10; просмотров: 138 | Нарушение авторских прав