implementation: the "Logic" class

Definition of the Logic class:

Formula------------ Constant ------------------------ Atom
                |                                          |
                --------- Variable                  ---------- Char, and String
                |                                          |
                --------- Apply-Operator       ---------- Number ------------ Integer, Real, Bool, etc...
                |                                                                        
                --------- Apply-Functor


Atom:  {  string: name,  int: index  }                                 // atoms are eg: "john", "mary"
Variable:  {  int: index  }
Apply-Operator:  {  char: op,  Formula[]: arguments  }          // op applied to 1 or more arguments
Apply-Functor:  {  Atom: functor, Formula[]: arguments  }    // functor applied to 1 or more arguments
                                                                                      // functor can be function or predicate
                                                                                      // functor's name is just an Atom

Definition of FOL terminology:

This set of terminology is standard for FOL:

1. At the top level is the formula (or proposition, or sentence, or logic statement, all synonyms).
2. A formula can be a rule or a fact.  A rule is of the form
        A <- X, Y, Z, ...
   And a fact does not contain the "<-" operator.
3. Each formula consists of a number of literals joined by logical operators (aka connectives) such as AND and OR, and operations can be nested.  Note that NOT is a unary operator.  Eg:
• (loves john mary)                                     is a literal
• (NOT (female john))                                is a literal
• (AND (loves john mary) (female mary))    are 2 literals joined by AND
• (OR (AND (p X) (q Y))  (r Z))                  is nested
4. Each literal consists of a predicate plus its arguments, eg:
• (loves john mary)                    where love = predicate with 2 arguments
• (male paul)                             where male = predicate with 1 argument
• (female (daughter-of paul))      where female = predicate with 1 argument, "daughter-of" is a function symbol
5. Terms (or arguments) can be:
• variables   (eg:  X, Y, Z)
• constants   (eg:  john, mary, 17, "String")
• functions of other terms   (eg:  daughter-of(john),  sine(3.14))

That's all!

Our simplified terminology:

In anticipation of higher-order logic:

1. The notion of predicates and functions are combined into functors.
2. We can also absorb functors into operators, but this is not currently done.
3. In FOL, a function-application is not a formula, but this is relaxed in our definition.  Potentially it can lead to ill-formed formulas.  For example, sine(3.14) is clearly not a formula;  but we want to allow some functions that return formulas.

The result is more elegant, and we can express this by a set of re-write rules:
     formula ===> constant
     formula ===> variable
     formula ===> (functor formula1 formula2 ...)
     formula ===> (op formula1 formula2 ...)

More about rules

Rules are of the form:

     A <- B, C, D, ...

where A is the "head", B,C,D,... is the "body", and "<-" is just a special operator like "AND";  we can call it "COND" for conditional.

Each "," is equivalent to an "AND".  So, the above rule is represented as:

     (COND A (AND B C D...))

where "AND" can accept more than 2 arguments.

( In our logic, <- translates to a link in a Bayesian network.  For this reason, it seems not very meaningful for a formula to have "<-" inside the body instead of at the head position. )

Some special cases:

1. If a rule has no head, it is still a rule, such as:
        (interesting X)    means "everything is interesting"
   -- note that all variables are implicitly universally quantified, ie, the above is really:
        for-all X,  interesting X
2. We can ignore the case where a rule has no body (it's not useful).
3. A rule without variables is still a rule, eg:
        wet <- rains
        not cloudy <- sunny

Representing variables and constants

Notice that we can use any way we want to represent variables and constants internally.  In my Lisp code, variables are like "?1" etc and constants are "john" etc.  In a more sophisticated KB, we would of course use some kind of indexes.

Code

This is Russell's C# code, and Chuck's Cobra code.  When in doubt, please conform to the definition above.