;; -*- Mode: Lisp; Syntax: Common-Lisp; Package: snark-user -*- ;; iw-snark.lisp ;; Bill MacCartney ;; bmac@ksl.stanford.edu ;; 9 May 2002 (when (eq cl-user::*current-case-mode* :case-sensitive-lower) (set-case-mode :|case-insensitive-upper|)) ;; Load Snark (load "snark-system") (snark:make-snark-system) ;;(snark:make-snark-system t) ; use this if .fasl files missing (in-package :snark-user) (default-use-resolution) ; set SNARK options (default-assert-supported nil) (initialize) ;; Load AllegroServe for HTTP access (require :aserve) (use-package '(net.aserve.client)) (defparameter *publish-uri* "http://www.ksl.stanford.edu/software/iw/snark/") (defparameter *publish-path* "/ksl/u9/projects/ksl/web/software/IW/snark/") (defvar *example* 'hd) (defun test (&optional (example 'hd)) (setf *example* example) (funcall (case example ('hd #'hd-example) ('fred #'fred-example) ('nuke #'nuke-example) )) ; run a proof (dolist (row (row-ancestry (proof))) (create-proof-node row) )) (defun create-proof () (multiple-value-bind (body response-code headers uri) (do-http-request "http://belo.stanford.edu:8080/iwregistrar/CreateProof" :method :post :query '(("InferenceEngine" . "SNARK") ("PublishingURL" . *publish-uri*))) (format t "~&~S~&" body) )) (defun create-proof-node (row) (let* ((number (row-number row)) (filename (filename-from-number number)) (uri (uri-from-number number)) (formula (format nil "~S" (or (row-input-wff row) (term-to-lisp (row-wff row))))) (reason (row-reason row)) (rewrites-used (row-rewrites-used row)) (rule (if (listp reason) (first reason) reason)) (antecedent-numbers (if (listp reason) (mapcar #'row-number (append (cdr reason) rewrites-used)) NIL)) (inf-rule (cond ((member rule '(RESOLVE REWRITE)) (if (eq 2 (length antecedent-numbers)) "Bi-Resolution" "Hyp-Resolution")) ((eq rule 'ASSERTION) "Told") ((eq rule 'ASSUMPTION) "Assumption") ((eq rule '~CONCLUSION) "NegConc"))) (antecedent-uris "") (ontology (if (eq (row-source row) 'nuke) "nuke" "")) ) (dolist (antecedent antecedent-numbers) (setf antecedent-uris (format nil "~A,~A" antecedent-uris (uri-from-number antecedent)))) (format t "~&--------------") (format t "~&number: ~S" number) (format t "~&filename: ~S" filename) (format t "~&uri: ~S" uri) (format t "~&formula: ~S" formula) (format t "~&reason: ~S" reason) (format t "~&rewrites-used: ~S" rewrites-used) (format t "~&rule: ~S" rule) (format t "~&antecedent-numbers: ~S" antecedent-numbers) (format t "~&inf-rule: ~S" inf-rule) (format t "~&antecedent-uris: ~S" antecedent-uris) (format t "~&ontology: ~S" ontology) (when t ; so i can turn this block off for testing (multiple-value-bind (body response-code headers uri2) (do-http-request "http://belo.stanford.edu:8080/iwregistrar/CreateProofNode" :method :post :query `(("InferenceEngine" . "SNARK") ("Statement" . ,formula) ("URI" . uri) ("InferenceRule" . ,inf-rule) ("Antecedent". ,antecedent-uris) ("Ontology". ,ontology) )) (format t "~&~S~&" body) (with-open-file (stream (make-pathname :directory *publish-path* :name filename) :direction :output :if-exists :supersede :if-does-not-exist :create) (format stream "~A" body)) )) )) (defun filename-from-number (number) (format nil "~S~D.daml" *example* number)) (defun uri-from-number (number) (let ((filename (filename-from-number number))) (format nil "~A~A" *publish-uri* filename))) #| Date: Wed, 7 May 2003 13:22:05 -0700 (PDT) From: Paulo Pinheiro da Silva To: Bill MacCartney Subject: Re: services for generating IW proofs Some conventions in the following specification: 1) Parameters are of type String. 2) Terms between quotas are keywords. 3) Parameters with an [opt] are optional. 4) The order of the parameters is irrelevant for the services. 5) Returned values are tagged by their corresponding keywords. ----------------------------------------------------------------------------- Service: CreateProof Parameters: 'InferenceEngine' - The ID of a registered inference engine, e.g., 'SNARK' for SNARK. Return: 'Result' - one of the following messages: 'OK' for a correct request. 'INVALID INFERENCE ENGINE" if not registered inference engine has the specified InferenceEngine ID. 'InferenceRule' - List of IDs of inference rules related to the selected inference engine. Example: The submission of http://belo.stanford.edu:8080/iwregistrar/CreateProof?InferenceEngine=SNARK produces the following output OKDemodulationResolution ----------------------------------------------------------------------------- Service: CreateProofNode Parameters: 'Statement' - a sentence in KIF labeling the current node. 'URI' - URI of the current node. 'InferenceRule' - one of the rule IDs returned by the CreateProof service. 'Antecedent'[opt] - a list of the URIs of premises for the current node, if any. Indeed, the statement in the node is considered an assertion if no antecedent is provided. 'Bindings'[opt] - A list of pair of variable bindings for the current node. No binding is expected for assertions. Variables should be prefixed by a question mark. Variables come first in the pair 'Ontology'[opt] - A list of URIs of ontologies containing the current statement, if any. Ontologies should have an entry in the registry in order to be linked to the proof during browsing. Description: In the current context, the reasoner provides the attributes requered for generating a proof node and the service returns the proof node in the IW format. Inconsistencies of the proof node with respect to the current registry are identified by the service. Return: 'Result' - one of the following messages: 'OK' for a correct generated proof 'INVALID PARAMETER' if any parameter is invalid. 'INVALID INFERENCE RULE' if the rule is not in the provided list of rules. 'INVALID ONTOLOGY' if the ontology URI is not in the registry. 'NodeContent' - the proof node in the IW format. ----------------------------------------------------------------------------- |# (defun fred-example () (initialize) (use-clausification nil) (mapc #'(lambda (form) (assert form :source 'fred)) '( (instance Living AnimacyAttribute) (subclass AnimacyAttribute BiologicalAttribute) (<=> (subclass ?SUBCLASS ?CLASS) (and (instance ?SUBCLASS SetOrClass) (instance ?CLASS SetOrClass) (forall (?INST) (=> (instance ?INST ?SUBCLASS) (instance ?INST ?CLASS))))) (=> (and (attribute ?ORG ?ATT) (instance ?ATT BiologicalAttribute)) (instance ?ORG Organism)) )) (assume '(attribute Fred Living)) (prove '(instance Fred Organism)) ) (defun hd-example () (initialize) (use-clausification) (mapcar #'declare-proposition-symbol '(ok_pump on_pump man_fill water ok_boiler on_boiler steam coffee teabag hot_drink)) (mapc #'(lambda (form) (assert form :source 'hd)) '((implies (and ok_pump on_pump) water) (implies man_fill water) (implies man_fill (not on_pump)) (implies (not man_fill) on_pump) (implies (and water ok_boiler on_boiler) steam) (implies (not water) (not steam)) (implies (not ok_boiler) (not steam)) (implies (not on_boiler) (not steam)) (implies (and steam coffee) hot_drink) (implies (and steam teabag) hot_drink) (or coffee teabag) )) (assume '(and ok_pump ok_boiler on_boiler)) (prove 'hot_drink) ) (defun nuke-example () (initialize) (use-clausification) (mapcar #'declare-proposition-symbol '(refiner uranium-ore black-mkt-source nuclear-material detonator casing warhead missile truck nuclear-threat)) (mapc #'(lambda (form) (assert form :source 'nuke)) '((implies (and refiner uranium-ore) nuclear-material) (implies black-mkt-source nuclear-material) (or black-mkt-source uranium-ore) (implies (and nuclear-material detonator casing) warhead) (implies (not nuclear-material) (not warhead)) (implies (not detonator) (not warhead)) (implies (not casing) (not warhead)) (implies (and warhead missile) nuclear-threat) (implies (and warhead truck) nuclear-threat) (or missile truck) )) (assume '(and refiner detonator casing)) (prove 'nuclear-threat) )