How do we prove a proposition given a set of rules? The prolog implementation of the Typol motor takes a set of rules, initial data, and a proposition. Some of the free variables of the proposition are instantiated with the initial data. Input data may be integers, strings, and abstract syntax trees. The motor then attempts to prove the proposition within the set of rules, instantiating the remaining free variables along the way. When the proposition may be proved, we usually retrieve the values of the newly instantiated variables
The initial value assigned to the subject of the proposition is usually the root of an abstract syntax tree. The Typol motor tries to prove the proposition by finding a rule whose subject pattern matches the proposition's subject tree. When a match occurs, the matching rule's hypotheses are instantiated to those of the proposition. Free variables of the rule's patterns are instantiated to corresponding subtrees in the proposition.
Once the motor finds a rule that matches a proposition, it attempts to prove recursively the premises of the rules. If the rule is an axiom, no further proof is necessary.
If, while the motor is trying to prove a rule, a premise fails, the rule does not prove the proposition. So the motor looks for another matching rule. In Typol, a proposition may not be proved if the motor finds no matching rules.
For example, we may ask the Typol motor to prove the following proposition:
|- Exp : integer N
given a set of rules. The variable Exp is bound to a source tree. The variable N is initially free. If the proposition may be proved, N will contain the single integer result of the evaluation.