prologlogicboolean-logicclpb

Can prolog be used to determine invalid inference?

If I have two premises as follows:

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

and a derived conclusion:

  1. 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?"

Solution

  • You could use library(clpb):

    Firstly assign to a variable Expr your expression:

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

    Note that:

    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]].