Logic notations — EG, PC, CLIF, CGIF (typed and untyped)

Based on https://www.taoke.de/ke/Logic/LGC-Notation/index.html.

The tutorial of John Sowa ([Sowa2018a]) also discusses mappings to other logic syntaxes and graphical representations. The abbreviations stand for:

• EG = Existential Graph,
• PC = Predicate Calculus,
• CLIF = Common Logic Interchange Format,
• CGIF = Common Graph Interchange Format.

A t is added for typed, a u is added for untyped, e.g. PCu = untyped predicate calculus format. Instead of Sowa’s “the cat is on the mat” example, the premise Farmer owns donkey is used in TAoKE (see section Farmer beats Donkey). All the following examples are semantically equivalent. The expressions are TRUE if there exists a farmer who owns a donkey.

• Peirce (EG): Farmer — Owns — Donkey
• Peirce: Σ_x Σ_y Farmer_x ? Donkey_y ? owns_x,y
• Peano (PCu): ∃x ∃y Farmer(x) ∧ Donkey(y) ∧ owns(x,y)
• Peano (PCt): (∃x:Farmer) (∃y Donkey) owns(x,y)
• CGIFu: [*x] [*y] (Farmer ?x) (owns ?x ?y) (Donkey ?y)
• CGIFt: [Farmer *x] [Donkey *y] (owns ?x ?y)
• CLIFu: (exists (x y) (and (Farmer x) (Donkey y) (owns x y)))
• CLIFt: (exists ((x Farmer ) (Donkey y)) (owns x y))

The EGIF phrase structure rules define a proper subset of CGIF. Sowa in [Sowa2018a] defines a set of EGIF rules using Extended Backus–Naur Form (EBNF).

The sentence Tom believes that Mary wants to marry a sailor (see section Tom’s Belief) can be written as:

• CLIF for IKL: (believes Tom (that (wants-to-marry Mary sailor)))
• CGIF for IKL: (believes Tom [Proposition (wants-to-marry Mary sailor)])

[BaMc2003] provides DL background when relating these notations to description logics.