CODEWITHSUNDEEP
prologfirst-order-logic
Dragoș Constantin
Dragoș Constantin

Reputation: 1

How would you go about implementing this example of Resolution in Prolog?

This is perhaps one of the simpler examples of Resolution in FOL there is, but I'm having some trouble wrapping my head around how this would look like written in Prolog:

∀x. GradStudent(x) ⊃ Student(x)
∀x. Student(x) ⊃ HardWorker(x)
GradStudent(sue)

The query is KB |= HardWorker(sue). I can see how you'd go about manually doing the Resolution, but I'm lost as to how this would look like in Prolog.

Where I'm getting stuck is the HardWorker predicate, there is no explicit definition of HardWorker and of course that is not valid in Prolog.

Upvotes: 0

Views: 202

Answers (1)

repeat
repeat

Reputation: 18726

Turn the arrow around:

hardworker(X) :- student(X).

student(X) :- gradstudent(X).

gradstudent(sue).

So we go on and ask if sue is a hard worker:

?- hardworker(sue).
true.

Note the incompleteness of this all: There are other hard workers than just students. There are other kinds of students than grad students. And Sue is probably not the only grad student.

Upvotes: 1

Related Questions