GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-23 19:42:50 -06:00
Code Issues Packages Projects Releases Wiki Activity

gfcm header

Browse Source
This commit is contained in:
aarne
2004-09-14 17:05:46 +00:00
parent 35f884ddfd
commit fe045070cf
26 changed files with 1348 additions and 883 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
grammars/logic/Arithm.gf
View File

@@ -3,9 +3,10 @@ abstract Arithm = Logic ** {
-- arithmetic
fun
Nat, Real : Dom ;
data
zero : Elem Nat ;
succ : Elem Nat -> Elem Nat ;
fun
trunc : Elem Real -> Elem Nat ;
EqNat : (m,n : Elem Nat) -> Prop ;
@@ -19,13 +20,13 @@ fun
two : Elem Nat ;
sum : (m,n : Elem Nat) -> Elem Nat ;
prod : (m,n : Elem Nat) -> Elem Nat ;
data
evax1 : Proof (Even zero) ;
evax2 : (n : Elem Nat) -> Proof (Even n) -> Proof (Odd (succ n)) ;
evax3 : (n : Elem Nat) -> Proof (Odd n) -> Proof (Even (succ n)) ;
eqax1 : Proof (EqNat zero zero) ;
eqax2 : (m,n : Elem Nat) -> Proof (EqNat m n) -> Proof (EqNat (succ m) (succ n)) ;
fun
IndNat : (C : Elem Nat -> Prop) ->
Proof (C zero) ->
((x : Elem Nat) -> Proof (C x) -> Proof (C (succ x))) ->
@@ -45,7 +46,6 @@ def
(Univ Nat (\x -> Impl (Conj (LtNat one x) (Div n x)) (EqNat x n))) ;
Abs = Abs ;
--- data Elem = zero | succ ;
fun ex1 : Text ;
def ex1 =

16
grammars/logic/Logic.gf
View File

@@ -32,25 +32,36 @@ fun
ImplP : (A : Prop) -> (Proof A -> Prop) -> Prop ;
-- inference rules
data
ConjI : (A,B : Prop) -> Proof A -> Proof B -> Proof (Conj A B) ;
fun
ConjEl : (A,B : Prop) -> Proof (Conj A B) -> Proof A ;
ConjEr : (A,B : Prop) -> Proof (Conj A B) -> Proof B ;
data
DisjIl : (A,B : Prop) -> Proof A -> Proof (Disj A B) ;
DisjIr : (A,B : Prop) -> Proof B -> Proof (Disj A B) ;
fun
DisjE : (A,B,C : Prop) -> Proof (Disj A B) ->
(Proof A -> Proof C) -> (Proof B -> Proof C) -> Proof C ;
data
ImplI : (A,B : Prop) -> (Proof A -> Proof B) -> Proof (Impl A B) ;
fun
ImplE : (A,B : Prop) -> Proof (Impl A B) -> Proof A -> Proof B ;
data
NegI : (A : Prop) -> (Proof A -> Proof Abs) -> Proof (Neg A) ;
fun
NegE : (A : Prop) -> Proof (Neg A) -> Proof A -> Proof Abs ;
AbsE : (C : Prop) -> Proof Abs -> Proof C ;
data
UnivI : (A : Dom) -> (B : Elem A -> Prop) ->
((x : Elem A) -> Proof (B x)) -> Proof (Univ A B) ;
fun
UnivE : (A : Dom) -> (B : Elem A -> Prop) ->
Proof (Univ A B) -> (a : Elem A) -> Proof (B a) ;
data
ExistI : (A : Dom) -> (B : Elem A -> Prop) ->
(a : Elem A) -> Proof (B a) -> Proof (Exist A B) ;
fun
ExistE : (A : Dom) -> (B : Elem A -> Prop) -> (C : Prop) ->
Proof (Exist A B) -> ((x : Elem A) -> Proof (B x) -> Proof C) ->
Proof C ;
@@ -61,9 +72,6 @@ fun
-- pronoun
Pron : (A : Dom) -> Elem A -> Elem A ;
data
Proof = ConjI | DisjIl | DisjIr ;
def
-- proof normalization
ConjEl _ _ (ConjI _ _ a _) = a ;