;;;; -*- Mode: LISP; Syntax: Common-Lisp; Base: 10 -*- ;;;; --------------------------------------------------------------------- ;;;; File name: backward.lsp ;;;; System: FIRE ;;;; Author: Ken Forbus ;;;; Created: January 1, 2002 ;;;; Purpose: Backchainer ;;;; Modified: Thursday, June 3, 2004 at 11:48:53 by hinrichs ;;;; --------------------------------------------------------------------- ;;; The strategy for backchaining in FIRE is quite different than used in many reasoning ;;; systems. In logic programming systems and in many knowledge based systems (e.g., Cyc), ;;; backchaining is the principle manner in which things get done. What often happens in ;;; practice is that queries can absorb a huge amount of resources in an unpredicatable ;;; manner. Our strategy in FIRE is to keep backchaining tightly limited, so that (like ASK) ;;; it can be treated as a fairly simple, atomic process, with more complex situations handled ;;; by the and/or graph mechanism which supports the use of suggestions and plans. The latter ;;; provides more opportunities for reflection. But reflection of course is slow, hence the ;;; tightly limited backchaining supported in FIRE. ;;; One secret to avoiding poor performance due to exponentials is to keep ;;; the size of space being searched very small. As Pat Hayes put it, ;;; you turn loose of the dog's leash in a really big yard, and it will ;;; spend a lot of time running around. ;;; The idea we are exploring in FIRE is to keep the backchainer on a tight leash. ;;; We keep FIRE's backchainer constrained via the following: ;;; 1. The parameters max-depth and max-nodes set the maximum depth that will be explored by ;;; the backchainer and the maximum number of axioms that will be used, respectively. ;;; Standard but very useful techniques. If one sets these parameters very tightly initially, ;;; and expands them if more solutions are needed, this is a means of doing progressive deepening, ;;; which the search literature seems to suggest is a lot more efficient than living with the ;;; storage cost of constructing generators for a query. ;;; 2. Not all axioms are available for backchaining. Axioms in the KB are analyzed off-line and ;;; compiled into chainers. Backchaining only operates within a single chainer. ;;; If there is a result which can only be obtained via backchaining and requires multiple chainers, ;;; the suggestions architecture will have to be invoked to suggest answering those queries via ;;; backchaining on another chainer. ;;; Right now, for experimental purposes, we are using the following simplifications: ;;; 1. No support for generating suggestions based on backchaining failures. ;;; Which of them are worth pursuing is going to be an interesting question. ;;; Probably only backchainable predicates that are possibly inferrable through a ;;; different chainer. (If you could have gotten them with the current chainer, ;;; you would have!) ;;; 2. The default is to look at all chainers associated with a reasoner. ;;; Obviously, if suggestions are made about backtracking, they should specify a chainer. ;;;; The command interface entry point to the backchainer is ;;;; query ;;;; The programmatic interface entry points to the backchainer are ;;;; query-all, which checks all chainers ;;;; query-chainer, which uses the specified chainer ;;;; ;;;; The result of these procedures is a list of answers. Each answer has the form ;;;; ( . ) ;;;; where is a set of substitutions which, given the support, would ;;;; lead to an instantiation of formula which is true. is ;;;; a DAG whose entries (called steps) are of the form ;;;; ( . ) ;;;; where is the kind of support. can be :step or :kb or :WM. ;;;; is the statement in the argument, and ;;;; is a list of steps (possibly empty). ;;;; The purpose of the well-founded support is to enable FIRE to instantiate ;;;; a set of justifications in the LTRE which captures what was derived via backchaining. ;;;; (Not all conclusions are worth keeping, hence the creating of these datastructures rather ;;;; than just incrementally adding this information to the LTRE.) ;;;; helps FIRE figure out how to instantitiate something. ;;;; For :WM, nothing needs to be done since the result was obtained via LTRE access anyway. ;;;; ASK automatically installs TMS structure for its conclusions. ;;;; For :kb, a new assumption needs to be added to the working memory, namely that a particular ;;;; statement is in the KB. No substitutions should be performed on the KB statement, and ;;;; there should not be any antecedents. ;;;; For :step, a new clause needs to be added to the WM by (a) instantiating the arguments for ;;;; the antecedents and (b) installing a clause of the form (:implies (:and ,@ antes ,sub)) ;;;; where sub = with substitutions made. ;;;; Details below. (in-package :fire) ;;;------------------------------------------- ;;; Global registers used in the backchainer ;; ;; These parameters are used everywhere within the backchainer, so to keep the ;; code from getting too gnarly, we use specials for them. (defvar *max-nodes* 1000 "Work limit for a query") (defvar *max-depth* 10 "Maximum depth for a query") (defvar *current-chainer* nil "Chainer currently used.") (defvar *n-answers-sought* 100 "Number of answers sought in current query.") (defvar *current-context* :any "Current context used.") (defvar *bc-effort* :lots "Effort to be used (ASK parameter).") (defvar *bc-aggressive-tms?* t "Justify all conclusions in TMS immediately.") ;; Debugging registers. ;; These are only bound by the command-line entry point. (defvar cl-user::*results* nil) (defvar cl-user::*bindings* nil) (defvar cl-user::*reasons* nil) (defun q (formula &key (reasoner *reasoner*) (context :any) (effort :lots) (number :all) (max-depth 10) (max-nodes 10000) (chainer nil) (aggressive-tms? t)) "For command line use. Saves results in globals for easy access." (let ((results (query formula :reasoner reasoner :context context :effort effort :number number :max-depth max-depth :max-nodes max-nodes :chainer chainer :aggressive-tms? aggressive-tms?))) (setq data::*results* results) (setq data::*bindings* (mapcar #'car results)) (setq data::*reasons* (mapcar #'cdr results)) (unless aggressive-tms? ;; It would be redundant (dolist (result results) (install-query-reasons-in-wm (cdr result) :reasoner reasoner))) results)) (defun query (formula &key (reasoner *reasoner*) (context :any) (effort :lots) (number :all) (max-depth 10) (max-nodes 10000) (chainer nil) ; If specified, restrict search to that chainer (aggressive-tms? t)) (unless (reasoner? reasoner) ;; Extra error checking due to possible command-line usage (error "Reasoner not specified: ~A, ~A" reasoner formula)) (let ((*current-context* context) (*bc-effort* effort) (*n-answers-sought* number) (*bc-aggressive-tms?* aggressive-tms?) (*max-depth* max-depth) (*max-nodes* max-nodes)) (with-reasoner reasoner ;; Ensure available in context (cond ((conjunction? formula) (conjunctive-query (cdr formula) chainer)) (chainer (query-within-chainer formula chainer)) (t (query-all-chainers formula)))))) (defun conjunctive-query (the-conjuncts chainer) ;; We're going to be recursive here because we assume that the number of ;; conjuncts isn't going to be that huge. If it's large, then it ought ;; to be done via axioms in a chainer! (do ((conjunct (car the-conjuncts) (car conjuncts)) (conjuncts (cdr the-conjuncts) (cdr conjuncts)) (first-pass? t nil) (solutions nil extended-solutions) (extended-solutions nil nil)) ((null conjunct) solutions) (cond (first-pass? (setq extended-solutions (if (conjunction? conjunct) (conjunctive-query conjunct chainer) (if chainer (query-within-chainer conjunct chainer) (query-all-chainers conjunct))))) ((null solutions) ;; Failure -- some conjunct failed (return-from conjunctive-query nil)) (t ;; Extend current solutions (dolist (solution solutions) ;; Solution = ( . ) (let* ((this-query (sublis (car solution) conjunct)) (this-solutions (extend-query-solutions solution (cond ((conjunction? this-query) (conjunctive-query this-query chainer)) (chainer (query-within-chainer this-query chainer)) (t (query-all-chainers this-query)))))) (setq extended-solutions (nconc extended-solutions this-solutions)))))))) (defun extend-query-solutions (base-solution new-solutions) ;; Each solution is of the form ( . ) ;; We simply merge the binding lists, and join the TMS explanations with ;; the :AND keyword. (let ((bindings (car base-solution)) (explanation (cdr base-solution))) (mapcar #'(lambda (solution) (cons (append bindings (car solution)) (list :AND (cdr solution) explanation))) new-solutions))) (defun query-all-chainers (formula) (let ((results nil)) (dolist (chainer (chainers *reasoner*)) ; iterate over the reasoner's chainers (not the kb's) (let ((these-results (query-within-chainer formula chainer))) (when (and these-results (or (only-one-answer-sought?) (ground-formula? formula))) (return-from query-all-chainers these-results)) (unionf results these-results :test #'variant?))) results)) (defun query-within-chainer (formula chainer) (let ((*current-chainer* chainer)) (do-query formula *max-depth* nil))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; Backchainer inner loop ;;; The overall breakdown of chores: ;;; ;;; DO-QUERY detects if the query is locally redundant, ;;; uses ASK to see if it can be handled immediately, ;;; and otherwise gathers applicable clauses and starts ;;; iterating through them. ;;; ;;; QUERY-CLAUSE tries to answer a particular query with ;;; a given clause. It finds the appropriate order to ;;; solve the terms in, exploiting the feasibility analysis ;;; cached with the clause, computed when the clause was ;;; created to take into account dependencies introduced ;;; by reasoning sources. It uniquizes the variables, ;;; to prevent problems of variable capture. ;;; USE-SINGLE-CLAUSE-TERM handles the special case when ;;; there is only one term in a clause, and so it must ;;; be true (remember, these are DNF) ;;; EXPLORE-OTHER-TERMS loops through the other terms ;;; in the given clause, accumulating solutions for each ;;; one, generating all consistent solutions. Solving each ;;; of these terms invokes DO-QUERY, thus closing the ;;; inner loop. (defun do-query (formula max-depth stack) "Figures out if formula is true, backchaining if necessary." (cond ((some #'(lambda (parent) (variant? formula parent)) stack) nil) ; been here before ((metaknowledge-query? formula) (justify-metaknowledge-query formula max-depth stack)) (t (let ((known-answers (justify-ask formula))) ; call ask (unless (or (sufficient-answers? known-answers formula) (< max-depth 0) ; check resource constraints (< *max-nodes* 0)) ;; Backchain: (let* ((polarity (if (negation? formula) :false :true)) (predicate (formula-predicate formula)) (clauses (applicable-clauses predicate polarity *current-chainer*))) (dolist (clause-entry clauses) (let ((results (query-clause clause-entry formula (1- max-depth) stack))) (if (sufficient-answers? results formula) (return-from do-query (values results)) (unionf known-answers results :test #'variant?)))))) known-answers)))) ;;; Given a term in the term-position (e.g. the consequent) ;;; and a disjunctive clause, prove term is true. ;;; a) bind variables to chosen term ;;; (if failure, then clause doesn't apply) ;;; b) for each remaining term, prove that term *doesn't* hold ;;; (thereby proving that consequent must hold) (defun query-clause (clause-entry formula max-depth stack) ;; clause-entry = ( (..( . ) ..)) (let* ((clause (car clause-entry)) (start-term (cadr clause-entry)) (input-signature-table (third clause-entry)) (input-bindings (extract-input-bindings formula (car start-term)))) (unless (eq input-bindings :fail) (let ((term-order (retrieve-term-order input-bindings input-signature-table))) (multiple-value-bind (terms substitutions) (uniquize-variables2 (cons start-term term-order) (variables clause)) (setq start-term (car terms) term-order (cdr terms)) (let ((bindings (ltre::unify formula (car start-term)))) (unless (eq bindings :fail) ;; Now we walk down the other terms, looking to prove them ;; Recall terms is a list of ( . ) (cond ((null term-order) (use-single-term-clause formula bindings substitutions clause)) (t (explore-other-terms formula bindings clause term-order max-depth (cons formula stack) substitutions)))))))))) (defun extract-input-bindings (formula pattern) ;; Returns variables that are now bound, but in sorted order, ;; to match signatures in term ordering table (let ((bindings (ltre:unify pattern formula))) (cond ((eq bindings :fail) :fail) (t (let ((grounded (delete nil (mapcar #'(lambda (binding) (if (and (ground-formula? (cdr binding)) (contains-term? (car binding) pattern)) (car binding))) bindings)))) ;; Canonicalize order (sort grounded 'ltre::alphalessp)))))) (defun retrieve-term-order (input-signature term-ordering-table) ;; The term ordering table is a list of entries of the form ;; ( . ) ;; where the input signatures are themselves lists of which variables ;; in the term are bound at that point. ;; The variables are canonicalized for easy matching (dolist (entry term-ordering-table) (when (member input-signature (cdr entry) :test 'equal) (return-from retrieve-term-order (values (car entry)))))) (defun use-single-term-clause (formula bindings substitutions clause) ;; (declare (ignore substitutions)) ;; A bit counterintuitive, but correct ;; Don't need to invert the substitutions, just look up the answers ;; for the original variables in the formula. (let ((lifted-solution (lift-solution-from-bindings formula bindings substitutions)) (*bc-aggressive-tms?* nil)) (list (cons lifted-solution (make-conjunctive-reason formula clause lifted-solution nil))))) ;;; Keep substitutions around to incrementally instantiate expansions ;;; of quantified queries. (defun explore-other-terms (formula bindings clause terms max-depth stack substitutions) (let ((results nil)) (dolist (term-entry terms) (cond ((null results) ;; First one (let ((first-results (do-subquery term-entry clause max-depth stack substitutions t bindings))) (when (null first-results) ;; Failed on first, can't be any more (return-from explore-other-terms (values nil))) ;; Update the justifications descriptions, since ;; these are going to be conjunctives. (setq results (mapcar #'(lambda (result) (cons (car result) (list (cdr result)))) first-results)))) (t ;; Subsequent answers must be combined (let ((new-results nil)) ;; For each of the solutions accumulated so far, ;; see what consistent extensions we can find ;; for this term of the clause. (do ((solution (car results) (car other-solutions)) (other-solutions (cdr results) (cdr other-solutions))) ((null solution) ;; Now have tried extending all solutions so far ;; through this term. If we didn't get anything, ;; the clause fails, otherwise we have to look ;; at the rest (if new-results (setq results new-results) (return-from explore-other-terms (values nil)))) (let* ((local-bindings (car solution)) (new-result (do-subquery term-entry clause max-depth stack substitutions t bindings local-bindings))) ;; If this one failed, there could be others (unionf new-results (increment-solution new-result solution) :test #'variant?))))))) (lift-solutions formula clause results bindings substitutions))) ;;; Support quantifiers and structural subqueries. (defun do-subquery (term-entry clause max-depth stack substitutions flip? &rest blists) (cond ((quantified-term? (car term-entry)) (do-quantifier-query term-entry clause max-depth stack substitutions flip? blists)) (t (let ((subquery (apply #'instantiate-bindings (maybe-flip term-entry flip?) blists))) (if (structural-statement? (car term-entry)) (justify-structural-query subquery) (do-query subquery max-depth stack)))))) ;;; ;;; Metaknowledge queries ;;; (defun metaknowledge-query? (formula) (and (listp formula) (let ((pred (car formula))) (if (mixed-case?) (or (eq pred 'data::uninferredSentence) (eq pred 'data::consistentThat)) (or (eq pred 'data::uninferred-sentence) (eq pred 'data::consistent-that)))))) (defun handle-metaknowledge-query (pred formula max-depth stack) ;; metaknowledge queries always concern the belief status of some ;; formula. uninferredSentence means that one cannot derive ;; it via query. consistentThat is stronger, its negation is ;; also not believed. (ecase pred ((data::uninferredSentence data::uninferred-sentence) (let ((result (do-query formula max-depth stack))) (cond (result nil) ;; Already inferred ((ltre:false? formula) nil) ;; Already inferred (t (justify-by-timestamped-assumption (list pred formula)) (list nil))))) ;; Definitely not ((data::consistentThat data::consistent-that) (let ((result (do-query formula max-depth stack))) (cond (result result) ;; Already known ((ltre:false? formula) nil) ;; Cannot be (t (justify-by-timestamped-assumption (list pred formula)) (list nil))))))) ;; Might be ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; Quantifier queries ;;; ;;; To show (thereExists x (foo x)) ;;; 1) bind *n-answers-sought* to 1, ;;; 2) either match directly or query the subterms, ;;; 3) remove the quantified variable from the returned binding list (defun do-quantifier-query (term-entry clause max-depth stack substitutions flip? blists) (let* ((quantified-term (car term-entry)) (subs (cons (cons (var quantified-term) (gensym "?")) substitutions))) (remove-variable-from-results (var quantified-term) (or (match-directly-asserted-quantifier term-entry clause max-depth stack subs flip? blists) (prove-quantifier-expansion term-entry clause max-depth stack subs flip? blists))))) ;;; Try looking for directly asserted existential clauses: ;;; (This is ultimately just going to try to unify with facts in the kb, ;;; which will often fail because the kb is not canonicalized) (defun match-directly-asserted-quantifier (term-entry clause max-depth stack subs flip? blists) (let* ((*n-answers-sought* 1) (formula (sublis subs (form (car term-entry)))) ;; uniquify vars (subquery (apply #'instantiate-bindings formula blists)) (result (do-query subquery max-depth stack))) ;;; All right, this needs work: result)) ;;; Prove (or disprove) the existential via expansion: (defun prove-quantifier-expansion (term-entry clause max-depth stack subs flip? blists) (let* ((quantified-term (car term-entry)) (polarity (cdr term-entry)) (expansion (sublis subs (expansion quantified-term)))) ;; (format t "~%Expansion of ~S is:~%~S" (form quantified-term) expansion) ;; Bind this and do the right thing based on polarity: (with-n-answers-sought ((form quantified-term)) ; defined in macros.lsp (conj-query expansion clause max-depth stack subs flip? blists)))) ;;; Prove a conjunctive-normal-form statement ;;; This mirrors explore-other-terms (defun conj-query (cnf clause max-depth stack substitutions flip? blists) (let ((results nil)) (dolist (conj cnf) (let ((start-term (car conj))) (setq results (apply #'do-subquery start-term clause max-depth stack substitutions flip? blists)) (unless results (return-from conj-query (values nil))) (setq results (mapcar #'(lambda (result) (cons (car result) (list (cdr result)))) results)) (dolist (term (cdr conj)) (let ((new-results nil)) (do ((solution (car results) (car other-solutions)) (other-solutions (cdr results) (cdr other-solutions))) ((null solution) (if (null new-results) (return-from conj-query (values nil))) (setq results new-results)) (let* ((local-bindings (car solution)) (new-result (apply #'do-subquery term clause max-depth stack substitutions flip? local-bindings blists))) (unionf new-results (increment-solution new-result solution) :test #'variant?))))))) results)) (defun increment-solution (extensions solution) ;; Extensions is ( . ) ;; Solution is ( . ) ;; N.B. These are shared, so we must copy (mapcar #'(lambda (extension) ;; Do we need to filter for duplicates and consistency ;; of bindings? Doubt it given the substitution strategy ;; followed above. (cons (append (car extension) (car solution)) (cons (cdr extension) (cdr solution)))) extensions)) ;;; ;;; Wrappers for primitive calls ;;; (defun justify-ask (formula) (generate-query-reasons-for-ask-answers formula (ask formula *reasoner* *current-context* *n-answers-sought* :pattern *bc-effort*))) (defun justify-metaknowledge-query (formula max-depth stack) (generate-query-reasons-for-ask-answers formula (handle-metaknowledge-query (car formula) (cadr formula) max-depth stack))) (defun justify-structural-query (formula) (generate-query-reasons-for-ask-answers formula (ask-structural-statement formula *reasoner* nil nil :bindings *bc-effort*))) ;;; ;;; Creating reasons ;;; (defun generate-query-reasons-for-ask-answers (formula answers) (delete nil (mapcar #'(lambda (answer) (let ((bindings (ltre::unify formula answer))) (when (eq bindings :fail) ;; Could have been contextualized (if (case-fact? answer) (setq bindings (ltre::unify formula (third answer))))) (unless (eq bindings :fail) (cons bindings (list :WM answer))))) answers))) (defun make-conjunctive-reason (formula clause bindings antecedents) (let ((result (sublis bindings formula))) (when *bc-aggressive-tms?* (justify-kb-result-if-needed (axiom clause) *reasoner*) (ltre::assert! `(:implies (:and ,@ (mapcar 'cadr antecedents) ,(axiom clause)) ,result) :bc (ltre *reasoner*))) (cons :step (cons result (cons (list :kb (axiom clause)) ;; The KB axiom the clause was derived from antecedents))))) ;; The rest of the antecedents ;;; ;;; Installing justifications in WM ;;; (defun install-query-reasons-in-wm (explanation &key (reasoner *reasoner*)) (with-reasoner reasoner (install-query-wm-rationale explanation))) (defun install-query-wm-rationale (explanation) (cond ((or (null explanation) (not (listp explanation))) nil) ((non-ground-conclusion? explanation) nil) ;; Don't clutter LTRE with this (t (install-wm-rationale explanation)))) (defun non-ground-conclusion? (explanation) (and (listp explanation) (eq (car explanation) :step) (not (ground-formula? (cadr explanation))))) (defun install-wm-rationale (explanation) (cond ((null explanation) nil) ((not (listp explanation)) nil) (t (ecase (car explanation) (:WM ;; Already assumed to be in LTRE, so just return form so that those above ;; can use result (list (cadr explanation))) (:kb ;; Need to make an assumption (let ((form (make-in-kb-statement (cadr explanation)))) (ltre:assume! form :kb-query) (list form))) ;; Nothing to return in the and case, since no node (:AND (mapcar 'install-query-wm-rationale (cdr explanation))) (:OR (cons :or (mapcar 'install-query-wm-rationale (cdr explanation)))) (:step (let ((consequence (cadr explanation)) (antes (mapcan 'install-query-wm-rationale (cddr explanation)))) (cond ((ground-formula? consequence) ;; Assert it (ltre:assert! `(:implies (:and ,@ antes) ,consequence) :bc) (list consequence)) ;; Otherwise just pass the antecedents upwards (t antes)))))))) (defun justify-by-timestamped-assumption (conclusion) (let ((asn-form (make-timestamped-assumption conclusion))) (ltre::assume! asn-form :temporal-cwa) (ltre::assert! `(:implies ,asn-form ,conclusion) :temporal-cwa))) (defun check-backchaining-explanation (expl) (cond ((not (listp expl)) nil) ((eq (car expl) :step) (format t "~%Conclusion: ~A is ~A." (cadr expl) (ltre::label-of (cadr expl))) (dolist (step (cddr expl)) (check-backchaining-explanation step))) ((eq (car expl) :WM) (format t "~% WM: ~A is ~A." (cadr expl) (ltre::label-of (cadr expl)))) ((eq (car expl) :kb) (format t "~% kb: ~A is ~A." (cadr expl) (ltre:label-of (cadr expl)))) (t nil))) ;;; ;;; Lifting solutions ;;; (defun lift-solutions (formula clause results bindings substitutions) (let ((real-formula (if (global-context? *current-context*) formula (make-case-fact *current-context* formula)))) (mapcar #'(lambda (result) (let ((lifted-solution (lift-solution-from-bindings real-formula (append bindings (car result)) substitutions))) (cons lifted-solution (make-conjunctive-reason real-formula clause lifted-solution (cdr result))))) results))) (defun lift-solution-from-bindings (formula bindings substitutions) "Ensures solution only contains external variables." (let ((external-vars (formula-variables formula)) (solution nil)) (dolist (var external-vars) (let ((value (cdr (assoc var bindings)))) (if (null value) ;; Something badly wrong (error "Variable not bound in solution: ~A in ~A, ~A." var formula bindings) (let ((variable-value (lift-variable-value value bindings external-vars substitutions))) (if variable-value (push (cons var variable-value) solution) ;; If variable-value is nil, then this is a variable ;; that binds to another variable, ignore, since all ;; free variables universally quantified. PKP, 01/08/04 ))))) solution)) (defun lift-variable-value (value binding-list external-vars substitutions) "Remove internal variables by looking them up on binding list" (cond ((null value) nil) ((member value external-vars) value) ;; Stop here ((variable? value) (cond ((member value external-vars) ;; Stop here value) ;; We need both assoc and rassoc checks here in case both ;; are variables unify doesnt promise any particular order. (t (let ((indirect-value (assoc value binding-list))) (cond ((null indirect-value) (setq indirect-value (rassoc value substitutions)) (if (null indirect-value) (error "No binding for internal variable: ~A, ~A, ~A." value binding-list external-vars)) ;; If the internal variable is bound to a variable, then ;; we just drop it from the solution as in the solution we ;; want to give bindings for variables. Free variables are ;; universally quantified. [PKP, 01/08/04] (if (variable? indirect-value) nil)) (t (lift-variable-value (cdr indirect-value) binding-list external-vars substitutions))))))) ((consp value) (cons (lift-variable-value (car value) binding-list external-vars substitutions) (lift-variable-value (cdr value) binding-list external-vars substitutions))) (t value))) ;;; ;;; Helpers ;;; ;;; Somehow it seems like this isn't quite what we want. Shouldn't we cut off ;;; backchaining when there are *num-answers-sought* answers? (defun sufficient-answers? (answers formula) (and answers (or (only-one-answer-sought?) ;; Got at least one (ground-formula? formula)))) ;; There can be only one (defun only-one-answer-sought? () (eql *n-answers-sought* 1)) ;;; Flip polarity to prove disjunct doesn't hold (defun maybe-flip (term-entry flip?) (if (and flip? (eq (cdr term-entry) :true)) (make-negation (car term-entry)) (car term-entry))) ;;; Instantiate expression with an arbitrary number of binding lists: (defun instantiate-bindings (expr &rest binding-lists) (mapc #'(lambda (blist) (setq expr (sublis blist expr))) binding-lists) expr) ;;; Delete locally-scoped quantified variables from a blist (defun remove-variable-from-results (var results) (mapcar #'(lambda (result) (cons (remove var (car result) :key #'first) (cdr result))) results)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; Debugging and shakedown procedures ;;; ;;; For shakedowns, see qrg\Fire\v1\Tests\chainer-regression, ;;; or for independent tests, see bc-logic-tests, TOU-tests & quantification-tests. (defun cl-user::trace-backchainer () (trace query conjunctive-query do-query do-subquery query-clause use-single-term-clause explore-other-terms justify-metaknowledge-query sufficient-answers? applicable-clauses formula-predicate justify-metaknowledge-query do-quantifier-query increment-solution justify-ask install-wm-rationale lift-solutions)) (defun cl-user::untrace-backchainer () (untrace query conjunctive-query do-query do-subquery query-clause use-single-term-clause explore-other-terms justify-metaknowledge-query sufficient-answers? applicable-clauses formula-predicate justify-metaknowledge-query do-quantifier-query increment-solution justify-ask install-wm-rationale lift-solutions)) ;;; End of Code