Consult Syntax

A theory text is a set of lines usually read in from a file. Each line is first converted by the term syntax and then interpreted according to the text syntax. The main purpose of a theory text is to provide an ordered collection of premises. Among the premises we find facts and rules. Rules consist of a head and of a body, separated by the implication operator (“:-“). Facts consist only of a head. Facts can be considered to be rules where the body corresponds to then atom “true”, which can then be omitted. 

theory	  --> { sentence "." }.
sentence --> part [ "/\" sentence ] | "unit".
part --> clause | directive.

clause --> head ":-" body | head.
head      --> callable.

directive --> ":-" body.
body      --> goal [ "," body ] | "true".
goal --> callable | variable.

callable --> atom | compound.


in(X,[X|_]).                  % is a fact.
in(X,[_|Y]) :- in(X,Y).       % is a rule.
:- op(800, xfx, in).          % is a directive.

Besides facts and rules a theory text can also include directives. Directives are detected by a degenerated implication operator (“:-“) which is used prefix position. Whenever a directive is encountered in a theory text, the interpreter is invoked to solve the goal against the current state of the interpreter. Solutions to directives are not printed and directives are only solved once. The most typical directive is the operator definition directive. But the application of directives is not limited to operator definitions.

To avoid common typing errors a number of sanity checks are performed on facts and rules. Among these checks we find the singleton variable check. This check assures that anonymous variables (“_”) are used for variables that occur only once in a fact or rule. We also find the discontinued predicate check and the multi-file predicate check. These checks assures that in the normal case all the facts and rules for a predicate are defined in one row and that they only come from one source.

The head of a rule or fact needs to be a callable. That is it has to be either an atom or a compound. It is not possible to have rules or facts for numbers or variables. Internally the Prolog interpreter only supports natively conjunctions (,)/2 in the body. All other constructs in the body have to refer to predicates defined in the knowledge base. This includes logical predicates such as (,)/2, (;)/2, (->)/2 and (\+)/1 which are predefined defined by the system. If a predicate cannot be found an existence exception is thrown during execution.

It is possible to combine multiple clauses and directives into a single input line by means of the (/\)/2 operator or to indicate no clause and no directive by the atom “unit”. This is useful for returning multiple clauses and directives by term expansion. The operator (/\)/2 has been chosen in remembrance of hypothetical reasoning but it works slightly different. Clauses and directives that are joined via (/\)/2 during consult give not raise to inter-clausal variables. The individual clauses are still automatically universally quantified.