;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Today: Logic programming
;;
;; Viewpoint #3: (best)
;; We are building a 'model' of truth. We start by
;; asserting some basic facts (axioms) -- these
;; facts are assumed to be true.
;;
;; We also specify some rules of inference which tell
;; us how to use some facts to prove other facts. The
;; process of tracing from axioms to final facts
;; (or backwards) is called deduction.
(load "query.scm")
(query-driver-loop)
;;
;; Rules
;;
;; So far, just a glorified fact-repeater. Not very
;; interesting.
(assert! (kurt likes logic))
(assert! (kurt likes 61a students))
(assert! (kurt likes 61a midterm grading))
(assert! (kurt likes (giving zeroes)))
(assert! (kurt likes (failing students)))
(kurt likes ?what)
;; But, I told you that this system can also do
;; deductions -- like so:
(assert! (rule (?something is good)
(kurt likes ?something)))
;; (rule x y) -->
;; o if y then x
;; o y implies x
;; o y -> x
;;
;; o if y is provably true, then so is x
;;
(?what is good)
;;
;; o How does do this?
;;
;; o It knows "(kurt likes logic)" is true.
;; o It knows that if "(kurt likes x)" then
;; "(x is good)" is true.
;;
;; o Therefore, "(logic is good)"
;;
;;
;; o Formally: X is true if
;; 1. X is an axiom
;; 2. X can be formed by applying rules of
;; inference (recursively) to axioms
;;
;; o Rules are not bidirectional:
;;
;;
;; kurt likes something -> it is good
;; something is good --/--> kurt likes it
;; example:
(assert! (ambeval is good))
(kurt likes ?what)
(?what is good)
;;
;; Interesting rules:
;;
;; o We can use rules to describe the relations
;; between alogirthms, their inputs, and their
;; return values.
;;
;; o Consider APPEND:
;;
;; o What can we say about the relations of Append
;;
;; 1. (append ?x ?y ?z) ; (append x y) ==> z
;;
;; 2. (append () ?x ?x) ; (append '() x) ==> x
;;
;; 3. (append (cons a x) y) == (cons a (append x y))
;;
;; -- in the logic language --
;;
;; 3. (append ?x ?y ?z) -> (append (?a . ?x) ?y (?a . ?z))
;;
;;
;;
;; o Rules for Append
(assert! (rule (append () ?x ?x)))
(assert! (rule (append (?a . ?x) ?y (?a . ?z))
(append ?x ?y ?z)))
;; o What do we have?
;;
;; o Zero how-to knowledge.
;; o We'd only be half-way there to writing this in scheme.
;;
;; o A complete description of the rules for append.
;; o Sufficient for the logic language
(append (1 2 3) (4 5 6) ?z)
;; o But, remember that logic is just syntactic!!
;; o We haven't said which are inputs and/or outputs
(append (1 2 3) ?y (1 2 3 4 5 6))
;; o In fact, we can use multiple placeholders:
(append ?x ?y (1 2 3 4 5 6))
;; o This is super cool!
;; o But it is just syntactic pattern matching:
;;
;; "Find all patterns that start with "append"
;; and end with (1 2 3 4 5 6)
;; that are deducible from the rules and axia."
;; o There are limits:
(append ?x ?y ?z)
;; o We'll explore these a bit more later: