Prolog - resolution

2
votes

I am doing resolution proof in formal logic using truth table and prolog program outcome of my experiments are different and I want to know why.

Here is the problem in plain english: 1. If someone looks into eyes of fighter, he is going to get angry. 2. If the fighter gets angry, he is going to punch.

If the fighter punched, did someone look into fighter's eyes?

'Fighter punched' is conclusion, and we know when conclusion is true the premise could be either false or true, therefore we can't answer the question.

However, following SWI prolog program returns true:

eyes:-angry.
angry:-punch.
punch.
?-eyes.
True

Also

aggregate_all(count, (eyes), Count) 
1

Can somebody explain this?

1
prologlogicresolution

1 Answers

3
votes

Remember that :- in Prolog is supposed to look like an arrow — an arrow from right to left, like <==. (We do not actually use an arrow, so that users can freely define a custom operator and use it for their own purpose without interfering with regular Prolog code.)

Thus, all your arrows point in the wrong direction. You probably meant:

angry(true) :- eyes(true).

punch(true) :- angry(true).

I am introducing a Boolean argument for these predicates so that you can play with different parameters without worrying about (non)existence of any predicates.

For example, if you add to these clauses:

eyes(true).

Then you get:

?- punch(T).
T = true.

However, if you instead add:

eyes(false).

then you get:

?- punch(T).
false.

This shows that yes, someone must have looked the person in the eye.