|
10
|
1 module example2 where
|
|
|
2 open import Data.List hiding (all ; and ; or )
|
|
|
3 open import Data.Maybe
|
|
15
|
4 open import Data.Bool hiding ( not ; _∧_ ; _∨_ )
|
|
10
|
5
|
|
|
6 data Const : Set where
|
|
|
7 anakin : Const
|
|
|
8 luke : Const
|
|
|
9 leia : Const
|
|
|
10
|
|
|
11 data Var : Set where
|
|
|
12 X : Var
|
|
|
13 Y : Var
|
|
|
14 Z : Var
|
|
|
15
|
|
|
16 data Func : Set where
|
|
|
17
|
|
|
18 data Pred : Set where
|
|
|
19 father : Pred
|
|
|
20 brother : Pred
|
|
|
21
|
|
|
22 open import Logic Const Func Var Pred
|
|
|
23
|
|
|
24 _⇒_ : Statement → Statement → Statement
|
|
15
|
25 x ⇒ y = ( ¬ x ) ∨ y
|
|
10
|
26
|
|
|
27 ex1 : Statement
|
|
15
|
28 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) )
|
|
10
|
29
|
|
|
30 subst-expr : Expr → Var → Expr → Expr
|
|
|
31 subst-expr (var X) X v = v
|
|
|
32 subst-expr (var Y) Y v = v
|
|
|
33 subst-expr (var Z) Z v = v
|
|
|
34 subst-expr (func f₁ e) xv v = func f₁ ( subst-expr e xv v )
|
|
|
35 subst-expr (e , e1) xv v = ( subst-expr e xv v ) , ( subst-expr e1 xv v )
|
|
|
36 subst-expr x _ v = x
|
|
|
37
|
|
|
38 amap : (px : Pred ) → Bool
|
|
|
39 amap px = false
|
|
|
40 pmap : (px : Pred ) → Expr → Bool
|
|
|
41 pmap father ( const leia , const anakin ) = true
|
|
|
42 pmap father ( const luke , const anakin ) = true
|
|
|
43 pmap brother ( const leia , const luke) = true
|
|
15
|
44 pmap brother ( const luke , const leia) = true
|
|
|
45 pmap brother ( const luke , const luke) = true -- strange but our definition of brother requires this
|
|
|
46 pmap brother ( const leia , const leia) = true
|
|
10
|
47 pmap px _ = false
|
|
|
48
|
|
|
49 -- we only try simple constant, it may contains arbitrary complex functional value
|
|
|
50 all0 : List Expr
|
|
|
51 all0 = const anakin ∷ const luke ∷ const leia ∷ []
|
|
|
52
|
|
15
|
53 --
|
|
|
54 -- pmap is a model of axiom ex1
|
|
|
55 --
|
|
|
56 test9 : Bool
|
|
|
57 test9 = M amap pmap all0 subst-expr ex1
|
|
|
58
|
|
|
59 test3 : Bool
|
|
|
60 test3 = M amap pmap all0 subst-expr (
|
|
|
61 ( predx father ( const leia , const anakin ) ∧ predx father ( const luke , const anakin ) ) ⇒ predx brother ( const leia , const luke) )
|
|
10
|
62
|
|
|
63 --
|
|
15
|
64 -- Valid Proposition is true on any interpretation
|
|
10
|
65 --
|
|
|
66 pmap1 : (px : Pred ) → Expr → Bool
|
|
|
67 pmap1 father ( const leia , const anakin ) = true
|
|
|
68 pmap1 father ( const luke , const anakin ) = true
|
|
|
69 pmap1 brother ( const leia , const luke) = false
|
|
|
70 pmap1 px _ = false
|
|
|
71
|
|
15
|
72 test6 : Bool
|
|
|
73 test6 = M amap pmap1 all0 subst-expr (
|
|
|
74 ( ex1 ∧ ( predx father ( const leia , const anakin ) ∧ predx father ( const luke , const anakin ) )) ⇒ predx brother ( const leia , const luke) )
|
|
10
|
75
|
|
15
|
76 --
|
|
|
77 -- pmap1 is not a model of axiom ex1
|
|
|
78 --
|
|
10
|
79
|
|
15
|
80 test4 : Bool
|
|
|
81 test4 = M amap pmap1 all0 subst-expr ex1
|
|
|
82
|
|
|
83 test5 : Bool
|
|
|
84 test5 = M amap pmap1 all0 subst-expr ( All X => All Y => ( predx father ( var X , const anakin ) ∧ predx father (var Y , const anakin ) ))
|
|
14
|
85
|
|
|
86 open import clausal Const Func Var Pred
|
|
|
87
|
|
15
|
88 test7 : List Clause
|
|
|
89 test7 = translate ex1 [] [] subst-expr
|
|
18
|
90
|
|
|
91 -- brother (X , Y) :- father (X , Z) , father (Y , Z)
|
|
|
92
|
