Логика первого порядка на практике, как бороться с неразрешимостью?

Question

Я очень новичок в этих вещах. Надеюсь, это не очень наивный вопрос.

Я пробовал следующую формулу в Прологе: A ⇒ B

и учитывая, что B истинно, я оцениваю A, и он говорит ЛОЖЬ.

Мой вопрос почему ЛОЖЬ? (почему не ИСТИНА?) Учитывая текущую информацию, мы ничего не знаем о B. Работает ли Пролог исходя из предположения, что для чего-то неизвестного он выдает FALSE?

Если это предположение, насколько это распространено?

Еще одна вещь, которая приходит в голову, это то, что она находит назначение для соединения входного запроса и аксиом (в основном решение SAT). Поскольку полученный результат равен TRUE, независимо от того, какое значение имеет A, он просто выбирает один случайным образом (или ноль по умолчанию?).

Основываясь на свойствах логики 1-го порядка, она полуразрешима. если предложение A логически подразумевает предложение B, то это можно обнаружить, но не наоборот. Итак, как последний случай обрабатывается на практике, когда нет доказательств ИСТИНЫ?

PS1. Небольшое объяснение о том, как работает Пролог, также может быть полезным. Использует ли он SAT решатели в качестве черного ящика? Или жадные алгоритмы поиска?

Answer 1

Работает ли Пролог исходя из предположения, что для чего-то неизвестного он выдает FALSE?

Да, конечно. Такое поведение отражает предположение о закрытом мире (CWA) в том, что если факт явно не указан, он считается ложным.

Если это предположение, насколько это распространено?

Очень часто - большинство баз данных используют это предположение.

Это может помочь вам узнать о методе логического вывода Prolog: SLD Resolution.

Answer 2

Чтобы рассуждать о неопределенности в Прологе, вы можете написать интерпретатор для трехзначной логики. В этом интерпретаторе истинные значения true, false, а также unknown:

:- initialization(main).
main :-
    three_valued_logic(((true,false);unknown),Result),
    writeln(Result).

three_valued_logic(true,true).
three_valued_logic(false,false).
three_valued_logic(unknown,unknown).
three_valued_logic(not(A),false) :-
    three_valued_logic(A,true).
three_valued_logic(not(A),true) :-
    three_valued_logic(A,false).
three_valued_logic(not(A),unknown):-
    three_valued_logic(A,unknown).
three_valued_logic((A,B),true) :-
    three_valued_logic([A,B],[A1,B1]),
    (A1==true;B1==true).
three_valued_logic((A,B),false) :-
    three_valued_logic([A,B],[A1,B1]),
    (A1==false;B1==false).
three_valued_logic((A,B),unknown) :-
    three_valued_logic([A,B],[A1,B1]),
    (A1==unknown;B1==unknown).
three_valued_logic((A;B),unknown) :-
    three_valued_logic([A,B],[A1,B1]),
    (A1==unknown;B1==unknown),(A1==false;B1==false).
three_valued_logic((A;B),false) :-
    three_valued_logic([A,B],[A1,B1]),
    (A1==false,B1==false).
three_valued_logic((A;B),true) :-
    three_valued_logic([A,B],[A1,B1]),
    (A1==true;B1==true).
three_valued_logic([],[]).
three_valued_logic([A|B],[A1|B1]) :-
    three_valued_logic(A,A1),three_valued_logic(B,B1).

В этом примере истинное значение ((true,false);unknown) является unknown, в то время как (false,unknown) является false,

Answer 3

Чистый Пролог не использует предположение о замкнутом мире. Поэтому, если вы получите ответ "ложь" или "нет", это означает, что НЕ ПРОИЗВОДИМ. Или написано символически:

Значение "ложь" или "нет" в чистом прологе:

~ (Database |- Query)              (i)

Это не значит, что отрицание запроса является выводимым. Поэтому ответ "ложь" или "нет" не означает символически:

Неправильное значение "ложь" или "нет" в чистом прологе:

Database |- ~Query                 (ii)

Есть некоторые операторы, такие как отрицание как сбой (+)/1, которые позволяют интерпретатору Пролога переходить от (i) к (ii). Но это уже не чистый Пролог, и под капотом, например, (+) / 1 могут быть реализованы нелогичные операторы, такие как вырезать (!).

Да, разрез (!) Больше не является чистым Прологом и не является декларативным. Например, отрицание как сбой (+)/1, реализовано следующим образом:

\+ X  :- X, !, fail.
\+ _.

Отрицание как неудача имеет такие проблемы, как смещение значения в зависимости от того, созданы ли аргументы или нет. Существуют и другие способы добавления отрицательных знаний в программы Prolog, но они не встречаются в обычных интерпретаторах Prolog, поскольку они более сложны, чем подход cut (!).

до свидания