Архитектура Аудит Военная наука Иностранные языки Медицина Металлургия Метрология Образование Политология Производство Психология Стандартизация Технологии |
Перевірка сумісності сукупності тверджень шляхом побудови двійкової діаграми рішень
Перевіримо суперечність формули F=(A«ØB)Ù(BÚØC)Ù(ØA®ØC)Ù(AÚC) шляхом побудови приведеної упорядкованої двійкової діаграми рішень. Виберемо лінійний порядок на множині атомів, що входять у F. Нехай він буде таким: A<B<C. Розгалужуємо формулу F по А: F=AÞF1,F0, де F1=F[1/A], F0=F[0/A], тобто: F1=(1«ØB)Ù(BÚØC)Ù(Ø1®ØС)Ù(1ÚС), F0=(0«ØB)Ù(BÚØC)Ù(Ø0®ØС)Ù(0ÚС). Далі розгалужуємо формули F1 та F0 по В. F1=BÞF11, F10, де F11=F1[1/B], F10=F1[0/B], тобто: F11=(1«Ø1)Ù(1ÚØC)Ù(Ø1®ØС)Ù(1ÚС)=0Ù(1ÚØC)Ù(Ø1®ØС)Ù(1ÚС)=0, F10=(1«Ø0)Ù(0ÚØC)Ù(Ø1®ØС)Ù(1ÚС)=1Ù(0ÚØC)Ù(Ø1®ØС)Ù(1ÚС)= (0ÚØC)Ù(Ø1®ØС)Ù(1ÚС). F0=BÞF01, F00, де F01=F0[1/B], F00=F0[0/B], тобто: F01=(0«Ø1)Ù(1ÚØC)Ù(Ø0®ØС)Ù(0ÚС)=1Ù(1ÚØC)Ù(Ø0®ØС)Ù(0ÚС)= (1ÚØC)Ù(Ø0®ØС)Ù(0ÚС), F00=(0«Ø0)Ù(0ÚØC)Ù(Ø0®ØС)Ù(0ÚС)=0Ù(0ÚØC)Ù(Ø0®ØС)Ù(0ÚС)=0. Розгалужуємо формули F10 та F01 по С. F10=СÞF101, F100, де F101=F10[1/С], F100=F10[0/С], тобто: F101=(0ÚØ1)Ù(Ø1®Ø1)Ù(1Ú1)=(0Ú0)Ù(0®0)Ù(1Ú1)=0Ù(0®0)Ù(1Ú1)=0, F100=(0ÚØ0)Ù(Ø1®Ø0)Ù(1Ú0)=(0Ú1)Ù(0®1)Ù(1Ú0)=1Ù1Ù1=1. F01=СÞ F011, F010, де F011=F01[1/С], F010=F01[0/С], тобто: F011=(1ÚØ1)Ù(Ø0®Ø1)Ù(0Ú1)=1Ù(1®0)Ù1=1Ù0Ù1=0, F010=(1ÚØ0)Ù(Ø0®Ø0)Ù(0Ú0)=1Ù(1®1)Ù0=1Ù1Ù0=0. Усі розгалуження виконано; побудуємо упорядковану ДДР формули F (див. рис.6). Дана ДДР не є приведеною (бо містить надлишкову вершину F01). Вилучимо її (див. рис. 7). Тепер діаграма містить надлишкову вершину F0. Після приведення маємо ПУДДР (див. рис. 8).
Бачимо, що у приведеній ДДР є кінцева вершина, що має позначку «1», отже, формула F має моделі, тобто не є суперечною. Таким чином, можна зробити висновок, що подана сукупність тверджень є сумісною.
Контрольні питання 1. Як перевірити сумісність сукупності тверджень за допомогою таблиць істинності? 2. Як перевірити сумісність сукупності тверджень методом Девіса й Патнема? 3. Як перевірити сумісність сукупності тверджень методом резолюцій? 4. Як використати нормальні форми логіки висловлень для перевірки сумісності сукупності тверджень? |
Последнее изменение этой страницы: 2019-04-10; Просмотров: 232; Нарушение авторского права страницы