diff options
author | Camm Maguire <camm@debian.org> | 2017-05-08 12:58:52 -0400 |
---|---|---|
committer | Camm Maguire <camm@debian.org> | 2017-05-08 12:58:52 -0400 |
commit | 092176848cbfd27b96c323cc30c54dff4c4a6872 (patch) | |
tree | 91b91b4db76805fd2a09de0745b22080a9ebd335 /books/workshops/1999/ivy/ivy-v2/ivy-sources/exercises/exercise4.lsp |
Import acl2_7.4dfsg.orig.tar.gz
[dgit import orig acl2_7.4dfsg.orig.tar.gz]
Diffstat (limited to 'books/workshops/1999/ivy/ivy-v2/ivy-sources/exercises/exercise4.lsp')
-rw-r--r-- | books/workshops/1999/ivy/ivy-v2/ivy-sources/exercises/exercise4.lsp | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/books/workshops/1999/ivy/ivy-v2/ivy-sources/exercises/exercise4.lsp b/books/workshops/1999/ivy/ivy-v2/ivy-sources/exercises/exercise4.lsp new file mode 100644 index 0000000..5b94757 --- /dev/null +++ b/books/workshops/1999/ivy/ivy-v2/ivy-sources/exercises/exercise4.lsp @@ -0,0 +1,32 @@ +;; Exercise file to accompany +;; +;; Ivy: A Preprocessor and Proof Checker for First-order Logic +;; +;; William McCune (mccune@mcs.anl.gov) +;; Olga Shumsky (shumsky@ece.nwu.edu) +;; +;; Startup file for exercise 4. +;; +;; Define a resolution function that takes two formulas and +;; two specifications of subformulas within the formulas, +;; and computes a resolvent, if possible, of the two formulas +;; on the specified literals. +;; +;; Prove that the function is sound. + +;; All neccesary definitions are in: +(include-book "../base") + +;; Hint: the following lemma might be useful: +(encapsulate + nil + (local (include-book "../close")) + (defthm feval-alls-subset + (implies (and (var-set a) + (var-set b) + (subsetp-equal a b) + (not (free-vars (alls a f)))) + (equal (feval (alls a f) i) + (feval (alls b f) i))) + :rule-classes nil) + ) |