На этом этапе обрабатываются случаи применения отрицания к формулам, не являющимся атомарными. Если такой случай имеет место, то формула переписывается по соответствующим правилам. Так, например, формула
~(человек (цезарь)&существующий (цезарь))
преобразуется в
~человек(цезарь) # существующий (цезарь)
а
~аll(Х, человек (X))
преобразуется в
exists(Х,~человек(Х))
Преобразования, выполняемые на втором этапе, основаны на следующих фактах:
~(α&β) значит то же самое, что и (~α) # (~β)
~exists(ν,ρ) значит то же самое, что и all(ν,~ρ)
~all(ν,ρ) значит то же самое, что и exists(ν,~ρ)
После завершения второго этапа каждое вхождение отрицания в формулу будет относиться лишь к атомарным подформулам. Атомарная формула или ее отрицание называется литералом. На всех последующих этапах литералы обрабатываются как единый элемент, а то, какие литералы представлены отрицанием, будет существенным лишь в самом конце.
|
Главная
Каталог файлов
