Can prolog be used to determine invalid inference?

Question

If I have two premises as follows:

1. a -> c (a implies c)
2. b -> c (b implies c)

and a derived conclusion:

3. a -> b (a therefore implies b),

then the conclusion can be shown to be invalid because:

a -> c is valid for statement #1 when a is true and c is true, and b -> c is valid for statement #2 when b is false and c is true. This leads to a -> b when a is true and b is false, a direct contradiction of statement #3.

Or, per proof with a truth table that contains a line for where the premises are true but the conclusion is false:

Truth Table with true premises and false conclusion

My question is: "Is there a way to use prolog to show that the assertions of statements #1 and #2 contradict the conclusion of statement #3? If so, what is a clear and concise way to do so?"

Answer 1

You could use library(clpb):

Firstly assign to a variable Expr your expression:

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

Note that:

• '+' stands for logical OR

• '*' for logical AND

• '~' for logical NOT Also A->B is equivalent with A+(~B). So the above expression is equivalent with ((A->C),(B->C))-> (A->C) where we wrote '->' using +,~ and ',' with *.

Now if we query:

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

Predicate taut/2 takes as input an clpb Expression and returns T=1 if it tautology, T=0 if expression cannot be satisfied and fails in any other case. So the fact that the above query failed means that Expr was nor a tautology neither could not be satisfied, it meant that it could be satisfied.

Also by querying:

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

Predicate sat/1 returns True iff the Boolean expression is satisfiable and gives the answer that the above Expression is satisfiable when:

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

where '#' is the exclusive OR which means that your expression (we know from taut/2 that is satisfiable) is satisfied when 1#C#C*B is satisfied.

Another solution without using libraries could be:

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

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

Example:

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

Also if I understood correctly from your comment, to collect all possible solutions you could write:

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

Which gives a list of lists, where the inner lists have the form [true,true,true] in the above example which means a solution is A=true,B=true,C=true and in the above case it has only one solution.

To find all contradictions you could write:

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

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

last line could also been written as:

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

Example:

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

Answer 2

@coder has already given a very good answer, using clpb constraints.

I would like to show a slightly different way to show that the conclusion does not follow from the premises, also using CLP(B).

The main difference is that I post individual sat/1 constraints for each of the premises, and then use taut/2 to see whether the conclusion follows from the premises.

The first premise is:

a → c

In CLP(B), you can express this as:

sat(A =< C)

The second premise, i.e., b → c, becomes:

sat(B =< C)

If the a → b followed from these premises, then taut/2 would succeed with T = 1 in:

?- sat(A =< C), sat(B =< C), taut(A =< B, T).
false.

Since it doesn't, we know that the conclusion does not follow from the premises.

We can ask CLP(B) to show a counterexample, i.e., an assignment of truth values to variables where a → c and b → c both hold, and a → b does not hold:

?- sat(A =< C), sat(B =< C), sat(~(A =< B)).
A = C, C = 1,
B = 0.

Simply posting the constraints suffices to show the unique counterexample that exists in this case. If the counterexample were not unique, we could use labeling/1 to produce ground instances, for example: labeling([A,B,C]).

For comparison, consider for example:

?- sat(A =< B), sat(B =< C), taut(A =< C, T).
T = 1,
sat(A=:=A*B),
sat(B=:=B*C).

This shows that a → c follows from a → b ∧ b → c.