I wonder if I can use Prolog to do resolution reasoning

Question

I'm very new to mathematical logic and I'm trying to learn Prolog recently, I wonder if I can use Prolog to do resolution reasoning, e.g., to do the following reasoning:

1. knowing that ∀x.(sheep(x)→eatgrass(x))
2. knowing that ∀x.(deadsheep(x)→¬eatgrass(x))
3. to prove ∀x.(deadsheep(x)→¬sheep(x))

what I'm trying to realize is that write code like the following:

eatgrass(X) :- sheep(X).
false       :- deadsheep(X), eatgrass(X).
sheep(X).
deadsheep(X).

and get query answer 'false' when query

?- sheep(a),deadsheep(a).

It seems in Prolog I cannot realize something like line 2:

false :- deadsheep(X), eatgrass(X).

so I wonder if there is a way to do the reasoning like above mentioned in Prolog, thanks!

Answer 1

false :- deadsheep(X), eatgrass(X).

is an integrity constraint.

While exploitable in a more resolution-based theorem prover, you cannot have this in Prolog because it's not a clause (neither a definite clause, aka. Horn clause, i.e. without negation in the body, nor a general clause, i.e. with 'negation as failure' in the body).

(As an example, the Markgraf Karl Resolution Theorem Prover of 1981 indeed could handle integrity constraints)

Integrity constraints can be found in Answer Set Programming systems, which find solutions to logic programs in a way quite different from Prolog: not by SLDNF proof search but by finding sets of ground facts that are a model of the program (i.e. that make every statement of the program true).

You program with

sheep(X), deadsheep(X). does not make sense (because it says "everything is a sheep" and "everythinh is a deadsheep"), but if you change this to:

eatgrass(X) :- sheep(X).
false       :- deadsheep(X), eatgrass(X).
sheep(flopsy).
deadsheep(flopsy).

then this program is a way of asking: is there a set of ground atoms (in the logic sense) based on eatgrass/1, sheep/1, deadsheep/1 that is a model for the program, i.e. for which every statement of the program becomes true?.

Well, there is not, because we need

sheep(flopsy).
deadsheep(flopsy).

to be true, so clearly eatgrass(flopsy) needs to be true too, and this violates the integrity constraint.

What you can do is test the integrity constraint as part of your query:

Program:

eatgrass(X) :- sheep(X).
sheep(flopsy).
deadsheep(flopsy).

Query: Is there a sheep X such that X is not both eating grass and dead?

?- sheep(X),\+ (deadsheep(X),eatgrass(X)).

In this case, no.

Answer 2

As @David Tonhofer suggested, integrity constraints can be found in Answer Set Programming systems, I found potassco's clingo is a great tool to solve my problem, so I put the example code here in case someone may need a similar one:

eatgrass(X) :- sheep(X).
            :- deadsheep(X), eatgrass(X).
sheep(shawn).
deadsheep(shawn).

The second line is an integrity constraint which can be supported in clingo, and if you run this program using clingo online, clingo will tell you this is unsatisfiable, which suggests the reasoning is correct.