Mercurial > hg > Members > kono > Proof > FirstOrder

changeset 15:2f4db56bb289 current

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix example
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 15 Aug 2020 16:59:52 +0900
parents 1e3ebb348a54
children fbecfa63dc2c
files Logic.agda clausal.agda example1.agda example2.agda simple-logic.agda
diffstat 5 files changed, 75 insertions(+), 60 deletions(-) [+]
line wrap: on
line diff
--- a/Logic.agda	Sat Aug 15 11:51:03 2020 +0900
+++ b/Logic.agda	Sat Aug 15 16:59:52 2020 +0900
@@ -1,6 +1,6 @@
 module Logic (Const Func Var Pred : Set)  where
 open import Data.List hiding (all ; and ; or )
-open import Data.Bool hiding ( not )
+open import Data.Bool hiding ( not ; _∧_ ; _∨_ )
 
 data Expr  : Set  where
    var   : Var → Expr 
@@ -11,8 +11,8 @@
 data Statement : Set where
    pred       : Pred  → Statement 
    predx  : Pred  → Expr → Statement 
-   _/\_   : Statement → Statement  → Statement 
-   _\/_         : Statement → Statement  → Statement 
+   _∧_   : Statement → Statement  → Statement 
+   _∨_         : Statement → Statement  → Statement 
    ¬_         : Statement  → Statement 
    All_=>_        : Var → Statement → Statement 
    Exist_=>_      : Var → Statement → Statement 
@@ -21,8 +21,8 @@
 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 ∧ 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 )
@@ -41,15 +41,15 @@
    m :  Statement  → Bool
    m (pred x) = amap x
    m (predx x x₁) = pmap x x₁
-   m (s /\ s₁) = m s  ∧ m s₁ 
-   m (s \/ s₁) = m s ∨ 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 )
    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 ) ∧ m-all t vx s
+     m-all (x ∷ t) vx s = m (subst-prop s sbst 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 [] vx s = false
-     m-exist (x ∷ t) vx s = m (subst-prop s sbst vx x ) ∨ m-exist t vx s
+     m-exist (x ∷ t) vx s = m (subst-prop s sbst vx x ) Data.Bool.∨ m-exist t vx s
 
--- a/clausal.agda	Sat Aug 15 11:51:03 2020 +0900
+++ b/clausal.agda	Sat Aug 15 16:59:52 2020 +0900
@@ -1,6 +1,6 @@
 module clausal (Const Func Var Pred : Set)  where
 open import Data.List hiding (all ; and ; or )
-open import Data.Bool hiding ( not )
+open import Data.Bool hiding ( not ; _∧_ ; _∨_ )
 open import Function
 
 open import Logic Const Func Var Pred 
@@ -14,8 +14,8 @@
 -- data Statement : Set where
 --    pred       : Pred  → Statement 
 --    predx  : Pred  → Expr → Statement 
---    _/\_   : Statement → Statement  → Statement 
---    _\/_         : Statement → Statement  → Statement 
+--    _∧_   : Statement → Statement  → Statement 
+--    _∨_         : Statement → Statement  → Statement 
 --    ¬_         : Statement  → Statement 
 --    All_=>_        : Var → Statement → Statement 
 --    Exist_=>_      : Var → Statement → Statement 
@@ -26,16 +26,16 @@
 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 ∧ 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 ∧ 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)
@@ -58,14 +58,14 @@
       mkarg : (v : Var) (vl : List Var ) → Expr
       mkarg v []  = var v
       mkarg v (v1 ∷ t )  = var v , mkarg v1 t
-   skolemv1 next (s /\ s₁)                             = skolemv1 ( λ s → skolemv1 (λ s₁ → next (s /\ s₁) ) s₁ ) s 
-   skolemv1 next (s \/ s₁)                             = skolemv1 ( λ s → skolemv1 (λ s₁ → next (s \/ s₁) ) s₁ ) s 
+   skolemv1 next (s ∧ s₁)                             = skolemv1 ( λ s → skolemv1 (λ s₁ → next (s ∧ s₁) ) s₁ ) s 
+   skolemv1 next (s ∨ s₁)                             = skolemv1 ( λ s → skolemv1 (λ s₁ → next (s ∨ s₁) ) s₁ ) s 
    skolemv1 next                                       = next 
 
 -- remove universal quantifiers (assuming all variables are different)
 univout  : Statement → Statement
-univout (s /\ s₁) = univout s /\ univout s₁
-univout (s \/ s₁) = univout s \/ univout s₁
+univout (s ∧ s₁) = univout s ∧ univout s₁
+univout (s ∨ s₁) = univout s ∨ univout s₁
 univout (All x => s ) = s
 univout x = x
 
@@ -75,12 +75,12 @@
 
 {-# TERMINATING #-} 
 conjn  : Statement → Statement
-conjn (s /\ s₁) = conjn s /\ conjn s₁
-conjn (s \/ s₁) = conjn1 ( ( conjn s ) \/ ( conjn s₁) )
+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 ∧ 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
@@ -91,11 +91,11 @@
 clausify : Statement → List Clause
 clausify s = clausify1 s [] where
    inclause : Statement → Clause → Clause
-   inclause (x \/ y ) a  = inclause x ( inclause y a ) 
+   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 ∧ 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
--- a/example1.agda	Sat Aug 15 11:51:03 2020 +0900
+++ b/example1.agda	Sat Aug 15 16:59:52 2020 +0900
@@ -1,7 +1,7 @@
 module example1 where
 open import Data.List hiding (all ; and ; or )
 open import Data.Maybe 
-open import Data.Bool hiding ( not )
+open import Data.Bool hiding ( not ; _∧_ ; _∨_ )
 
 data Const : Set where
       a : Const
@@ -26,7 +26,7 @@
 open import Logic Const Func Var Pred 
 
 ex1 : Statement
-ex1 = ¬ ( pred q  /\ ( All X =>  predx p ( func f (var X) ) ))
+ex1 = ¬ ( pred q  ∧ ( All X =>  predx p ( func f (var X) ) ))
 
 subst-expr :  Expr  → Var → Expr → Expr 
 subst-expr  (var X) X v = v
@@ -51,3 +51,8 @@
 test003 : Bool 
 test003 = 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
+
--- a/example2.agda	Sat Aug 15 11:51:03 2020 +0900
+++ b/example2.agda	Sat Aug 15 16:59:52 2020 +0900
@@ -1,7 +1,7 @@
 module example2 where
 open import Data.List hiding (all ; and ; or )
 open import Data.Maybe 
-open import Data.Bool hiding ( not )
+open import Data.Bool hiding ( not ; _∧_ ; _∨_ )
 
 data Const : Set where
       anakin : Const
@@ -23,10 +23,10 @@
 open import Logic Const Func Var Pred 
 
 _⇒_ : Statement → Statement → Statement 
-x ⇒ y = ( ¬ x ) \/ y
+x ⇒ y = ( ¬ x ) ∨ y
 
 ex1 : Statement
-ex1 = All X => All Y => (( Exist Z => ( ( predx father ( var X , var Z ) /\  predx father (var Y , var Z ) ))) ⇒ predx brother ( var X , var Y) )
+ex1 = All X => All Y => (( Exist Z => ( ( predx father ( var X , var Z ) ∧  predx father (var Y , var Z ) ))) ⇒ predx brother ( var X , var Y) )
 
 subst-expr :  Expr  → Var → Expr → Expr 
 subst-expr  (var X) X v = v
@@ -42,18 +42,27 @@
 pmap father ( const leia , const anakin ) = true
 pmap father ( const luke , const anakin ) = true
 pmap brother ( const leia , const luke) = true
+pmap brother ( const luke , const leia) = true
+pmap brother ( const luke , const luke) = true  -- strange but our definition of brother requires this
+pmap brother ( const leia , const leia) = true
 pmap px _ = false
 
 -- we only try simple constant, it may contains arbitrary complex functional value
 all0   :  List Expr
 all0 =  const anakin ∷ const luke ∷ const leia ∷ []
 
-test003 : Bool 
-test003 = M amap pmap all0 subst-expr (
-     ( ex1 /\ ( predx father ( const leia , const anakin ) /\ predx father ( const luke , const anakin ) )) ⇒ predx brother ( const leia , const luke) )
+--
+-- pmap is a model of axiom ex1
+--
+test9 : Bool 
+test9 = M amap pmap all0 subst-expr ex1 
+
+test3 : Bool 
+test3 = M amap pmap all0 subst-expr (
+     (  predx father ( const leia , const anakin ) ∧ predx father ( const luke , const anakin ) ) ⇒ predx brother ( const leia , const luke) )
 
 --
--- Valid Proposition true on any interpretation
+-- Valid Proposition is true on any interpretation
 --
 pmap1 : (px :  Pred ) → Expr → Bool 
 pmap1 father ( const leia , const anakin ) = true
@@ -61,20 +70,21 @@
 pmap1 brother ( const leia , const luke) = false
 pmap1 px _ = false
 
-test006 : Bool 
-test006 = M amap pmap1 all0 subst-expr (
-     ( ex1 /\ ( predx father ( const leia , const anakin ) /\ predx father ( const luke , const anakin ) )) ⇒ predx brother ( const leia , const luke) )
+test6 : Bool 
+test6 = M amap pmap1 all0 subst-expr (
+     ( ex1 ∧ ( predx father ( const leia , const anakin ) ∧ predx father ( const luke , const anakin ) )) ⇒ predx brother ( const leia , const luke) )
 
-test004 : Bool 
-test004 = M amap pmap all0 subst-expr ( ex1  )
+--
+-- pmap1 is not a model of axiom ex1
+--
 
-test005 : Bool 
-test005 = M amap pmap all0 subst-expr (   All X => All Y => ( predx father ( var X , const anakin ) /\  predx father (var Y , const anakin ) ))
+test4 : Bool 
+test4 = M amap pmap1 all0 subst-expr ex1 
+
+test5 : Bool 
+test5 = M amap pmap1 all0 subst-expr (   All X => All Y => ( predx father ( var X , const anakin ) ∧  predx father (var Y , const anakin ) ))
 
 open import clausal Const Func Var Pred 
 
-open Expr
-open Clause
-
-test007 : List Clause
-test007 = translate ex1 [] [] subst-expr  
+test7 : List Clause
+test7 = translate ex1 [] [] subst-expr  
--- a/simple-logic.agda	Sat Aug 15 11:51:03 2020 +0900
+++ b/simple-logic.agda	Sat Aug 15 16:59:52 2020 +0900
@@ -1,5 +1,5 @@
 module simple-logic where
-open import Data.Bool
+open import Data.Bool hiding  ( _∨_ ; _∧_ )
 
 data Var : Set where
    X : Var
@@ -20,14 +20,14 @@
    p : Expr → Statement
    q : Statement
    r : Statement
-   _/\_    :  Statement → Statement → Statement
-   _\/_    :  Statement → Statement → Statement
+   _∧_    :  Statement → Statement → Statement
+   _∨_    :  Statement → Statement → Statement
    ¬       :  Statement → Statement 
    all_=>_ :  Var → Statement → Statement
    ∃_=>_   :  Var → Statement → Statement
 
-test002 : Statement
-test002 = ¬ ( q /\ ( all X => p ( f ( var X  ))))
+test2 : Statement
+test2 = ¬ ( q ∧ ( all X => p ( f ( var X  ))))
 
 subst-expr : Expr → Var → (value : Expr ) → Expr
 subst-expr (var X ) X v = v 
@@ -41,8 +41,8 @@
 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 ∧ 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 
@@ -52,14 +52,14 @@
 M0 q = true
 M0 r = false
 M0 (p  a ) = true
-M0 (x /\ y) = M0 x ∧ M0 y
-M0 (x \/ y) = M0 x ∨ M0 y
+M0 (x ∧ y) = M0 x Data.Bool.∧ M0 y
+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 ) ∧ M0 ( subst-prop y x b ) ∧ M0 ( subst-prop y x c ) 
-M0 (∃ x => y)   = M0 ( subst-prop y x a ) ∨ M0 ( subst-prop y x b ) ∨ M0 ( subst-prop y x c ) 
+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 _ = false
 
-test003 : Bool 
-test003 = M0 ( ∃ X => p ( var X ))
+test3 : Bool 
+test3 = M0 ( ∃ X => p ( var X ))