# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597454335 -32400
# Node ID 17cd0e70e931ae2694667edffa08377bb9e458ab
# Parent  edf4a816abffdcd090d91eda7b366c129547cd91
add clausal form transformation

diff -r edf4a816abff -r 17cd0e70e931 Logic.agda
--- a/Logic.agda	Thu Aug 13 18:44:09 2020 +0900
+++ b/Logic.agda	Sat Aug 15 10:18:55 2020 +0900
@@ -6,7 +6,7 @@
    var   : Var → Expr 
    func  : Func → Expr → Expr 
    const : Const → Expr 
-   _,_ : Expr →Expr → Expr 
+   _,_ : Expr → Expr → Expr 
 
 data Statement : Set where
    pred       : Pred  → Statement 
diff -r edf4a816abff -r 17cd0e70e931 clausal.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/clausal.agda	Sat Aug 15 10:18:55 2020 +0900
@@ -0,0 +1,117 @@
+module clausal (Const Func Var Pred : Set)  where
+open import Data.List hiding (all ; and ; or )
+open import Data.Bool hiding ( not )
+open import Function
+
+open import Logic Const Func Var Pred 
+
+-- data Expr  : Set  where
+--    var   : Var → Expr 
+--    func  : Func → Expr → Expr 
+--    const : Const → Expr 
+--    _,_ : Expr →Expr → Expr 
+
+-- data Statement : Set where
+--    pred       : Pred  → Statement 
+--    predx  : Pred  → Expr → Statement 
+--    _/\_   : Statement → Statement  → Statement 
+--    _\/_         : Statement → Statement  → Statement 
+--    ¬_         : Statement  → Statement 
+--    All_=>_        : Var → Statement → Statement 
+--    Exist_=>_      : Var → Statement → Statement 
+
+-- make negations on predicates only
+negin1  : Statement → Statement
+
+negin  : Statement → Statement
+negin (pred x) = pred x
+negin (predx x x₁) = predx x x₁
+negin (s /\ s₁) = negin s /\ negin s₁
+negin (s \/ s₁) = negin s \/ negin s₁
+negin (¬ s) = negin1 s
+negin (All x => s) = All x => negin s
+negin (Exist x => s) = Exist x => negin s
+
+negin1 (pred x) = ¬ (pred x)
+negin1 (predx x x₁) = ¬ (predx x x₁)
+negin1 (s /\ s₁) = negin1 s \/ negin1 s₁
+negin1 (s \/ s₁) = negin1 s /\ negin1 s₁
+negin1 (¬ s) = negin s
+negin1 (All x => s) = (Exist x => negin1 s )
+negin1 (Exist x => s) = (All x => negin1 s)
+
+-- remove existential quantifiers using sokem functions
+--    enough unused functions and constants for skolemization necessary
+--    assuming non overrupping quantified variables
+
+record Skolem : Set where
+   field 
+     st : Statement
+     cl : List Const
+     fl : List Func
+     vr : List Var
+
+{-# TERMINATING #-} 
+skolem  : List Const → List Func → (sbst : Expr  → Var →  Expr  → Expr  ) → Statement → Statement
+skolem cl fl sbst s = Skolem.st (skolemv record { st = s ; cl = cl ; fl = fl ; vr = [] })  where
+   skolemv : Skolem → Skolem
+   skolemv S with Skolem.vr S | Skolem.st S 
+   skolemv S | v | All x => s  = record S1 { st = All x => Skolem.st S1 } where
+        S1 : Skolem 
+        S1 = skolemv record S { st = s ;  vr = x ∷ v } 
+   skolemv S | [] | (Exist x => s) with Skolem.cl S
+   ... | [] = S
+   ... | sk ∷ cl = skolemv record S { st = subst-prop s sbst x (Expr.const sk) ; cl = cl }
+   skolemv S | (v ∷ t) | (Exist x => s)  with Skolem.fl S
+   ... | [] = S
+   ... | sk ∷ fl = skolemv record S { st = subst-prop s sbst x (func sk (mkarg v t )) ; fl = fl }  where
+      mkarg : (v : Var) (vl : List Var ) → Expr
+      mkarg v []  = var v
+      mkarg v (v1 ∷ t )  = var v , mkarg v1 t
+   skolemv S | v | s /\ s₁ = record S2 { st = Skolem.st S1 /\ Skolem.st S2 }  where
+        S1 = skolemv record S {st = s}
+        S2 = skolemv record S1 {st = s₁}
+   skolemv S | v | s \/ s₁ = record S2 { st = Skolem.st S1 \/ Skolem.st S2 }  where
+        S1 = skolemv record S {st = s}
+        S2 = skolemv record S1 {st = s₁}
+   skolemv S | _ | _ = S
+
+-- remove universal quantifiers
+univout  : Statement → Statement
+univout (s /\ s₁) = univout s /\ univout s₁
+univout (s \/ s₁) = univout s \/ univout s₁
+univout x = x
+
+-- move disjunctions inside
+{-# TERMINATING #-} 
+conjn1  : Statement → Statement
+
+{-# TERMINATING #-} 
+conjn  : Statement → Statement
+conjn (s /\ s₁) = conjn s /\ conjn s₁
+conjn (s \/ s₁) = conjn1 ( ( conjn s ) \/ ( conjn s₁) )
+conjn x = x
+
+conjn1 ((x /\ y) \/ z) = conjn (x \/ y) /\ conjn (x \/ z )
+conjn1 (z \/ (x /\ y)) = conjn (z \/ x) /\ conjn (z \/ y )
+conjn1 x = x
+
+data Clause  : Set where
+   _:-_ : ( x y : List Statement ) → Clause
+
+-- turn into [ [  [ positive ] :- [ negative ] ]
+--   to remove overraps, we need equality
+clausify : Statement → List Clause
+clausify s = clausify1 s [] where
+   inclause : Statement → Clause → Clause
+   inclause (x \/ y ) a  = inclause x ( inclause y a ) 
+   inclause (¬ x) (a :- b )  = a :- ( x ∷ b ) 
+   inclause  x (a :- b)   = ( x ∷ a ) :- b  
+   clausify1 : Statement → List Clause → List Clause
+   clausify1 (x /\ y) c =  clausify1 y (clausify1 x c )
+   clausify1 x c = inclause x ([] :- [] ) ∷ c
+
+translate : Statement → List Const → List Func  →  (sbst : Expr  → Var →  Expr  → Expr  ) →  List Clause
+translate s cl fl sbst = clausify $ conjn $ univout $ skolem cl fl sbst $ negin s
+
+