Backchaining Theorem Prover

   1.  ((FATHER (ZEUS) (ARES)))
   2.  ((MOTHER (HERA) (ARES)))
   3.  ((FATHER (ARES) (HARMONIA)))
   4.  ((PARENT X Y) (MOTHER X Y))
   5.  ((PARENT X Y) (FATHER X Y))
   6.  ((GRANDPARENT X Y) (PARENT Z Y) (PARENT X Z))

> (goal '(father x (harmonia)))
  1>  (GOAL (FATHER X (HARMONIA)))
((X ARES))

> (goal '(parent z (harmonia)))
  1>  (GOAL (PARENT Z (HARMONIA)))
    2>  (GOAL (FATHER Z (HARMONIA)))
    < 2 (GOAL ((Z ARES)))
((Z ARES))

> (goal '(grandparent x (harmonia)))
  1>  (GOAL (GRANDPARENT X (HARMONIA)))
    2>  (GOAL (PARENT Z (HARMONIA)))
      3>  (GOAL (FATHER Z (HARMONIA)))
      < 3 (GOAL ((Z ARES)))
    < 2 (GOAL ((Z ARES)))
    2>  (GOAL (PARENT X (ARES)))
      3>  (GOAL (FATHER X (ARES)))
      < 3 (GOAL ((X ZEUS)))
    < 2 (GOAL ((X ZEUS)))
((X ZEUS))

Contents    Page-10    Prev    Next    Page+10    Index