; Resolution theorem proving
;
; Traditional resolution theorem provers maintain a clause database
; of formulas in Conjunction Normal Form (CNF a big And of Ors).
; Each clause is a set of positive and negative literals
; The prover saturates this set by taking two clauses
; {a}\/c1 {not a}\/c2 and creating a new clause c1 \/ c2.
; Clauses also are pruned by simplications, unit propagation,
; and subsumption.
; These systems use sophisticated term indexing to find matching clauses
; A natural question is whether egglog's saturation and term indexing gives
; a leg up towards building one of these systems. A programmable one even,
; with built in support for equality reasoning
; Resolution is provided by a join
; unit propagation is an equation solving process and egraph substitution
; Clause Simplification is provided by rewrite rules
; This encoding seems about right but is unsatisfying
; Using AC to encode the set nature of clauses is inefficient
; An important aspect of these provers that seems challenging to encode shallowly
; is that the match also occurs modulo _unification_.
; The unification variables of each clause are not globally scoped, really
; they are scoped outside the body of each clase in an implicit \forall
; This encoding as it stands really only supports ground atoms modulo equality
(datatype Bool)
(constructor TrueConst () Bool)
(let $True (TrueConst))
(constructor FalseConst () Bool)
(let $False (FalseConst))
(constructor myor (Bool Bool) Bool)
(constructor negate (Bool) Bool)
; clauses are assumed in the normal form (or a (or b (or c False)))
(union (negate $False) $True)
(union (negate $True) $False)
; "Solving" negation equations
(rule ((= (negate p) $True)) ((union p $False)))
(rule ((= (negate p) $False)) ((union p $True)))
; canonicalize associtivity. "append" for clauses
; terminate with false
(rewrite (myor (myor a b) c) (myor a (myor b c)))
; commutativity
(rewrite (myor a (myor b c)) (myor b (myor a c)))
;absorption
(rewrite (myor a (myor a b)) (myor a b))
(rewrite (myor a (myor (negate a) b)) $True)
; simplification
(rewrite (myor $False a) a)
(rewrite (myor a $False) a)
(rewrite (myor $True a) $True)
(rewrite (myor a $True) $True)
; unit propagation
; This is kind of interesting actually.
; Looks a bit like equation solving
(rewrite p $True
:when ((= $True (myor p $False))))
(rule ((= $True (myor p $False))) ((union p $True)))
; resolution
; This counts on commutativity to bubble everything possible up to the front of the clause.
(rule ((= $True (myor a as)) (= $True (myor (negate a) bs)))
((union (myor as bs) $True)))
; example predicate
(constructor p (i64) Bool)
(let $p0 (p 0))
(let $p1 (p 1))
(let $p2 (p 2))
;(union (or $p0 (or $p1 (or $p2 $False))) $True)
;(union (or (negate $p0) (or $p1 (or (negate $p2) $False))) $True)
(union (myor $p1 (myor (negate $p2) $False)) $True)
(union (myor $p2 (myor (negate $p0) $False)) $True)
(union (myor $p0 (myor (negate $p1) $False)) $True)
(union $p1 $False)
(union (myor (negate $p0) (myor $p1 (myor $p2 $False))) $True)
(run 10)
(check (!= $True $False))
(check (= $p0 $False))
(check (= $p2 $False))
; we could turn the original axioms into _patterns_ in all possible directions.
; Which is kind of compelling
; (rule ((or (pat x))) )
; or let a unification expansion happen and use thos