cs110 This example is taken from the predicate calculus and

cs110

This example is taken from the predicate calculus and represents a goal-driven graph search where the goal to be proved true in this situation is a predicate calculus expression containing variables. The axioms are the logical descriptions of a relationship between a Fred is a collie. collie(fred). Sam is Fred\'s master. master(fred, sam). The day is Saturday. day(saturday). It is cold on Saturday. not (warm(saturday)). Fred is trained. trained(fred). Spaniels are good dogs and so are trained collies. forall X[spaniel(X) logicalor (collie(X) logicaland trained(X)) rightarrow gooddog(X)] If a dog is a good dog and has a master then he will be with his master. forall (X, Y, Z) [gooddog(X) logicaland master(X, Y) logicaland location(Y, Z) rightarrow location(X, Z)] If it is Saturday and warm, then Sam is at the park. (day(saturday) logicaland warm(saturday)) rightarrow location(sam, park). If it is Saturday and not warm, then Sam is at the museum. (day(saturday) logicaland not (warm(Saturday))) rightarrow location(sam, museum).

Solution

Location(X,Z) Gooddog(X) Collie(X) Collie(fred) trained(X) trained(fred) master(X,Y) master (fred,sam) location(Y,Z) day(Saturday) -(warm(Saturday)) Subsituition={fred/X,sam/Y,musesum}