;;; A simple theorem proving domain for EGGS inspired by the MA system. ;;; Try (eggs '(derives nil (or (and p q) (not (and p q)))) 6) then try ;;; again after learning or try (derives nil (or p (not p))) (index-brules '((<- (derives (?x . ?y) ?x)) (<- (derives ?x (or ?y ?z)) (derives ?x ?y)) (<- (derives ?x (or ?y ?z)) (derives ?x ?z)) (<- (derives ?y ?z) (derives (?x . ?y) ?z) (derives ((not ?x) . ?y) ?z))))