Полезное:
Как сделать разговор полезным и приятным
Как сделать объемную звезду своими руками
Как сделать то, что делать не хочется?
Как сделать погремушку
Как сделать так чтобы женщины сами знакомились с вами
Как сделать идею коммерческой
Как сделать хорошую растяжку ног?
Как сделать наш разум здоровым?
Как сделать, чтобы люди обманывали меньше
Вопрос 4. Как сделать так, чтобы вас уважали и ценили?
Как сделать лучше себе и другим людям
Как сделать свидание интересным?
Категории:
АрхитектураАстрономияБиологияГеографияГеологияИнформатикаИскусствоИсторияКулинарияКультураМаркетингМатематикаМедицинаМенеджментОхрана трудаПравоПроизводствоПсихологияРелигияСоциологияСпортТехникаФизикаФилософияХимияЭкологияЭкономикаЭлектроника
|
Метод резолюций в логике предикатовМетод резолюции состоит в следующем. Пусть имеется два предложения С1=A1∨…∨Am∨D и C2=B1∨…∨Bn∨D, содержащих один и тот же атом D. Резольвентой предложений C1 и С2 является предложение С=A1∨…∨Am∨B1∨…∨Bn. Если литералы D и D' не равны, но существует унификатор, делающий их равными, то наиболее общий унификатор для D и D' применяется к предложениям C1 и С2, а затем вычисляется их резольвента. Если резольвента C пуста, то это указывает на невыполнимость исходной формулы. В случае нехорновских дизъюнктов метод резолюции необходимо дополнить правилом факторизации, применяемым для устранения повторяющихся литералов в одном предложении. Если литералы не равны, то также выполняется их унификация. Рассмотрим простой пример. Пусть брадобреи бреют всех людей, которые не бреются сами и не бреют тех, кто бреется сам. Тогда брадобреи не существуют. A1: ∀x Бб(x)⇒∀y(Б(y,y)⇒Б(x,y)) A2: ∀x Бб(x)⇒∀y(Б(y,y)⇒Б(x,y)) B: ∃x Бб(x) После перевода в сколемовскую конъюнктивную нормальную форму получаем предложения: C1: Бб(x)∨Б(y,y)∨Б(x,y) C2: Бб(x)∨Б(y,y)∨Б(x,y) C3: Бб(a) Применяя метод резолюции и правило факторизации, получаем предложения: C4: Бб(x)∨Б(x,x) факторизация C1 C5: Бб(x)∨Б(x,x) факторизация C2 C6: Б(a,a) резольвента C3 и C4 C7: Б(a,a) резольвента C3 и C5 С8: ⊥ резольвента C6 и C7 Исчисление предикатов. Язык и правила вывода исчисления предикатов. Чтобы построить новое исчисление, нам требуется указать 3 компонента: язык, аксиомы и правила вывода. Язык Добавим к языку исчисления высказываний новые конструкции с предикатами и получим язык исчисления предикатов. Вот расширенная грамматика: § <выражение>::= <импликация> § <импликация>::= <дизъюнкция> | <дизъюнкция> <импликация> § <дизъюнкция>::= <конъюнкция> | <дизъюнкция> <конъюнкция> § <конъюнкция>::= <терм> | <конъюнкция> & <терм> § <терм>::= <предикат> | <предикат> (<аргументы>) | <переменная><терм> | <переменная><терм> § <аргументы>::= <переменная> § <аргументы>::= <переменная>,<аргументы>
(a) индивидные переменные --- мы будем записывать их маленькими латинскими буквами из начала алфавита (b) предикаты (они обобщили пропозициональные переменные) (c) кванторы: всеобщности () и существования ().
|