The LISt Processing (LISP) programming language, which is based on the lambda calculus, is the second oldest (1958) programming language — only the FORTRAN language is older. LISP became the favored programming language for artificial intelligence research. All program code is written as parenthesized lists. The Knowledge Interchange Format (KIF), which has a LISP-like format, was created to serve as a syntax for first-order logic. The IFF language (or logical notation) (Table 1), which is a vastly simplified and modified version of KIF, also has a LISP-like format. The IFF language contains both logical code and comments. Both nested namespaces and metalevels are specified by prefixes. The IFF grammar which specifies the syntax of the IFF language, is written in Extended Backus Naur Form (EBNF).

    Math   IFF
 names        
    a   o.i.a, inner context i,  outer context o 
atoms and terms        
 set element   x ∈ X or X(x)   (X x)
 predicate member   x ∈ p or p(x)   (p x)
 relation member   (xy) ∈ r or r(xy)   (r x y)
 function application   f(x)   (f x)
 equations        
    σ = τ or =(σ τ)   (= σ τ)
 connectives        
conjunction   φ ⋀ ψ or ⋀(φ ψ)   (and P Q)
disjunction   φ ⋁ ψ or ⋁(φ ψ)   (or P Q)
implication   φ ⇒ ψ or ⇒(φ ψ)   (implies P Q) or (=> P Q)
equivalence   φ ⇔ ψ or ⇔(φ ψ)   (iff P Q) or (<=> P Q)
negation   ¬ φ or ¬(φ)   (not P)
 quantifiers        
universal   x0 ∈ X0x1 ∈ X1 φ    
    or ∀(x0 ∈ X0x1 ∈ X1) (φ)   (forall ((X0 x0) (X1 x1)) P)
existential   x0 ∈ X0x1 ∈ X1 φ    
    or ∃(x0 ∈ X0x1 ∈ X1) (φ)   (exists ((X0 x0) (X1 x1)) P)
Table 1: Syntax Tutorial

 

Some IFF documents such as this one contain a lot of unicode characters, and so require a recent browser. But even some recent browsers fail to render it properly. Two browsers that do render these documents correctly are Firefox and Opera.