# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598070852 -32400
# Node ID 6cd5b63ecc38b188429389da41b41cceef267364
# Parent  76e93314915195f88008ef9a0a3b0038c85c3fb5
replace syntax

diff -r 76e933149151 -r 6cd5b63ecc38 Logic.agda
--- a/Logic.agda	Sat Aug 15 17:15:14 2020 +0900
+++ b/Logic.agda	Sat Aug 22 13:34:12 2020 +0900
@@ -3,29 +3,19 @@
 open import Data.Bool hiding ( not ; _∧_ ; _∨_ )
 
 data Expr  : Set  where
-   var   : Var → Expr 
-   func  : Func → Expr → Expr 
+   var   : Var   → Expr 
+   func  : Func  → Expr → Expr 
    const : Const → Expr 
-   _,_ : Expr → Expr → 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 
-
---   Exprindepenent variable substituion using dependent substution (sbst)
-subst-prop :  (e : Statement  ) → (sbst : Expr  → Var →  Expr  → Expr  )  → Var → Expr → Statement 
-subst-prop (pred x) sbst xv v = pred x
-subst-prop (predx x x₁) sbst xv v = predx x ( sbst x₁ xv v )
-subst-prop (e ∧ e₁) sbst xv v = ( subst-prop e sbst xv v ) ∧ ( subst-prop e₁ sbst xv v )
-subst-prop (e ∨ e₁) sbst xv v = ( subst-prop e sbst xv v ) ∨ ( subst-prop e₁ sbst xv v )
-subst-prop (¬ e) sbst xv v = ¬ ( subst-prop e sbst xv v )
-subst-prop (All x => e) sbst xv v = All x => ( subst-prop e sbst xv v )
-subst-prop (Exist x => e) sbst xv v = Exist x => ( subst-prop e sbst xv v )
+   pred       : Pred      → Statement 
+   predx      : Pred      → Expr      → Statement 
+   _∧_        : Statement → Statement → Statement 
+   _∨_        : Statement → Statement → Statement 
+   ¬_         : Statement → Statement 
+   All_=>_    : Var       → Statement → Statement 
+   Exist_=>_  : Var       → Statement → Statement 
 
 --
 -- The interpretation
@@ -34,22 +24,35 @@
 --
 {-# TERMINATING #-} 
 M : (amap :  Pred  → Bool ) (pmap :  Pred → Expr → Bool )
-   →  (all-const   : List Expr )
-   →  (sbst : Expr  → Var →  Expr  → Expr  )
+   → (all-const   : List Expr )
+   → (sbst : Expr  → Var →  Expr  → Expr  )
    → Statement  → Bool
 M amap pmap all0 sbst s = m s where
+
+   --   Expr indepenent variable substituion using Expr substution (sbst)
+   _[_/_] :  (e : Statement  ) → Var → Expr → Statement 
+   (pred x) [ xv / v ]     = pred x
+   (predx x x₁) [ xv / v ] = predx x ( sbst x₁ xv v )
+   (e ∧ e₁) [ xv / v ]     = (  e [ xv / v ]) ∧ (  e₁ [ xv / v ])
+   (e ∨ e₁) [ xv / v ]     = (  e [ xv / v ]) ∨ (  e₁ [ xv / v ])
+   (¬ e) [ xv / v ]        = ¬ (  e [ xv / v ])
+   (All x => e) [ xv / v ]   = All x =>   (  e [ xv / v ])
+   (Exist x => e) [ xv / v ] = Exist x => (  e [ xv / v ])
+
    m :  Statement  → Bool
-   m (pred x) = amap x
+   m (pred x)     = amap x
    m (predx x x₁) = pmap x x₁
-   m (s ∧ s₁) = m s  Data.Bool.∧ m s₁ 
-   m (s ∨ s₁) = m s Data.Bool.∨ m s₁ 
-   m (¬ s) = Data.Bool.not (m s )
+   m (s ∧ s₁)     = m s  Data.Bool.∧ m s₁ 
+   m (s ∨ s₁)     = m s Data.Bool.∨ m s₁ 
+   m (¬ s)        = Data.Bool.not (m s )
+   -- an esasy emulation of quantifier using a variable free expr list
    m (All x => s) = m-all all0 x s  where
-     m-all :  List Expr → Var → Statement → Bool
-     m-all [] vx s = true
-     m-all (x ∷ t) vx s = m (subst-prop s sbst vx x ) Data.Bool.∧ m-all t vx s
+     m-all   : List Expr → Var → Statement → Bool
+     m-all   [] vx s = true
+     m-all   (x ∷ t) vx s = m ( s [ vx / x ]) Data.Bool.∧ m-all   t vx s
    m (Exist x => s) = m-exist all0 x s  where
-     m-exist :  List Expr → Var  → Statement → Bool
+     m-exist : List Expr → Var → Statement → Bool
      m-exist [] vx s = false
-     m-exist (x ∷ t) vx s = m (subst-prop s sbst vx x ) Data.Bool.∨ m-exist t vx s
+     m-exist (x ∷ t) vx s = m ( s [ vx / x ] ) Data.Bool.∨ m-exist t vx s
 
+
diff -r 76e933149151 -r 6cd5b63ecc38 clausal.agda
--- a/clausal.agda	Sat Aug 15 17:15:14 2020 +0900
+++ b/clausal.agda	Sat Aug 22 13:34:12 2020 +0900
@@ -47,14 +47,24 @@
 {-# TERMINATING #-} 
 skolem  : List Const → List Func → (sbst : Expr  → Var →  Expr  → Expr  ) → Statement → Statement
 skolem cl fl sbst s = skolemv1 ( λ s cl fl vr → s ) s cl fl []  where
+   --   Expr indepenent variable substituion using Expr substution (sbst)
+   _[_/_] :  (e : Statement  ) → Var → Expr → Statement
+   (pred x) [ xv / v ]     = pred x
+   (predx x x₁) [ xv / v ] = predx x ( sbst x₁ xv v )
+   (e ∧ e₁) [ xv / v ]     = (  e [ xv / v ]) ∧ (  e₁ [ xv / v ])
+   (e ∨ e₁) [ xv / v ]     = (  e [ xv / v ]) ∨ (  e₁ [ xv / v ])
+   (¬ e) [ xv / v ]        = ¬ (  e [ xv / v ])
+   (All x => e) [ xv / v ]   = All x =>   (  e [ xv / v ])
+   (Exist x => e) [ xv / v ] = Exist x => (  e [ xv / v ])
+
    skolemv1 : (Statement → List Const → List Func → List Var → Statement )
              → Statement → List Const → List Func → List Var → Statement
    skolemv1 next (All x => s )   cl fl vl              = skolemv1 next s cl fl ( x ∷ vl) 
    -- all existential quantifiers are replaced by constants or funcions
    skolemv1 next (Exist x => s ) [] fl []              = skolemv1 next s [] fl [] 
-   skolemv1 next (Exist x => s ) (sk ∷ cl ) fl []      = skolemv1 next (subst-prop s sbst x (Expr.const sk)) cl fl [] 
+   skolemv1 next (Exist x => s ) (sk ∷ cl ) fl []      = skolemv1 next (s [ x / (Expr.const sk) ] ) cl fl [] 
    skolemv1 next (Exist x => s ) cl [] (v ∷ t)         = skolemv1 next s cl [] (v ∷ t)
-   skolemv1 next (Exist x => s ) cl (sk ∷ fl) (v ∷ t)  = skolemv1 next (subst-prop s sbst x (func sk (mkarg v t) )) cl fl (v ∷ t)  where
+   skolemv1 next (Exist x => s ) cl (sk ∷ fl) (v ∷ t)  = skolemv1 next (s [ x / (func sk (mkarg v t) ) ] ) cl fl (v ∷ t)  where
       mkarg : (v : Var) (vl : List Var ) → Expr
       mkarg v []  = var v
       mkarg v (v1 ∷ t )  = var v , mkarg v1 t
diff -r 76e933149151 -r 6cd5b63ecc38 example1.agda
--- a/example1.agda	Sat Aug 15 17:15:14 2020 +0900
+++ b/example1.agda	Sat Aug 22 13:34:12 2020 +0900
@@ -48,11 +48,11 @@
 all0   :  List Expr
 all0 =  const a ∷ const b ∷ const c ∷ []
 
-test003 : Bool 
-test003 = M amap pmap all0 subst-expr ( Exist X => predx p (var X)  )
+test3 : Bool 
+test3 = M amap pmap all0 subst-expr ( Exist X => predx p (var X)  )
 
 open import clausal Const Func Var Pred 
 
-test004 : List Clause
-test004 = translate ( Exist X => predx p (var X) ) (c ∷ []) (h ∷ []) subst-expr
+test4 : List Clause
+test4 = translate ( Exist X => predx p (var X) ) (c ∷ []) (h ∷ []) subst-expr
 
diff -r 76e933149151 -r 6cd5b63ecc38 example2.agda
--- a/example2.agda	Sat Aug 15 17:15:14 2020 +0900
+++ b/example2.agda	Sat Aug 22 13:34:12 2020 +0900
@@ -87,3 +87,6 @@
 
 test7 : List Clause
 test7 = translate ex1 [] [] subst-expr  
+
+-- brother (X , Y) :- father (X , Z) , father (Y , Z)
+
diff -r 76e933149151 -r 6cd5b63ecc38 simple-logic.agda
--- a/simple-logic.agda	Sat Aug 15 17:15:14 2020 +0900
+++ b/simple-logic.agda	Sat Aug 22 13:34:12 2020 +0900
@@ -37,15 +37,15 @@
 subst-expr (x , y ) n v = (subst-expr x n v) , (subst-expr y n v) 
 subst-expr x  n v = x 
 
-subst-prop : (orig : Statement ) → Var → (value : Expr ) → Statement
-subst-prop (p x ) n v = p ( subst-expr x n v )
-subst-prop q n v = q
-subst-prop r n v = r
-subst-prop (x ∧ y) n v = subst-prop x n v ∧ subst-prop x n v
-subst-prop (x ∨ y) n v = subst-prop x n v ∨ subst-prop x n v
-subst-prop (¬ x) n v = ¬ (subst-prop x n v )
-subst-prop (all x => y) n v = all x => subst-prop y n v 
-subst-prop (∃ x => y) n v =  ∃ x => subst-prop y n v 
+_[_/_]  : (orig : Statement ) → Var → (value : Expr ) → Statement
+(p x ) [ n / v ] = p ( subst-expr x n v )
+q [ n / v ] = q
+r [ n / v ] = r
+(x ∧ y) [ n / v ] = (x [ n / v ] ) ∧  (x [ n / v ])
+(x ∨ y) [ n / v ] = (x [ n / v ] ) ∨  (x [ n / v ])
+(¬ x) [ n / v ] = ¬ (x [ n / v ] )
+(all x => y) [ n / v ] = all x => (y [ n / v ])
+(∃ x => y) [ n / v ] =  ∃ x =>    (y [ n / v ])
 
 {-# TERMINATING #-} 
 M0 : Statement → Bool
@@ -56,8 +56,8 @@
 M0 (x ∨ y) = M0 x Data.Bool.∨ M0 y
 M0 (¬ x) = not (M0 x)
 -- we only try simple constant, it may contains arbitrary complex functional value
-M0 (all x => y) = M0 ( subst-prop y x a ) Data.Bool.∧ M0 ( subst-prop y x b ) Data.Bool.∧ M0 ( subst-prop y x c ) 
-M0 (∃ x => y)   = M0 ( subst-prop y x a ) Data.Bool.∨ M0 ( subst-prop y x b ) Data.Bool.∨ M0 ( subst-prop y x c ) 
+M0 (all x => y) = M0 ( y [ x / a ] ) Data.Bool.∧ M0 ( y [ x / b ] ) Data.Bool.∧ M0 (  y [ x / c ] ) 
+M0 (∃ x => y)   = M0 ( y [ x / a ] ) Data.Bool.∨ M0 ( y [ x / b ] ) Data.Bool.∨ M0 (  y [ x / c ] ) 
 M0 _ = false
 
 test3 : Bool