Specification of the Declaration file

 

When using a DATR theory, the declaration file permits easy generation of large numbers of theorems. Three different tags are currently supported:
# node, # show and # showif.

• # node followed by a list of nodes, delimited with a single dot, declares the set of nodes which should not be used in the forthcoming queries. Example:
  # hide Node1 Node2 Node3 .
• # show followed by a list of paths, delimimed with a single dot, too, declares the paths, which will be automatically queried with the not hidden nodes. Example:
  # show <path one> <path two> <path three> .
• # showif is succeeded by a conditional clause of the form
  <ifpath> = ifresult:
  followed by a list of paths similar to the # show tag. All not hidden nodes will be queried with all listed paths if, and only if, the query with the ifpath leads to the ifresult. As usual, any number of WHITESPACE characters may appear between the tag and the '#' character, and '%' comments can be used. Example:
  # showif <fact> = true :
  <path five> <path six> .

Further examples can be found in Appendix 6.2.