Next: cd
Up: add: Adding Input
Previous: Examples
Contents
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
must be an atom
, or a pair
[
] of atoms, representing one or two file names,
respectively.
In the second form of the command,
is supposed to specify
the name of the file containing the meta-logical directives,
while
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
.ord.
If a file by that name exists, it is assumed that it contains
relevant meta-logical information associated with
.
In that case, in(
) is equivalent to
in([
.ord,
]).
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
.o
are dumped, partially saturated theory modules.
If a file by that name exists, in(
) will
read
.o rather than
itself.
In cases where this default behaviour is not wanted, addsrc(
)
should be used, which is otherwise equivalent to in(
).
Next: cd
Up: add: Adding Input
Previous: Examples
Contents
Harald Ganzinger
2002-12-04
Imprint | Data Protection