Separating Logic and Meta-Logical Directives

We suggest (but do not strictly require) that ordering declarations and other meta-logical directives be kept separate from theory presentations. In the add and addsrc commands $I$ must be an atom $F$, or a pair [$FO,F$] of atoms, representing one or two file names, respectively. In the second form of the command, $FO$ is supposed to specify the name of the file containing the meta-logical directives, while $F$ is supposed to denote the file containing the theory. When using the first form of the command, the system checks for the presence of a file named $F$.ord. If a file by that name exists, it is assumed that it contains relevant meta-logical information associated with $F$. In that case, in($F$) is equivalent to in([$F$.ord,$F$]).

Theories may exist in different presentations. In particular it is possible to dump a (partially) saturated theory module to a file and read it back in later (cf. out command). In that case inferences will not be (re-)computed if each premise belongs to the (same) theory module. For fully saturated theories such a linear strategy is complete. For partially completed theories it may be incomplete but nevertheless be be useful as a strategy. It is assumed that files with names of the form $F$.o are dumped, partially saturated theory modules. If a file by that name exists, in($F$) will read $F$.o rather than $F$ itself. In cases where this default behaviour is not wanted, addsrc($F$) should be used, which is otherwise equivalent to in($F$).

Imprint | Data Protection