Mercurial > hg > Members > kono > Proof > FirstOrder
changeset 13:b8b3eaf0dd61
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 15 Aug 2020 11:28:18 +0900 |
| parents | 4b131e351170 |
| children | 1e3ebb348a54 |
| files | clausal.agda |
| diffstat | 1 files changed, 5 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/clausal.agda Sat Aug 15 11:03:32 2020 +0900 +++ b/clausal.agda Sat Aug 15 11:28:18 2020 +0900 @@ -47,8 +47,10 @@ {-# 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 - skolemv1 : (Statement → List Const → List Func → List Var → Statement ) → Statement → List Const → List Func → List Var → Statement + 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 existentical 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 ) cl [] (v ∷ t) = skolemv1 next s cl [] (v ∷ t) @@ -58,12 +60,13 @@ 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 cl fl vl = next s cl fl vl + skolemv1 next = next -- remove universal quantifiers univout : Statement → Statement univout (s /\ s₁) = univout s /\ univout s₁ univout (s \/ s₁) = univout s \/ univout s₁ +univout (All x => s ) = s univout x = x -- move disjunctions inside