← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/1999/ivy/ivy-v2/ivy-sources/modeler.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/1999/ivy/ivy-v2/ivy-sources/modeler.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;; This book contains the top definitions and soundness theorems for
 
4
;; the model and countermodel procedures.  This book is analogous
 
5
;; to a combination of the refute-n-check and prover books for the
 
6
;; refutation procedure, but it is much simpler, because the soundness
 
7
;; proof here is trivial.
 
8
 
 
9
(include-book "nnf")            ; nnf
 
10
(include-book "rename-top")     ; rename-all
 
11
(include-book "skolem-top")     ; skolemize
 
12
(include-book "cnf")            ; cnf
 
13
(include-book "pull-top")       ; pull-quants
 
14
 
 
15
(include-book "derive")
 
16
 
 
17
(defstub external-modeler (clauses) t)
 
18
 
 
19
;; Function model-attempt is analogous to a combination of
 
20
;; refute-n-check and refutation-attempt.  We compose all of the
 
21
;; preprocessing steps, build an initial proof object, and
 
22
;; call external-modeler, and check the result.
 
23
 
 
24
(defun model-attempt (f)
 
25
  (declare (xargs :guard (and (wff f) (not (free-vars f)))))
 
26
  (if (not (and (wff f) (not (free-vars f))))
 
27
      nil
 
28
    (let* ((preprocessed
 
29
            (cnf
 
30
             (pull-quants (skolemize (rename-all (nnf f))))))
 
31
           (mace-result
 
32
            (external-modeler
 
33
             (assign-ids-to-prf
 
34
              (initial-proof
 
35
               (remove-leading-alls preprocessed)) 1))))
 
36
      (if (feval f mace-result)
 
37
          mace-result
 
38
        nil))))
 
39
 
 
40
;; This "soundness" proof is really trivial, because model-attempt
 
41
;; checks MACE's answer by calling feval.
 
42
 
 
43
(defthm model-attempt-fsound  ;; Top Theorem #3
 
44
  (implies (model-attempt f)
 
45
           (and (wff f)
 
46
                (not (free-vars f))
 
47
                (feval f (model-attempt f)))))
 
48
 
 
49
(in-theory (disable model-attempt))
 
50
 
 
51
;; Now state it positively.  That is, if we find a model of the negation
 
52
;; of a formula, then we have a countermodel of the formula.
 
53
;; This is a top function, so check the guard.
 
54
 
 
55
(defun countermodel-attempt (f)
 
56
  (declare (xargs :guard (and (wff f) (not (free-vars f)))))
 
57
  (if (not (and (wff f) (not (free-vars f))))
 
58
      nil
 
59
    (model-attempt (list 'not f))))
 
60
 
 
61
(defthm countermodel-attempt-fsound  ;; Top Theorem #4
 
62
  (implies (countermodel-attempt f)
 
63
           (and (wff f)
 
64
                (not (free-vars f))
 
65
                (not (feval f (countermodel-attempt f)))))
 
66
  :hints (("Goal"
 
67
           :in-theory (enable model-attempt))))
 
68
 
 
69
(in-theory (disable countermodel-attempt))
 
70