Specification of the Trace file/output

  Specifying a trace file with the -t filename option of zdatrinf redirects all query related output from screen to the given file. Only when the manual input is enabled will results still be displayed on the console.

The quantity and quality of the trace file depends on the selected verbosity level of zdatrinf and ranges from showing just query results without the query or the final full stop at verbosity level -2, to a complete trace including all used rules and (for debugging purposes) all detected atoms and nodes at verbosity level 3.

With tracing enabled (verbosity level 1 or higher) several kinds of information about inferences are provided, including the inference rule number and:

=i,j,k> LOCAL localnode:< matchedpath || unmatched path > == rhs
        GLOBAL globalnode:< globalpath >

Small letters indicate variables:

• i current depth of the query counting from 0.
• j current depth of path recursions counting from 0.
• k current item on the right hand side counting from 0.
• localnode current local node name.
• matched path part of local path that was matched (matched prefix). If the complete path was matched, the double pipe symbol is omitted.
• unmatched path part of local path that was not matched (unmatched suffix).
• rhs the right hand side of the current equation.
• globalnode current global node name.
• globalpath current global path

To illustrate a typical trace presume the following (silly) theory:

	A:
	<> == ample
	<a> == <<b>>
	<b> == c
	<c> == <d> "A:<>"
	<d> == ex.

A typical output for verbosity level 1 is shown in the example below. The first line is the manual query input, the last two lines are the statistics and the result.

#1=> A:<a>
=0,0,0> LOCAL A:< a > == < < b > > 
        GLOBAL A:< a >
=1,1,0> LOCAL A:< b > == c 
        GLOBAL A:< a >
=1,0,0> LOCAL A:< c > == < d > "A: <  > " 
        GLOBAL A:< a >
=2,0,0> LOCAL A:< d > == ex 
        GLOBAL A:< a >
=2,0,1> LOCAL A:< > == ample 
        GLOBAL A:< >
[Query 1 (7 Inferences)] A:< a >
 = ex ample .