Search code examples
prologlogical-operators

Find parameter values that satsify logical formula in Prolog


I have a fact base of a single logical formula, e.g.

check(A,B) :- A,B.

I can query check(true,true). or check(true,false). and the compiler will give correct results. But I would like to also make queries where some parameters are variables, to obtain all values of those variables that make the query true. E.g., I'd like to query check(X,Y). and obtain X=true, Y=true., or check(X,true) and obtain X=true. However, I can't get it to work even for this trivial case, nor find the solution anywhere. All queries with variables return Arguments are not sufficiently instantiated.

I've also tried findall(X,check(true,X),Solution). and various variants using bagof or setof.


Solution

  • check_both(X, Y) :-
        check_single(X),
        check_single(Y).
    
    check_single(true) :- !.
    check_single(X) :- call(X).
    

    Results in swi-prolog:

    ?- check_both(X, Y).
    X = Y, Y = true.
    
    ?- X=1, check_both(X=1, Y).
    X = 1,
    Y = true.
    
    ?- X=1, check_both(X=2, Y).
    false.
    
    ?- X=1, check_both(true, X=1).
    X = 1.
    
    ?- X=1, check_both(true, X=2).
    false.
    
    ?- member(X, [a, b]), check_both(X=Y, true).
    X = Y, Y = a ;
    X = Y, Y = b.