Next: Signature declarations
Up: Natural Deduction Language
Previous: Input phrases
  Contents
NDL scripts
A script is simply a sequence of phrases (signature declarations,
assertions, deductions, and file-loading directives), possibly separated
by periods. The following is a sample script:
Functions f:1, g:2.
Relations P:1, Q:1, loves:2.
Constants Mary, Tom.
assert (forall x (Tom loves x)).
assume Mary loves Tom
begin
specialize (forall x (Tom loves x)) with Mary;
both Tom loves Mary, Mary loves Tom
end
Here Functions f:1, g:2 is a declaration of function symbols:
f and g are declared to be function symbols of arity
1 and 2, respectively. Similarly, the declaration Relations P:1, Q:1,
R:2 declares P and Q to be unary relation symbols (of
arity 1) and loves to be a binary relation symbol (of arity 2).
Finally, Constants Tom, Mary introduces Tom and Mary
as constant symbols.
2004-08-04