Filtering...

soundness

books/projects/sat/lrat/stobj-based/soundness
other
(in-package "LRAT")
other
(include-book "lrat-checker")
other
(local (include-book "../list-based/soundness"))
other
(local (include-book "equiv"))
other
(defthm refutation-p-equiv
  (implies (and (formula-p formula)
      (refutation-p$ proof formula))
    (refutation-p proof formula)))
other
(defthm main-theorem-stobj-based
  (implies (and (formula-p formula)
      (refutation-p$ proof formula))
    (not (satisfiable formula)))
  :hints (("Goal" :in-theory '(refutation-p-equiv)
     :use main-theorem-list-based)))