;rules:
(infer (good X) from (logical X)
		     (simple X))
(infer (logical Y) from (scientific Y))

;facts:
(infer (good prolog))
(infer (huge jupiter))

constant
Var
(less 3 Z)


(tree Subtree1 Root Subtree2)

(cons a (cons b nil))


(sentence
 (np (n ron))
 (vp (v gave)
     (np (art a) (n paper))
     (compls (prep to) (np (n sue)))))

(infer (understands L X)
   from (groks terms L X)
	(groks syntax L X)
	(groks semantics L X))

; a semantic network
(infer (object event1 paper))
(infer (recipeint event1 sue))
(infer (actor event1 ron))
(infer (action event1 gave))

;was the object of event1 a paper?
-> (infer? (object event1 paper))
Satisfied

; what was given in event1
-> (infer? (object event1 What)
>          (print What))
paper
Satisfied

-> (infer? (actor Event Who)
>          (action Event gave)
>          (print Who Event))
ron event1
Satisfied

-> (infer? (actor X Y)
>           (action X Z)
            (print X Y Z))
event1 ron gave
Satisfied

(infer (g X Y) from (h1 Y) (h2 X))

means

for all X, Y:
  if (h1 Y) and (h2 X)
  then (g X Y)






(infer (f X))

means

for all X: (f X) is true

(infer (member X (cons X L)))
(infer (member X (cons Y M))
        from (member X M))



(infer (list nil))
(infer (list (cons X L)) from (list L))

(infer? (list (cons 1 (cons 2 nil))))


(infer (equals (addtoend nil X)
	       (cons X nil)))
(infer (equals (addtoend (cons Y L) X)
	       (cons Y M))
  from (equals (addtoend L X)
	       M))
(infer? (equals (addtoend (cons 3 nil) 4)
	        L)
        (print L))

C1
C2
C3
(infer? goal)

means:

try to satisfy goal by C1,
 then by C2, ...




(infer g from h1 h2)

means:

to satisfy g,
  first do h1, then h2

(infer imokay from youreokay hesokay) ; C1
(infer yourokay from theyreokay) ; C2
(infer hesokay) ; C3
(infer theyreokay) ; C4
(infer? imokay)






(infer hesnotokay from imnotokay) ; C5
(infer shesokay from hesnotokay) ; C6
(infer shesokay from theyreokay) ; C7
(infer? shesokay)






(infer hesnotokay from shesokay) ; C8
(infer hesnotokay from imokay) ; C9
(infer? shesokay)