Mercurial > hg > Members > kono > Proof > FirstOrder

changeset 14:1e3ebb348a54

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 Sat, 15 Aug 2020 11:51:03 +0900
parents b8b3eaf0dd61
children 2f4db56bb289
files Logic.agda clausal.agda example2.agda
diffstat 3 files changed, 16 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/Logic.agda	Sat Aug 15 11:28:18 2020 +0900
+++ b/Logic.agda	Sat Aug 15 11:51:03 2020 +0900
@@ -17,6 +17,7 @@
    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 )
@@ -26,10 +27,15 @@
 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 )
 
+--
+-- The interpretation
+--   all-const is a list of all possible arguments of predicates (possibly infinite)
+--   sbst is an Expr depenent variable substituion
+--
 {-# TERMINATING #-} 
 M : (amap :  Pred  → Bool ) (pmap :  Pred → Expr → Bool )
    →  (all-const   : List Expr )
-   →  (subst-prop : Expr  → Var →  Expr  → Expr  )
+   →  (sbst : Expr  → Var →  Expr  → Expr  )
    → Statement  → Bool
 M amap pmap all0 sbst s = m s where
    m :  Statement  → Bool
--- a/clausal.agda	Sat Aug 15 11:28:18 2020 +0900
+++ b/clausal.agda	Sat Aug 15 11:51:03 2020 +0900
@@ -62,7 +62,7 @@
    skolemv1 next (s \/ s₁)                             = skolemv1 ( λ s → skolemv1 (λ s₁ → next (s \/ s₁) ) s₁ ) s 
    skolemv1 next                                       = next 
 
--- remove universal quantifiers
+-- 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₁
--- a/example2.agda	Sat Aug 15 11:28:18 2020 +0900
+++ b/example2.agda	Sat Aug 15 11:51:03 2020 +0900
@@ -70,3 +70,11 @@
 
 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 ) ))
+
+open import clausal Const Func Var Pred 
+
+open Expr
+open Clause
+
+test007 : List Clause
+test007 = translate ex1 [] [] subst-expr