Mysaa/m1-internship
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Fixed module names as file names had changed.

Browse Source
This commit is contained in:
Mysaa 2023-06-02 17:45:13 +02:00
parent c8cc4b9f54
commit d3cf3cd0e6
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
4 changed files with 30 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
InfinitaryFirstOrderKripke.agda
View File

@ -2,11 +2,11 @@
open import Agda.Builtin.Nat
module PropositionalKripke (Term : Set) (R : Nat → Set) where
module InfinitaryFirstOrderKripke (Term : Set) (R : Nat → Set) where
open import ListUtil
open import PropUtil
open import FirstOrderLogic Term R
open import InfinitaryFirstOrderLogic Term R
private
variable

8
InfinitaryFirstOrderKripkeGeneral.agda
View File

@ -2,13 +2,13 @@
open import Agda.Builtin.Nat hiding (zero)
module PropositionalKripkeGeneral (Term : Set) (R : Nat → Set) where
module InfinitaryFirstOrderKripkeGeneral (Term : Set) (R : Nat → Set) where
open import ListUtil
open import PropUtil
open import FirstOrderLogic Term R using (Form; Args; Rel; _⇒_; _∧∧_; ⊤⊤; ∀∀; Con)
open import InfinitaryFirstOrderLogic Term R using (Form; Args; Rel; _⇒_; _∧∧_; ⊤⊤; ∀∀; Con)
open import PropositionalKripke Term R using (Kripke)
open import InfinitaryFirstOrderKripke Term R using (Kripke)
record Preorder (T : Set₀) : Set₁ where
constructor order
@ -78,7 +78,7 @@ module PropositionalKripkeGeneral (Term : Set) (R : Nat → Set) where
module NormalizationTests where
{- Now using our records -}
open import FirstOrderLogic Term R hiding (Form; _⇒_; Con)
open import InfinitaryFirstOrderLogic Term R hiding (Form; _⇒_; Con)
ClassicNN : NormalAndNeutral

2
InfinitaryFirstOrderLogic.agda
View File

@ -2,7 +2,7 @@
open import Agda.Builtin.Nat
module FirstOrderLogic (Term : Set) (R : Nat → Set) where
module InfinitaryFirstOrderLogic (Term : Set) (R : Nat → Set) where
open import PropUtil
open import ListUtil

24
Readme.agda
View File

@ -1,4 +1,5 @@
{-# OPTIONS --prop #-}
module Readme where
-- We will use String as propositional variables
@ -115,7 +116,7 @@ module PierceDisproof where
PierceNotProvable h = Pierce⊥w₁ (⟦ h ⟧ {w₁} tt)
module CompletenessAndNormalization where
module GeneralizationInPropositionalLogic where
-- With Kripke models, we can even prove completeness
-- Using the Universal Kripke Model
@ -145,5 +146,26 @@ module CompletenessAndNormalization where
u6 = NormalizationFrame.u NormalizationTests.Frame⊆
q6 = NormalizationFrame.q NormalizationTests.Frame⊆
module GeneralizationInInfinitaryFirstOrderLogic where
-- We also did implement infinitary first order logic
-- (i.e. ∀ is like an infinitary ∧)
-- The proofs works the same with only little modifications
open import InfinitaryFirstOrderKripkeGeneral String (λ n → String)
u1 = NormalizationFrame.u NormalizationTests.Frame⊢
q1 = NormalizationFrame.q NormalizationTests.Frame⊢
u2 = NormalizationFrame.u NormalizationTests.Frame⊢⁰
q2 = NormalizationFrame.q NormalizationTests.Frame⊢⁰
u3 = NormalizationFrame.u NormalizationTests.Frame∈*
q3 = NormalizationFrame.q NormalizationTests.Frame∈*
u4 = NormalizationFrame.u NormalizationTests.Frame⊂⁺
q4 = NormalizationFrame.q NormalizationTests.Frame⊂⁺
u5 = NormalizationFrame.u NormalizationTests.Frame⊂
q5 = NormalizationFrame.q NormalizationTests.Frame⊂
u6 = NormalizationFrame.u NormalizationTests.Frame⊆
q6 = NormalizationFrame.q NormalizationTests.Frame⊆