а ( міркувати, щоб програмувати , іздат (дюно, 1986)).
-> немає
? - Начальник (Еміль, генрі). p align="justify"> -> немає
? - Ідет_дождь (зараз)
-> немає
Так як в Пролозі немає оголошення й контролю типів, то немає і помилок програмування. Невірно написане користувачем ім'я для системи є новим атомів: анрі і генрі - два атоми, які не мають нічого спільного. Бінарне відношення не годиться в якості тернарного, зате тернарного ставлення задає три бінарних відносини з однаковими іменами - для трьох пар з трьох аргументів: відносини книга (_, _) і книга (_, _, _) для системи різні, чим і обумовлений відповідь на другий наведений вище питання.
17. Системи прямої дедукції. Системи зворотного дедукції
Системи прямої дедукції
У системах прямий дедукції нові знання отримують, застосовуючи висновки до фактів і правилам. Алгоритм завершує роботу при отриманні деякого знання, еквівалентного мети (або безпосередньо тягне її). Для ілюстрації системи прямої дедукції звернемося знову до попереднього прикладу. Доведемо теорему
(Факт (1) Факт (2) Правило (1)) Мета (1).
В· Етап (1):
Перетворимо Факт (1) і Правило (1)) в диз'юнктів, щоб застосувати потім метод резолюцій. За допомогою резолюції виводимо нове правило (2), використовуючи позначення
Факт (1) Правило (1)
Правило (2)
Факт (1): Правило (1):
Проф (Інфо, Жак_2)
Правило (2):
В· Етап (2): з Факту (2) та Правила (2) резолюцією виводимо новий
Факт (3):
Факт (2): Правило (2)
Студ (Мат, Марі_4)
Факт (3): іспит (Жак_2, Марі_4) Рівно (Інфо, Мат) = Л
(Відношення Рівно (Інфо, Мат) = Л має бути явно вказано у БД)
В· Етап (3):
Факт (3) відповідає Цілі (1). Отже, вона підтверджена. Аналогічно виведемо твердження Л з Факту (3) і заперечення Цілі (1):
Факт (3): Мета (1):
іспиту (Жак_2, Марі_4) іспит (Жак_2, Марі_4)
Систему прямої дедукції можна трактувати як систему, в якій застосовується теорема про прямий дедукції: Якщо F1, F2, ..., Fn, G - логічні вираження, то G є логічним наслідком з F1, F2, ..., Fn тоді і тільки тоді , коли логічний вираз (F1 ... FnG) тотожно хибно, тобто нездійсненно. Правила виводу і стратегії, що використовуються в системах прямий дедукції, графічно представимо І/АБО - деревами. p> Системи зворотного дедукції
У системах зворотного дедукції висновки застосовують до мети й до правил, щоб побудувати нові часткові цілі. Алгоритм завершує роботу, коли всі часткові цілі відповідають фактам. Таку систему можна тлумачити з логічної точки зору як систему, в якій застосовується теорема про зворотній дедукції, яка говорить: Якщо F1, F2, ..., Fn, G - логічні вираження, то G є логічним наслідком з F1, F2, ..., Fn тоді і тільки тоді, коли логічний вираз (тотожне істинно, тобто загальнозначуще.
У системах зворотного дедукції правила і цілі перетворять в Кон'юнктів, щоб застосувати потім правило згоди
В· Етап (1): з Цілі (1) і заперечення Правила (1), використовуючи правило згоди, виводимо нову Мета (2):
Мета (1) Правило (1)
іспиту (Жак_2. Марі_4)
Мета (2):
В· Етап (2): з Цілі (2) і заперечення Факту (1), за допомогою правила згоди, виводимо Мета (3):
Мета (2): Факт (1):
Проф (Інфо, Жак_2)
Мета (3):
Студ (z, Марі_4) Рівно (Інфо, z)
В· Етап (3): з Цілі (3) і заперечення Факту (2) виводимо теорему:
Мета (3): Факт (2):
Студ (z, Марі_4) Рівно (Інфо, z) Студ (Мат, Марі_4)
Рівно (Інфо, Мат) = І
18. Мова Prolog. Кон'юнкція. Змінні
Кон'юнкція
У логічних формулах використовують зв'язки і прості предикати. Те ж саме має місце і в Пролозі. Саму ходову в'язку - кон'юнкцію - позначають коми:
? - Начальник (Еміль, Анрі), начальник (Жозева, анрі). p align="justify"> Це вираз відповідає такий логічної формулою
Начальник (Еміль, Анрі) Начальник (Жозева, Анрі).
Кон'юнкція в Пролозі, як і в логіці, істинна тільки при істинності всіх компонент. Проте є важлива відмінність: у Пролозі семантика враховує п...
