diff options
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) + ) |