searchprologlogicnegationclause

Prolog order of clause body gives different results when using negation


I am struggling to understand why swapping the two body clauses gives different results when one of the clauses is a negation.

married(john).
male(john).
male(kev).

bachelor1(X) :- \+ married(X), male(X).
bachelor2(X) :- male(X), \+ married(X).

bachelor1(X). doesn't find any atom.

bachelor2(X). finds kev.


Solution

  • The operator \+ (mnemonic: ⊬) implements a non-monotonic inference rule (known as negation as failure) that expresses logical negation only for ground goals. According to this rule, \+(G) is true only if goal G cannot be proven. In other words, to prove \+(G), Prolog first tries to prove G and then:

    As we can see, both predicates bachelor1/1 and bachelor2/1 work as expected for queries without variables:

    ?- bachelor1(john).
    false.
    
    ?- bachelor1(kev).
    true.
    
    ?- bachelor2(john).
    false.
    
    ?- bachelor2(kev).
    true.
    

    In fact, the problem only occurs with queries containing variables. To understand the difference between bachelor1/1 and bachelor2/1, analyze the following Prolog search trees:

    First version

    Second version