Можно ли использовать пролог для определения неверного вывода?

Question

Если у меня есть две предпосылки следующим образом:

1. a -> c (a подразумевает c)
2. b -> c (b подразумевает c)

и вывод вывод:

3. a -> b (следовательно, a означает b),

тогда заключение может быть признано недействительным, потому что:

a -> c действительна для оператора #1, когда a истинно, а c верно, а b -> c действительна для оператора #2, когда b ложно и c верно. Это приводит к a -> b, когда a истинно, а b ложно, прямое противоречие утверждению № 3.

Или, для доказательства с таблицей истинности, которая содержит строку, где предпосылки верны, но вывод неверен:

Таблица правды с истинными предпосылками и ложным выводом

Мой вопрос: "Есть ли способ использовать пролог, чтобы показать, что утверждения утверждений № 1 и № 2 противоречат заключению утверждения № 3? Если да, то каков четкий и краткий способ сделать это?"

Answer 1

Вы можете использовать библиотеку (clpb):

Сначала присвойте переменной Expr ваше выражение:

Expr = ((A + ~C)*(B + ~C)+(~(A + ~B)),

Обратите внимание, что:

• "+" обозначает логическое ИЛИ

• '*' для логического И

• '~' для логического НЕ Также A->B эквивалентно A+(~B), Таким образом, приведенное выше выражение эквивалентно ((A->C),(B->C))-> (A->C) где мы написали '->' с помощью +,~ а также ',' с *,

Теперь, если мы запросим:

?-  use_module(library(clpb)).
true.
?- Expr=((A + ~C)*(B + ~C))+(~(A + ~B)),taut(Expr,T).
false.

Предикат taut/2 принимает в качестве входных данных выражение clpb и возвращает T=1, если он тавтологичен, T=0, если выражение не может быть выполнено и не выполняется в любом другом случае. Таким образом, тот факт, что вышеупомянутый запрос не удался, означает, что Expr не был ни тавтологией, ни не мог быть удовлетворен, это означало, что он мог быть удовлетворен.

Также путем запроса:

?- Expr=((A + ~C)*(B + ~C))+(~(A + ~B)),sat(Expr).
Expr = (A+ ~C)* (B+ ~C)+ ~ (A+ ~B),
sat(1#C#C*B),
sat(A=:=A).

сказуемое sat/1 возвращает True, если логическое выражение выполнимо и дает ответ, что приведенное выше выражение выполнимо, когда:

sat(1#C#C*B),
sat(A=:=A).

где '#' это exclusive OR это означает, что ваше выражение (мы знаем из тав / 2, что выполнимо) удовлетворяется, когда 1#C#C*B доволен.

Другое решение без использования библиотек может быть:

truth(X):-member(X,[true,false]).

test_truth(A,B,C):-
  truth(A),
  truth(B),
  truth(C),
  ((A->C),(B->C)->(A->C)).

Пример:

?- test_truth(A,B,C).
A = B, B = C, C = true ;
false.

Также, если я правильно понял из вашего комментария, чтобы собрать все возможные решения, вы можете написать:

?- findall([A,B,C],test_truth(A,B,C),L).
L = [[true, true, true]].

Что дает список списков, где внутренние списки имеют вид [true,true,true] в приведенном выше примере, что означает решение A=true,B=true,C=true и в приведенном выше случае он имеет только одно решение.

Чтобы найти все противоречия, вы можете написать:

 truth(X):-member(X,[true,false]).

    test_truth(A,B,C):-
      truth(A),
      truth(B),
      truth(C),
    not( (\+ ((\+A; C),(\+B ; C)) ; (\+A ; B)) ).

Последняя строка также может быть записана как:

not( ( (A->C;true),(B->C;true) ) -> (A->B;true) ;true ).

Пример:

  ?- findall([A,B,C],test_truth(A,B,C),L).
L = [[true, false, true]].

Answer 2

@coder уже дал очень хороший ответ, используя ограничения clpb.

Я хотел бы показать немного другой способ показать, что заключение не следует из помещения, также используя CLP(B).

Основное отличие заключается в том, что я размещаю индивидуальные sat/1 ограничения для каждого из помещений, а затем использовать taut/2 чтобы увидеть, следует ли заключение из помещения.

Первая предпосылка:

а → с

В CLP (B) вы можете выразить это как:

sat(A =< C)

Вторая предпосылка, т. Е. B → c, становится:

sat(B =< C)

Если a → b следовало из этих предпосылок, то taut/2 будет успешным с T = 1 в:

? - сб (A = ложь

Поскольку это не так, мы знаем, что заключение не следует из помещения.

Мы можем попросить CLP (B) показать контрпример, т. Е. Присваивать значения истинности переменным, где a → c и b → c оба имеют место, а a → b не имеет места:

? - сб (A = ~ (A = 
Достаточно просто опубликовать ограничения, чтобы показать уникальный контрпример, который существует в этом случае. Если бы контрпример не был уникальным, мы могли бы использовать labeling/1 производить наземные экземпляры, например: labeling([A,B,C]),
Для сравнения рассмотрим, например:
? - сб (A = Т = 1,
СБ (А =:=A*B),
СБ (В =: = В * С).
Это показывает, что a → c следует из a → b ∧ b → c.