The language supports full first-order logic expressions (“well-formed
formulas”), including universal and existential quantifiers. The keyboard
characters used for representing logical symbols are the following:

~ : “not”

&: “and”

v : “or”

-> : “implies”

<--> : “if and only if”

@ : “for all” (universal quantifier)

# : “there exists” (existential quantifier)

The language
supports *types* for logical objects, such as variables, constants, and
functions (or “functors” as they are often called in logic). Thus, for
instance, when a variable *x* is declared, it can be optionally
given a type, as follows:

Types

person;

Variables

x : person;

Types allow for the simplification of the
expressed logical theory, without losing in derivational power. Without
types, the previous type “person” would have to be expressed though a
predicate, such as person(x). With types, such predicates of a single
parameter become redundant, thus simplifying logical formulas.

The language
supports a *hierarchy of types,* in which one type can be a
subtype of another type. For example:

Types

person < mammal < living_being;

chimp < mammal;

plant < living_being;

Thus, an entire hierarchy tree can be
specified. All types are assumed to be subtypes of the special and known
type *Entity,* which needs no declaration. When objects of given
types are unified, the object of a subtype can substitute a variable of any
of its supertypes, but not vice-versa. For example, IsRunning(**x**)
can be unified with IsRunning(John) if IsRunning has been declared as a
predicate expecting parameters of type mammal (see the previous hierarchy of
types), and John is a constant of type person. In the unification, John will
substitute **x**, because person < mammal. However, an object of
type plant cannot substitute the variable **x** of IsRunning,
because plant is not a subtype of mammal.

The special predicate *is* (*x,
type*) is provided for use with types, where *x* is any well-formed
expression, and *type* is one of the declared types. This predicate
evaluates to true if and only if the type of *x* is either *type,*
or it is a subtype of *type*.

Types are of course optional. They are
included only for the user’s convenience.

The overall
syntax of the language allows an initial declaration of Types, Constants,
Variables, Functions, and Predicates (in that order, but each is optional),
followed by any sections of Axioms, Definitions, and Theorems (in *any*
order). More Axioms may then follow the Theorems, followed by further sets
of Axioms, Definitions, and Theorems, in any order, without limitation. The
applet includes buttons on its tool-bar at the top that allow the user to
step through the theory either:

one theorem at
a time (button
), or

an entire set
of theorems at a time (button
), or

proving all
theorems up to the end (button
).

The user can interrupt the proving process
at any time (button ),
modify the theory by editing it, or start over (button
).

The syntax
allows the user to choose extreme simplification, ending up with expressions
of Propositional Calculus form (such as P -> Q, etc), or full adherence to
the declared types, in which case type-checking is strict and enforced. It
is up to the user to choose either strict or free syntactic conventions.