Mercurial > hg > Members > kono > Proof > FirstOrder

changeset 8:0737e6671061

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 13 Aug 2020 12:50:30 +0900
parents abb61bee093a
children 627a6bf54ed5
files first-order.agda
diffstat 1 files changed, 13 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/first-order.agda	Thu Aug 13 12:46:37 2020 +0900
+++ b/first-order.agda	Thu Aug 13 12:50:30 2020 +0900
@@ -5,28 +5,28 @@
 open import Relation.Nullary hiding (¬_)
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 
-module Logic (Atom : Set ) (Const Func Var Pred : Atom → Set)  where
+module Logic (Term : Set ) (Const Func Var Pred : Term → Set)  where
 
   data Expr  : Set  where
-     var   : {v : Atom } → Var v → Expr 
-     func  : {x : Atom }  → (f : Func x) → Expr → Expr 
-     const : {c : Atom } → Const c → Expr 
+     var   : {v : Term } → Var v → Expr 
+     func  : {x : Term }  → (f : Func x) → Expr → Expr 
+     const : {c : Term } → Const c → Expr 
      args : Expr → Expr  → Expr 
 
   data Statement : Set where
-     atom       : {x : Atom } → Pred x → Statement 
-     predicate  : {p : Atom }  → Pred p → Expr → Statement 
+     atom       : {x : Term } → Pred x → Statement 
+     predicate  : {p : Term }  → Pred p → Expr → Statement 
      and        : Statement → Statement  → Statement 
      or         : Statement → Statement  → Statement 
      not        : Statement  → Statement 
-     All        : {x : Atom } → Var x → Statement → Statement 
-     Exist      : {x : Atom } → Var x → Statement → Statement 
+     All        : {x : Term } → Var x → Statement → Statement 
+     Exist      : {x : Term } → Var x → Statement → Statement 
 
   {-# TERMINATING #-} 
-  Model : (ampa :  {x : Atom } → (px :  Pred x ) → Bool )
-       →  (pmap : {p : Atom }  → (px :  Pred p ) → Expr → Bool )
+  Model : (ampa :  {x : Term } → (px :  Pred x ) → Bool )
+       →  (pmap : {p : Term }  → (px :  Pred p ) → Expr → Bool )
        →  (all-const   : List Expr )
-       → ( subst-prop :  {x : Atom } (e : Statement  ) → Var x → (value : Expr ) → Statement  )
+       → ( subst-prop :  {x : Term } (e : Statement  ) → Var x → (value : Expr ) → Statement  )
        → Statement  → Bool
   Model amap pmap all0 sbst s = model s where
       model :  Statement  → Bool
@@ -36,11 +36,11 @@
       model (or s s₁) = model s ∨ model s₁ 
       model (not s) = Data.Bool.not (model s )
       model (All x s) = model-all all0 x s  where
-          model-all :  List Expr → {x : Atom } → Var x → Statement → Bool
+          model-all :  List Expr → {x : Term } → Var x → Statement → Bool
           model-all [] vx s = true
           model-all (x ∷ t) vx s = model (sbst s vx x ) ∧ model-all t vx s
       model (Exist x s) = model-exist all0 x s  where
-          model-exist :  List Expr → {x : Atom } → Var x → Statement → Bool
+          model-exist :  List Expr → {x : Term } → Var x → Statement → Bool
           model-exist [] vx s = false
           model-exist (x ∷ t) vx s = model (sbst s vx x ) ∨ model-exist t vx s
 
@@ -71,7 +71,6 @@
       const : Kind
       var  : Kind
       func : Kind
-      conn : Kind
       arg  : Kind
       args : Kind