diff --git a/4-1.org b/4-1.org
index ca58ad2..ad0fd54 100644
--- a/4-1.org
+++ b/4-1.org
@@ -408,40 +408,40 @@ Borrowed from [[http://wqzhang.wordpress.com/2009/09/17/sicp-exercise-4-3/][Weiq
   ;; Exercise 4.3
   ;; -------------------------------------------------------------------
 
-  (define eval-table (make-eq-hash-table))
-  (define (get key)
-    (hash-table/get eval-table key #f))
-  (define (put key proc)
-    (hash-table/put! eval-table key proc))
+  (define *op-table* (make-eq-hash-table))
+  (define (get op type)
+    (hash-table/get *op-table* (list op type) #f))
+  (define (put op type proc)
+    (hash-table/put! *op-table* (list op type) proc))
 
   (define (eval exp env)
     (cond ((self-evaluating? exp) exp)
           ((variable? exp) (lookup-variable-value exp env))
-          ((get (car exp))
-           ((get (car exp)) exp env))
+          ((get (car exp) 'eval)
+           ((get (car exp) 'eval) exp env))
           ((application? exp)
            (apply (eval (operator exp) env)
                   (list-of-values (operands exp) env)))
           (else
            (error "Unknown expression type -- EVAL" exp))))
 
-  (put 'quote
+  (put 'quote 'eval
        (lambda (exp env)
          (text-of-quotation exp)))
-  (put 'set!
+  (put 'set! 'eval
        (lambda (exp env)
          (eval-assignment exp env)))
-  (put 'define eval-definition)
-  (put 'if eval-if)
-  (put 'lambda
+  (put 'define 'eval eval-definition)
+  (put 'if 'eval eval-if)
+  (put 'lambda 'eval
        (lambda (exp env)
          (make-procedure (lambda-parameters exp)
                          (lambda-body exp)
                          env)))
-  (put 'begin
+  (put 'begin 'eval
        (lambda (exp env)
          (eval-sequence (begin-actions exp) env)))
-  (put 'cond
+  (put 'cond 'eval
        (lambda (exp env)
          (eval (cond->if exp) env)))
 #+END_SRC
@@ -496,8 +496,8 @@ and ~or~ as derived expressions.
                 (eval-or-operands rest)))))
     (eval-or-operands (operands exp)))
 
-  (put 'and eval-and)
-  (put 'or eval-or)
+  (put 'and 'eval eval-and)
+  (put 'or 'eval eval-or)
 
   ;; Derived expressions
 
@@ -588,7 +588,7 @@ expressions.
               (map cadr var-alist))))
 
 
-  (put 'let
+  (put 'let 'eval
        (lambda (exp env)
          (eval (let->combination exp) env)))
 #+END_SRC
@@ -646,7 +646,7 @@ expressions?
     (nested-let (cadr exp)
                 (cddr exp)))
 
-  (put 'let*
+  (put 'let* 'eval
        (lambda (exp env)
          (eval (let*->nested-lets exp) env)))
 #+END_SRC
@@ -708,7 +708,7 @@ Modify ~let->combination~ of [[Exercise 4.6]] to also support named ~let~.
                                   (cdddr exp)))
           (else (error "Invalid expression -- LET"))))
 
-  (put 'let
+  (put 'let 'eval
        (lambda (exp env)
          (eval (let->combination exp) env)))
 #+END_SRC
diff --git a/4-4.org b/4-4.org
new file mode 100644
index 0000000..45e876e
--- /dev/null
+++ b/4-4.org
@@ -0,0 +1,899 @@
+#+TITLE: 4.4 - Logic Programming
+#+STARTUP: indent
+#+OPTIONS: num:nil
+
+- [[file:4-4.org][Raw org source]]
+- [[file:4-4.org.html][Htmlized org source]]
+  
+This section seems to describe all the cool things that turned me on
+to Prolog.
+* COMMENT Set up source file
+#+BEGIN_SRC scheme :tangle yes
+  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+  ;; 4.4 - Logic Programming
+  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+  (load "3-5.scheme") ;; Stream functions
+  (load "4-3.scheme") ;; All the things so far
+
+#+END_SRC
+* Deductive Information Retrieval
+
+** A sample data base
+#+name: knowledgebase
+#+BEGIN_SRC scheme :tangle 4-4-1-kb.scheme
+  ;; The personnel data base for Microshaft contains "assertions" about
+  ;; company personnel.  Here is the information about Ben Bitdiddle, the
+  ;; resident computer wizard:
+
+  (address (Bitdiddle Ben) (Slumerville (Ridge Road) 10))
+  (job (Bitdiddle Ben) (computer wizard))
+  (salary (Bitdiddle Ben) 60000)
+
+  ;; Each assertion is a list (in this case a triple) whose elements can
+  ;; themselves be lists.
+
+  ;; As resident wizard, Ben is in charge of the company's computer
+  ;; division, and he supervises two programmers and one technician.  Here
+  ;; is the information about them:
+
+  (address (Hacker Alyssa P) (Cambridge (Mass Ave) 78))
+  (job (Hacker Alyssa P) (computer programmer))
+  (salary (Hacker Alyssa P) 40000)
+  (supervisor (Hacker Alyssa P) (Bitdiddle Ben))
+
+  (address (Fect Cy D) (Cambridge (Ames Street) 3))
+  (job (Fect Cy D) (computer programmer))
+  (salary (Fect Cy D) 35000)
+  (supervisor (Fect Cy D) (Bitdiddle Ben))
+
+  (address (Tweakit Lem E) (Boston (Bay State Road) 22))
+  (job (Tweakit Lem E) (computer technician))
+  (salary (Tweakit Lem E) 25000)
+  (supervisor (Tweakit Lem E) (Bitdiddle Ben))
+
+  ;; There is also a programmer trainee, who is supervised by Alyssa:
+
+  (address (Reasoner Louis) (Slumerville (Pine Tree Road) 80))
+  (job (Reasoner Louis) (computer programmer trainee))
+  (salary (Reasoner Louis) 30000)
+  (supervisor (Reasoner Louis) (Hacker Alyssa P))
+
+  ;; All of these people are in the computer division, as indicated by
+  ;; the word `computer' as the first item in their job descriptions.
+
+  ;; Ben is a high-level employee.  His supervisor is the company's big
+  ;; wheel himself:
+
+  (supervisor (Bitdiddle Ben) (Warbucks Oliver))
+
+  (address (Warbucks Oliver) (Swellesley (Top Heap Road)))
+  (job (Warbucks Oliver) (administration big wheel))
+  (salary (Warbucks Oliver) 150000)
+
+  ;; Besides the computer division supervised by Ben, the company has an
+  ;; accounting division, consisting of a chief accountant and his assistant:
+
+  (address (Scrooge Eben) (Weston (Shady Lane) 10))
+  (job (Scrooge Eben) (accounting chief accountant))
+  (salary (Scrooge Eben) 75000)
+  (supervisor (Scrooge Eben) (Warbucks Oliver))
+
+  (address (Cratchet Robert) (Allston (N Harvard Street) 16))
+  (job (Cratchet Robert) (accounting scrivener))
+  (salary (Cratchet Robert) 18000)
+  (supervisor (Cratchet Robert) (Scrooge Eben))
+
+  ;; There is also a secretary for the big wheel:
+
+  (address (Aull DeWitt) (Slumerville (Onion Square) 5))
+  (job (Aull DeWitt) (administration secretary))
+  (salary (Aull DeWitt) 25000)
+  (supervisor (Aull DeWitt) (Warbucks Oliver))
+
+  ;; The data base also contains assertions about which kinds of jobs can
+  ;; be done by people holding other kinds of jobs.  For instance, a
+  ;; computer wizard can do the jobs of both a computer programmer and a
+  ;; computer technician:
+
+  (can-do-job (computer wizard) (computer programmer))
+  (can-do-job (computer wizard) (computer technician))
+
+  ;; A computer programmer could fill in for a trainee:
+
+  (can-do-job (computer programmer)
+              (computer programmer trainee))
+
+  ;; Also, as is well known,
+
+  (can-do-job (administration secretary)
+              (administration big wheel))
+#+END_SRC
+
+*** Prolog
+#+name: gen-pl-knowledgebase
+#+BEGIN_SRC emacs-lisp :noweb yes :exports none
+  (defun pl-symbol (symbol)
+    (->> symbol
+         symbol-name
+         s-downcase
+         (s-replace "-" "_")))
+
+  (defun pl-sequence (sequence)
+    (s-join ", " (mapcar #'pl-term sequence)))
+
+  (defun pl-list (sequence)
+    (s-concat "[" 
+              (pl-sequence sequence)
+              "]"))
+
+  (defun pl-term (term)
+    (cond ((symbolp term) (pl-symbol term))
+          ((listp term) (pl-list term))
+          (t (format "%s" term))))
+
+  (defun pl-fact (sequence)
+    (s-concat (pl-symbol (car sequence))
+              "("
+              (pl-sequence (cdr sequence))
+              ")."))
+
+  (let ((facts (mapcar #'pl-fact (quote (
+                                         <<knowledgebase>>
+                                         )))))
+    (s-join "\n" (sort facts #'string-lessp)))
+#+END_SRC
+
+For the sake of having something to play with, the knowledgebase is
+converted to prolog below:
+
+#+name: pl-knowledgebase
+#+caption: [[file:4-4-kb.pl]]
+#+BEGIN_SRC prolog :noweb yes :tangle yes :exports code
+  %% -*- mode: prolog -*-
+
+  <<gen-pl-knowledgebase()>>
+#+END_SRC
+
+** Simple queries
+
+Queries are performed by unifying patterns against known facts and
+rules. Variables in patterns are bound as the pattern is matched, and
+results are returned for all successful matches.
+
+** Compound queries
+
+#+BEGIN_QUOTE
+Simple queries form the primitive operations of the query language.
+In order to form compound operations, the query language provides
+means of combination.
+#+END_QUOTE
+
+#+BEGIN_QUOTE
+As for simple queries, the system processes a compound query by
+finding all assignments to the pattern variables that satisfy the
+query, then displaying instantiations of the query with those values.
+#+END_QUOTE
+
+*** Exercise 4.56
+Formulate compound queries that retrieve the following information:
+
+  a. the names of all people who are supervised by Ben Bitdiddle,
+     together with their addresses;
+  
+     ----------------------------------------------------------------------
+  
+     #+BEGIN_SRC scheme
+       (and (supervisor ?person (Bitdiddle Ben))
+            (address ?person ?where))
+     #+END_SRC
+  b. all people whose salary is less than Ben Bitdiddle's,
+     together with their salary and Ben Bitdiddle's salary;
+  
+     ----------------------------------------------------------------------
+  
+     #+BEGIN_SRC scheme
+       (and (salary (Bitdiddle Ben) ?salary-ben)
+            (salary ?person ?salary-person)
+            (< ?salary-person ?salary-ben))
+     #+END_SRC
+  c. all people who are supervised by someone who is not in the
+     computer division, together with the supervisor's name and
+     job.
+  
+     ----------------------------------------------------------------------
+  
+     #+BEGIN_SRC scheme
+       (and (supervisor ?person ?supervisor)
+            (job ?supervisor ?supervisor-job)
+            (not (job ?supervisor (computer . ?))))
+     #+END_SRC
+
+** Rules
+Rules are a tool for abstracting queries
+
+#+BEGIN_SRC scheme
+  (rule (lives-near ?person-1 ?person-2)
+        (and (address ?person-1 (?town . ?rest-1))
+             (address ?person-2 (?town . ?rest-2))
+             (not (same ?person-1 ?person-2))))
+#+END_SRC
+
+The same rule would be expressed in Prolog as:
+
+#+BEGIN_SRC prolog :tangle yes
+  lives_near(Person1, Person2) :-
+      address(Person1, [Town|_]),
+      address(Person2, [Town|_]),
+      Person1 \= Person2.
+#+END_SRC
+
+*** Exercise 4.57
+Define a rule that says that person 1 can replace
+person 2 if either person 1 does the same job as person 2 or
+someone who does person 1's job can also do person 2's job, and if
+person 1 and person 2 are not the same person. Using your rule,
+give queries that find the following:
+
+  a. all people who can replace Cy D. Fect;
+
+  b. all people who can replace someone who is being paid more
+     than they are, together with the two salaries.
+
+----------------------------------------------------------------------
+
+#+BEGIN_SRC scheme
+  (rule (can-replace ?person-1 ?person-2)
+        (and (job ?person-1 ?job-1)
+             (job ?person-2 ?job-2)
+             (not (same ?person-1 ?person-2))
+             (or (same ?job-1 ?job-2)
+                 (can-do-job ?job-1 ?job-2))))
+
+  (can-replace ?person (Cy D Fect))
+
+  (and (can-replace ?person-1 ?person-2)
+       (salary ?person-1 ?salary-1)
+       (salary ?person-2 ?salary-2)
+       (< ?salary-1 ?salary-2))
+#+END_SRC
+
+#+BEGIN_SRC prolog :tangle yes
+  can_replace(P1, P2) :-
+      job(P1, J1),
+      job(P2, J2),
+      (J1 == J2; can_do_job(J1, J2)),
+      P1 \= P2.
+
+  can_replace_for_cheap(P1, P2, S1, S2) :-
+      can_replace(P1, P2),
+      salary(P1, S1),
+      salary(P2, S2),
+      S1 > S2.
+#+END_SRC
+*** Exercise 4.58
+Define a rule that says that a person is a "big shot" in a division if
+the person works in the division but does not have a supervisor who
+works in the division.
+
+----------------------------------------------------------------------
+
+#+BEGIN_SRC scheme
+  (rule (big-shot ?person)
+        (job ?person (?division . ?))
+        (supervisor ?person ?supervisor)
+        (not (job ?supervisor (?division . ?))))
+#+END_SRC
+
+#+BEGIN_SRC prolog
+  big_shot(Person) :-
+      job(Person, [Division|_]),
+      supervisor(Person, Supervisor),
+      job(Supervisor, [SDivision|_]),
+      Division \= SDivision.
+#+END_SRC
+
+*** Exercise 4.59
+Ben Bitdiddle has missed one meeting too many.
+Fearing that his habit of forgetting meetings could cost him his
+job, Ben decides to do something about it.  He adds all the weekly
+meetings of the firm to the Microshaft data base by asserting the
+following:
+
+#+BEGIN_SRC scheme
+  (meeting accounting (Monday 9am))
+  (meeting administration (Monday 10am))
+  (meeting computer (Wednesday 3pm))
+  (meeting administration (Friday 1pm))
+#+END_SRC
+
+#+BEGIN_SRC prolog :tangle yes
+  meeting(accounting, [monday, '9am']).
+  meeting(administration, [monday, '10am']).
+  meeting(computer, [wednesday, '3pm']).
+  meeting(administration, [friday, '1pm']).
+#+END_SRC
+
+Each of the above assertions is for a meeting of an entire
+division.  Ben also adds an entry for the company-wide meeting
+that spans all the divisions.  All of the company's employees
+attend this meeting.
+
+#+BEGIN_SRC scheme
+  (meeting whole-company (Wednesday 4pm))
+#+END_SRC
+
+#+BEGIN_SRC prolog :tangle yes
+  meeting(whole_company, [wednesday, '4pm']).
+#+END_SRC
+
+  a. On Friday morning, Ben wants to query the data base for all
+     the meetings that occur that day.  What query should he use?
+
+     ----------------------------------------------------------------------
+
+     #+BEGIN_SRC scheme
+       (meeting ?who (Friday ?when))
+     #+END_SRC
+
+     #+BEGIN_SRC prolog
+       meeting(Who, [friday, When]).
+     #+END_SRC
+
+  b. Alyssa P. Hacker is unimpressed.  She thinks it would be much
+     more useful to be able to ask for her meetings by specifying
+     her name.  So she designs a rule that says that a person's
+     meetings include all `whole-company' meetings plus all
+     meetings of that person's division.  Fill in the body of
+     Alyssa's rule.
+
+     #+BEGIN_SRC scheme
+       (rule (meeting-time ?person ?day-and-time)
+             <RULE-BODY>)
+     #+END_SRC
+
+     ----------------------------------------------------------------------
+
+     #+BEGIN_SRC scheme
+       (rule (meeting-time ?person ?day-and-time)
+             (and (job ?person (?department . ?))
+                  (or (meeting whole-company ?day-and-time)
+                      (meeting ?department ?day-and-time))))
+     #+END_SRC
+
+     #+BEGIN_SRC prolog :tangle yes
+       meeting_time(Person, DayAndTime) :-
+           job(Person, [Department|_]),
+           (meeting(whole_company, DayAndTime);
+            meeting(Department, DayAndTime)).
+     #+END_SRC
+  c. Alyssa arrives at work on Wednesday morning and wonders what
+     meetings she has to attend that day.  Having defined the
+     above rule, what query should she make to find this out?
+
+     ----------------------------------------------------------------------
+
+     #+BEGIN_SRC scheme
+       (meeting-time (Hacker Alyssa P) (Wednesday ?))
+     #+END_SRC
+
+     #+BEGIN_SRC prolog
+       meeting_time([hacker, alyssa, p], [wednesday, _]).
+     #+END_SRC
+*** Exercise 4.60
+By giving the query
+
+#+BEGIN_SRC scheme
+     (lives-near ?person (Hacker Alyssa P))
+#+END_SRC
+
+Alyssa P. Hacker is able to find people who live near her, with
+whom she can ride to work.  On the other hand, when she tries to
+find all pairs of people who live near each other by querying
+
+#+BEGIN_SRC scheme
+     (lives-near ?person-1 ?person-2)
+#+END_SRC
+
+she notices that each pair of people who live near each other is
+listed twice; for example,
+
+#+BEGIN_SRC scheme
+     (lives-near (Hacker Alyssa P) (Fect Cy D))
+     (lives-near (Fect Cy D) (Hacker Alyssa P))
+#+END_SRC
+
+Why does this happen?  Is there a way to find a list of people who
+live near each other, in which each pair appears only once?
+Explain.
+
+** Logic as programs
+#+BEGIN_SRC scheme
+  (rule (append-to-form () ?y ?y))
+
+  (rule (append-to-form (?u . ?v) ?y (?u . ?z))
+        (append-to-form ?v ?y ?z))
+#+END_SRC
+
+#+BEGIN_SRC prolog :tangle yes
+  append([], L, L).
+  append([H|T], L2, [H|L3]) :-
+      append(T, L2, L3).
+#+END_SRC
+
+* How the Query System Works
+
+** Pattern matching
+
+** Streams of frames
+
+** Compound queries
+
+** Unification
+
+** Applying rules
+
+** Simple queries
+
+** The query evaluator and the driver loop
+
+* Is Logic Programming Mathematical Logic?
+
+** Infinite loops
+
+** Problems with `not'
+* Implementing the Query System
+** The Driver Loop and Instantiation
+#+BEGIN_SRC scheme :tangle yes
+  (define (query-driver-loop)
+    (prompt-for-input input-prompt)
+    (let ((q (query-syntax-process (read))))
+      (cond ((assertion-to-be-added? q)
+             (add-rule-or-assertion! (add-assertion-body q))
+             (newline)
+             (display "Assertion added to data base.")
+             (query-driver-loop))
+            (else
+             (newline)
+             (display output-prompt)
+             (display-stream
+              (stream-map
+               (lambda (frame)
+                 (instantiate q
+                              frame
+                              (lambda (v f)
+                                (contract-question-mark v))))
+               (qeval q (singleton-stream '()))))
+             (query-driver-loop)))))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (instantiate exp frame unbound-var-handler)
+    (define (copy exp)
+      (cond ((var? exp)
+             (let ((binding (binding-in-frame exp frame)))
+               (if binding
+                   (copy (binding-value binding))
+                   (unbound-var-handler exp frame))))
+            ((pair? exp)
+             (cons (copy (car exp)) (copy (cdr exp))))
+            (else exp)))
+    (copy exp))
+#+END_SRC
+** The Evaluator
+#+BEGIN_SRC scheme :tangle yes
+  (define (qeval query frame-stream)
+    (let ((qproc (get (type query) 'qeval)))
+      (if qproc
+          (qproc (contents query) frame-stream)
+          (simple-query query frame-stream))))
+#+END_SRC
+*** Simple queries
+#+BEGIN_SRC scheme :tangle yes
+  (define (simple-query query-pattern frame-stream)
+    (stream-flatmap
+     (lambda (frame)
+       (stream-append-delayed
+        (find-assertions query-pattern frame)
+        (delay (apply-rules query-pattern frame))))
+     frame-stream))
+#+END_SRC
+*** Compound queries
+#+BEGIN_SRC scheme :tangle yes
+  (define (conjoin conjuncts frame-stream)
+    (if (empty-conjunction? conjuncts)
+        frame-stream
+        (conjoin (rest-conjuncts conjuncts)
+                 (qeval (first-conjunct conjuncts)
+                        frame-stream))))
+
+  (put 'and 'qeval conjoin)
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (disjoin disjuncts frame-stream)
+    (if (empty-disjunction? disjuncts)
+        the-empty-stream
+        (interleave-delayed
+         (qeval (first-disjunct disjuncts) frame-stream)
+         (delay (disjoin (rest-disjuncts disjuncts)
+                         frame-stream)))))
+
+  (put 'or 'qeval disjoin)
+#+END_SRC
+*** Filters
+#+BEGIN_SRC scheme :tangle yes
+  (define (negate operands frame-stream)
+    (stream-flatmap
+     (lambda (frame)
+       (if (stream-null? (qeval (negated-query operands)
+                                (singleton-stream frame)))
+           (singleton-stream frame)
+           the-empty-stream))
+     frame-stream))
+
+  (put 'not 'qeval negate)
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (lisp-value call frame-stream)
+    (stream-flatmap
+     (lambda (frame)
+       (if (execute
+            (instantiate
+             call
+             frame
+             (lambda (v f)
+               (error "Unknown pat var -- LISP-VALUE" v))))
+           (singleton-stream frame)
+           the-empty-stream))
+     frame-stream))
+
+  (put 'lisp-value 'qeval lisp-value)
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (execute exp)
+    (apply (eval (predicate exp) user-initial-environment)
+           (args exp)))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (always-true ignore frame-stream) frame-stream)
+
+  (put 'always-true 'qeval always-true)
+#+END_SRC
+** Finding Assertions by Pattern Matching
+#+BEGIN_SRC scheme :tangle yes
+  (define (find-assertions pattern frame)
+    (stream-flatmap (lambda (datum)
+                      (check-an-assertion datum pattern frame))
+                    (fetch-assertions pattern frame)))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (check-an-assertion assertion query-pat query-frame)
+    (let ((match-result
+           (pattern-match query-pat assertion query-frame)))
+      (if (eq? match-result 'failed)
+          the-empty-stream
+          (singleton-stream match-result))))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (pattern-match pat dat frame)
+    (cond ((eq? frame 'failed) 'failed)
+          ((equal? pat dat) frame)
+          ((var? pat) (extend-if-consistent pat dat frame))
+          ((and (pair? pat) (pair? dat))
+           (pattern-match (cdr pat)
+                          (cdr dat)
+                          (pattern-match (car pat)
+                                         (car dat)
+                                         frame)))
+          (else 'failed)))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (extend-if-consistent var dat frame)
+    (let ((binding (binding-in-frame var frame)))
+      (if binding
+          (pattern-match (binding-value binding) dat frame)
+          (extend var dat frame))))
+#+END_SRC
+** Rules and Unification
+#+BEGIN_SRC scheme :tangle yes
+  (define (apply-rules pattern frame)
+    (stream-flatmap (lambda (rule)
+                      (apply-a-rule rule pattern frame))
+                    (fetch-rules pattern frame)))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (apply-a-rule rule query-pattern query-frame)
+    (let ((clean-rule (rename-variables-in rule)))
+      (let ((unify-result
+             (unify-match query-pattern
+                          (conclusion clean-rule)
+                          query-frame)))
+        (if (eq? unify-result 'failed)
+            the-empty-stream
+            (qeval (rule-body clean-rule)
+                   (singleton-stream unify-result))))))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (rename-variables-in rule)
+    (let ((rule-application-id (new-rule-application-id)))
+      (define (tree-walk exp)
+        (cond ((var? exp)
+               (make-new-variable exp rule-application-id))
+              ((pair? exp)
+               (cons (tree-walk (car exp))
+                     (tree-walk (cdr exp))))
+              (else exp)))
+      (tree-walk rule)))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (unify-match p1 p2 frame)
+    (cond ((eq? frame 'failed) 'failed)
+          ((equal? p1 p2) frame)
+          ((var? p1) (extend-if-possible p1 p2 frame))
+          ((var? p2) (extend-if-possible p2 p1 frame))  ; ***
+          ((and (pair? p1) (pair? p2))
+           (unify-match (cdr p1)
+                        (cdr p2)
+                        (unify-match (car p1)
+                                     (car p2)
+                                     frame)))
+          (else 'failed)))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (extend-if-possible var val frame)
+    (let ((binding (binding-in-frame var frame)))
+      (cond (binding
+             (unify-match
+              (binding-value binding) val frame))
+            ((var? val)                      ; ***
+             (let ((binding (binding-in-frame val frame)))
+               (if binding
+                   (unify-match
+                    var (binding-value binding) frame)
+                   (extend var val frame))))
+            ((depends-on? val var frame)     ; ***
+             'failed)
+            (else (extend var val frame)))))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (depends-on? exp var frame)
+    (define (tree-walk e)
+      (cond ((var? e)
+             (if (equal? var e)
+                 true
+                 (let ((b (binding-in-frame e frame)))
+                   (if b
+                       (tree-walk (binding-value b))
+                       false))))
+            ((pair? e)
+             (or (tree-walk (car e))
+                 (tree-walk (cdr e))))
+            (else false)))
+    (tree-walk exp))
+#+END_SRC
+** Maintaining the Data Base
+#+BEGIN_SRC scheme :tangle yes
+  (define THE-ASSERTIONS the-empty-stream)
+
+  (define (fetch-assertions pattern frame)
+    (if (use-index? pattern)
+        (get-indexed-assertions pattern)
+        (get-all-assertions)))
+
+  (define (get-all-assertions) THE-ASSERTIONS)
+
+  (define (get-indexed-assertions pattern)
+    (get-stream (index-key-of pattern) 'assertion-stream))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (get-stream key1 key2)
+    (let ((s (get key1 key2)))
+      (if s s the-empty-stream)))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define THE-RULES the-empty-stream)
+
+  (define (fetch-rules pattern frame)
+    (if (use-index? pattern)
+        (get-indexed-rules pattern)
+        (get-all-rules)))
+
+  (define (get-all-rules) THE-RULES)
+
+  (define (get-indexed-rules pattern)
+    (stream-append
+     (get-stream (index-key-of pattern) 'rule-stream)
+     (get-stream '? 'rule-stream)))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (add-rule-or-assertion! assertion)
+    (if (rule? assertion)
+        (add-rule! assertion)
+        (add-assertion! assertion)))
+
+  (define (add-assertion! assertion)
+    (store-assertion-in-index assertion)
+    (let ((old-assertions THE-ASSERTIONS))
+      (set! THE-ASSERTIONS
+            (cons-stream assertion old-assertions))
+      'ok))
+
+  (define (add-rule! rule)
+    (store-rule-in-index rule)
+    (let ((old-rules THE-RULES))
+      (set! THE-RULES (cons-stream rule old-rules))
+      'ok))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (store-assertion-in-index assertion)
+    (if (indexable? assertion)
+        (let ((key (index-key-of assertion)))
+          (let ((current-assertion-stream
+                 (get-stream key 'assertion-stream)))
+            (put key
+                 'assertion-stream
+                 (cons-stream assertion
+                              current-assertion-stream))))))
+
+  (define (store-rule-in-index rule)
+    (let ((pattern (conclusion rule)))
+      (if (indexable? pattern)
+          (let ((key (index-key-of pattern)))
+            (let ((current-rule-stream
+                   (get-stream key 'rule-stream)))
+              (put key
+                   'rule-stream
+                   (cons-stream rule
+                                current-rule-stream)))))))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (indexable? pat)
+    (or (constant-symbol? (car pat))
+        (var? (car pat))))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (index-key-of pat)
+    (let ((key (car pat)))
+      (if (var? key) '? key)))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (use-index? pat)
+    (constant-symbol? (car pat)))
+#+END_SRC
+** Stream Operations
+#+BEGIN_SRC scheme :tangle yes
+  (define (stream-append-delayed s1 delayed-s2)
+    (if (stream-null? s1)
+        (force delayed-s2)
+        (cons-stream
+         (stream-car s1)
+         (stream-append-delayed (stream-cdr s1) delayed-s2))))
+
+  (define (interleave-delayed s1 delayed-s2)
+    (if (stream-null? s1)
+        (force delayed-s2)
+        (cons-stream
+         (stream-car s1)
+         (interleave-delayed (force delayed-s2)
+                             (delay (stream-cdr s1))))))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (stream-flatmap proc s)
+    (flatten-stream (stream-map proc s)))
+
+  (define (flatten-stream stream)
+    (if (stream-null? stream)
+        the-empty-stream
+        (interleave-delayed
+         (stream-car stream)
+         (delay (flatten-stream (stream-cdr stream))))))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (singleton-stream x)
+    (cons-stream x the-empty-stream))
+#+END_SRC
+** Query Syntax Procedures
+#+BEGIN_SRC scheme :tangle yes
+  (define (type exp)
+    (if (pair? exp)
+        (car exp)
+        (error "Unknown expression TYPE" exp)))
+
+  (define (contents exp)
+    (if (pair? exp)
+        (cdr exp)
+        (error "Unknown expression CONTENTS" exp)))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (assertion-to-be-added? exp)
+    (eq? (type exp) 'assert!))
+
+  (define (add-assertion-body exp)
+    (car (contents exp)))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (empty-conjunction? exps) (null? exps))
+  (define (first-conjunct exps) (car exps))
+  (define (rest-conjuncts exps) (cdr exps))
+
+  (define (empty-disjunction? exps) (null? exps))
+  (define (first-disjunct exps) (car exps))
+  (define (rest-disjuncts exps) (cdr exps))
+
+  (define (negated-query exps) (car exps))
+
+  (define (predicate exps) (car exps))
+  (define (args exps) (cdr exps))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (rule? statement)
+    (tagged-list? statement 'rule))
+
+  (define (conclusion rule) (cadr rule))
+
+  (define (rule-body rule)
+    (if (null? (cddr rule))
+        '(always-true)
+        (caddr rule)))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (query-syntax-process exp)
+    (map-over-symbols expand-question-mark exp))
+
+  (define (map-over-symbols proc exp)
+    (cond ((pair? exp)
+           (cons (map-over-symbols proc (car exp))
+                 (map-over-symbols proc (cdr exp))))
+          ((symbol? exp) (proc exp))
+          (else exp)))
+
+  (define (expand-question-mark symbol)
+    (let ((chars (symbol->string symbol)))
+      (if (string=? (substring chars 0 1) "?")
+          (list '?
+                (string->symbol
+                 (substring chars 1 (string-length chars))))
+          symbol)))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (var? exp)
+    (tagged-list? exp '?))
+
+  (define (constant-symbol? exp) (symbol? exp))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define rule-counter 0)
+
+  (define (new-rule-application-id)
+    (set! rule-counter (+ 1 rule-counter))
+    rule-counter)
+
+  (define (make-new-variable var rule-application-id)
+    (cons '? (cons rule-application-id (cdr var))))
+#+END_SRC
+#+BEGIN_SRC scheme :tangle yes
+  (define (contract-question-mark variable)
+    (string->symbol
+     (string-append "?"
+                    (if (number? (cadr variable))
+                        (string-append (symbol->string (caddr variable))
+                                       "-"
+                                       (number->string (cadr variable)))
+                        (symbol->string (cadr variable))))))
+#+END_SRC
+** Frames and Bindings
+#+BEGIN_SRC scheme :tangle yes
+  (define (make-binding variable value)
+    (cons variable value))
+
+  (define (binding-variable binding)
+    (car binding))
+
+  (define (binding-value binding)
+    (cdr binding))
+
+  (define (binding-in-frame variable frame)
+    (assoc variable frame))
+
+  (define (extend variable value frame)
+    (cons (make-binding variable value) frame))
+#+END_SRC