next up previous contents
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