Задание 1. Логика высказываний
Согласно варианту (см. табл. 1):
· составить таблицу истинности, столбцы которой включают: пропозициональные переменные, посылки по отдельности, заключение, конъюнкцию всех посылок, импликацию заключения из этой конъюнкции,
· выделить штриховкой строки, в которых истинны все посылки и заключение,
· указать необходимые значения пропозициональных переменных для истинных значений всех посылок и заключения;
· доказать истинность заключения:
а) методом дедукции и нарисовать граф дедуктивного вывода,
b) методом резолюции и нарисовать граф вывода пустой резольвенты.
Таблица 1
| Вариант | Формула |
| (A ® B), (C ® D), (B ®Ø D), (A &Ø D) |¾ (Ø C & B) | |
| (B ®(A ® C)), (B ® A), Ø C &Ø D |¾ Ø(B Ú D) | |
| (B ® A), (B ®(Ø A Ú C)), (Ø С ÚØ D) |¾ (Ø B ÚØ D) | |
| (A ® B), (C ® B), (B ® D), Ø D |¾ (Ø A &Ø C) | |
| (A ® B), (A ®(B ® C)), (B ® C), Ø C |¾ (Ø A &Ø B) | |
| (A ® B), (C ® D), (B ®Ø D), C |¾ (Ø A & D) | |
| (A «B), (B ®(A ® C)),Ø C |¾ (Ø A &Ø B) | |
| (A ® B), (D ® C), Ø B, Ø C |¾ Ø(A Ú D) | |
| (A ® B), (C ®Ø B), (C &Ø D) |¾ Ø (A Ú D) | |
| (A ® B), (Ø B Ú C), (A ® C), (A Ú B Ú D), Ø B |¾ (C Ú D) | |
| (A ® B), (D ® C), Ø(B Ú C) |¾ (Ø A &Ø D) | |
| (A ® B), (C ®Ø B), (D ® C), D |¾ Ø A | |
| (A ® B), (B & D ® C), (A & D) |¾ C | |
| (A ® B), (C ® B), (Ø B Ú D), Ø(D Ú C) |¾ (Ø A &Ø C) | |
| (A ® B), (A ®(B ® C)), (A & D) |¾ C | |
| (A ® B), (C ® B), (D ®(A Ú C)), D |¾ B | |
| (A ® B), (C ® D), (B ®Ø D), (C &Ø D) |¾ (Ø A &Ø D) | |
| (A ® B), (A ®(B ® C)), Ø(C Ú D) |¾ (Ø A &Ø D) | |
| (A ® B), (B ® C), (C ® D), A & B |¾ B & D | |
| (A ®(B ® C)), (A ® B), Ø(C Ú D) |¾ (Ø A &Ø D) | |
| (A ®(B ® C)), (Ø D Ú A), B |¾ (Ø D Ú C) | |
| (A ®(B ® C)), (Ø D Ú A), B, D |¾ C | |
| (A ®(B ® C)), (A ® B), A & D |¾ C & D | |
| (A ®(B ® C)), (Ø D Ú A), B |¾ (Ø D Ú C) | |
| (A ®(B ® C)), (Ø D Ú A), B |¾ (D ® C) | |
| (A ®(B ® C)), ((A ® C)® D), Ø D |¾ Ø B | |
| (A ® B), (B ® C), (C ® D), (A Ú C) |¾ (C Ú D) | |
| (B ® A), (B ®(A ® C)), B & D |¾ C | |
| (B ® A), (B ®(A ® C)), Ø(C Ú D) |¾ Ø(B Ú D) | |
| (B ® A), (B ®(Ø A Ú C)), (B & D) |¾ C & D | |
| (B ® A), (A ® C), (D ® C), (B Ú D) |¾ (C Ú D) | |
| (B ®(A ® C)), (B ® A), (C ® D), Ø D |¾ Ø B | |
| (A ®(B ® C)), (Ø D Ú A), B |¾ (D Ú C) | |
| (B ® (A ® C)), (B ® A), Ø C ÚØ D |¾ Ø(B & D) | |
| (Ø A Ú B), (C ÚØ B), (Ø С &Ø D) |¾ Ø(A Ú D) | |
| (Ø A ÚØ B), (C ® A), (B ÚØ D) |¾ (Ø C ÚØ D) | |
| (Ø A Ú B), (C ÚØ B), (A Ú D), Ø D |¾ C | |
| (Ø A ÚØ B), (C ® A), B & D |¾ ØC ® D | |
| (A Ú B), (A ® C), (B ® D),Ø C |¾ D | |
| (Ø A Ú B), (C ®Ø B), Ø(C ® B) |¾ (Ø A &Ø B) | |
| (A ® B), (C ® D), (B ®Ø D), (A &Ø D) |¾ (Ø C & B) | |
| (A ® B), (C ® B), (B ® D), Ø D |¾ (Ø A &Ø C) | |
| (A ® B), (D ® C), Ø B, Ø C |¾ Ø(A Ú D) | |
| (A ® B), (C ®Ø B), (D ® C), D |¾ Ø A | |
| (A ® B), (C ® B), (D ®(A Ú C)), D |¾ B | |
| (A ®(B ® C)), (A ® B), Ø(C Ú D) |¾ (Ø A &Ø D) | |
| (A ®(B ® C)), (Ø D Ú A), B |¾ (Ø D Ú C) | |
| (B ® A), (B ®(A ® C)), B & D |¾ C | |
| (B ®(A ® C)), (B ® A), (C ® D), Ø D |¾ Ø B | |
| (Ø A ÚØ B), (C ® A), (B ÚØ D) |¾ (Ø C ÚØ D) |
Задание 2. Логика предикатов
Согласно варианту (см. табл. 2):
· преобразовать формулу к виду ПНФ, затем - ССФ,
· сформировать множество дизъюнктов К,
· выполнить унификацию дизъюнктов множества К.
Таблица 2
| Вариант | Формула |
| " x (A (x)® B (y))&" y (A (x)®(B (y)® C (z)))®$ z (C (z)) | |
| " x (B (x)®$ z (A (z)))&$ y (A (z)® C (y))®(Ø C (y)& B (x)) | |
| " x (A (x)®$ y (B (y)))®$ y (Ø A (x)ÚØ C (z)Ú B (y)) | |
| " x (A (x)®$ z (C (z)))&" y (C (z)® B (y))®(A (x)® B (y)) | |
| " x (A (x)®$ y (B (y)® C (z)))®" z (A (x)& B (y)® C (z)) | |
| " x (A (x)® B (z))&" y (C (y)® A (x))®$ z (C (y)® B (z)) | |
| " x ((A (x)® B (y))®" y (C (y)Ú A (x)))®(C (y)Ú$ y (B (y))) | |
| " x (A (x)® B (y))&" y (A (x)®(B (y)® C (z)))®(A(x)®$ z (C (z))) | |
| " x (A (x)® B (y))&(A (x)®" y (B (y)® C (z)))®$ z (C (z)) | |
| " x (A (x)®$ z (B (y)® C (z)))®" y (B (y)®(A (x)® C (z))) | |
| (" x (A (x))®$ z (B (z)))®" z ((B (x)® C (z))® C (z)) | |
| ($ x (Ø A (x))®" z (Ø B (z)))®(Ø B (x)Ú A (x)) | |
| (" x (A (x))®" y (B (y)))®$ y (C (y)& A (x)® C (y)& B (x)) | |
| " x (Ø A (x)®$ y (B (y)))®(Ø B (y)® A (x)) | |
| " x (Ø A (x)®$ y (Ø B (y)))®(B (y)® A (x)) | |
| " x (A (x)® B (x))&$ y (B (x)® C (y))®$ z (C (y)® D (z)) | |
| " x (A (x)® B (x))&" z (C (z)® A (x))®$ y (C (z)® B (y)) | |
| " x (B (x)®" y (A (y)))&" y (B (y)®(A (x)® C (z)))®$z(C(z)) | |
| (" x (A (x)® B (y)))&(A (x)®" y (B (y)® C (z)))®$ z (C (z)) | |
| " x (A (x)® B (x))®(" y (C (y)® A (x))®$ z (C (z)® B (x))) | |
| " x (B (x)® A (y))&(B (x)®" y (A (y)® C (z)))®$ z (C (z)) | |
| ($ x (A (x)® B (z))®$ y (C (y)Ú A (x)))®" z (C (y)Ú B (z)) | |
| (" x (B (x))®$ y (A (y)))&(A (y)®$ y (C (y)))®(Ø A (x)Ú C (y)) | |
| ((" x (A (x))®$ x (B (x)))®$ y (A (x)Ú C (y)))®(B (x)Ú C (y)) | |
| $ x (A (x)®" y (B (y)))&(Ø A (x)®" y (B (y)))® B (y) | |
| " x (A (x)®$ y (B (y)))&(Ø A (x)® B (x))® B (x) | |
| ($ x (B (x))®" y (A (y)))&(Ø B (x)® A (y))® A (z) | |
| (" x (B (x))®$ z (C (z)))®(A (y)& B (x)® A (y)& C (z)) | |
| $ x (A (x)® B (y))®" y " z ((C (z)® A (x))®(C (z)® B (y))) | |
| (" x (A (x))®$ z (C (z)))&" y (C (z)® B (y))®(A (x)® B (y)) | |
| (" x (A (x))®$ y (B (y)))&" y (C (y)®$ x (D (x)))®(A (x)& C (y)) | |
| " x (A (x)® B (y))&(A (x)®" y (B (y)® C (z)))®$ z (C (z)) | |
| ($ x (A (x)® B (z))®$ y (C (y)Ú A (x)))®" z (C (y)Ú B (z)) | |
| " x (A (x)® B (y))&" z (C (z)® A (x))®$ y (C (z)® B (y)) | |
| (" x (A (x)®$ z (B (z)))®$ y (A (x)Ú C (y)))®(B (z)Ú C (y)) | |
| " x (B (x)®" y (A (y)))&" y (B (x)®(A (y)® C (z))) | |
| " x (A (x)® B (x))®" y ((C (y)® A (x))®(C(y)®B(x))) | |
| (" x (A (x))®$ z (C (z)))&" y (C (z)® B (y))®(A (x)® B (y)) | |
| " x (A (x)®$ y (B (y)))&(Ø A (x)® B (x))® B (x) | |
| (" x (B (x))®$ y (A (y)))&(A (y)®$ y (C (y)))®(Ø A (x)Ú C (y)) | |
| " x (B (x)® A (y))&(B (x)®" y (A (y)® C (z)))®$ z (C (z)) | |
| " x (B (x)®" y (A (y)))&" y (B (y)®(A (x)® C (z)))®$z(C(z)) | |
| " x (A (x)® B (x))&$ y (B (x)® C (y))®$ z (C (y)® D (z)) | |
| " x (Ø A (x)®$ y (B (y)))®(Ø B (y)® A (x)) | |
| ($ x (Ø A (x))®" z (Ø B (z)))®(Ø B (x)Ú A (x)) | |
| " x (A (x)®$ z (B (y)® C (z)))®" y (B (y)®(A (x)® C (z))) | |
| " x (A (x)® B (y))&" y (A (x)®(B (y)® C (z)))®(A(x)®$ z (C (z))) | |
| " x (A (x)® B (z))&" y (C (y)® A (x))®$ z (C (y)® B (z)) | |
| " x (A (x)®$ y (B (y)))®$ y (Ø A (x)ÚØ C (z)Ú B (y)) | |
| " x (A (x)® B (y))&" y (A (x)®(B (y)® C (z)))®$ z (C (z)) |