<file:/home/connolly/w3ccvs/WWW/2000/10/swap/test/reason/a> <file:/home/connolly/w3ccvs/WWW/2000/10/swap/test/reason/b> <file:/home/connolly/w3ccvs/WWW/2000/10/swap/test/reason/c> . 2006-02-18T04:04:04Z @@step A binding is given eg in a proof or query result binding The step of conjunction introduction: taking a bunch of compent statements and building a formula from them. The step of taking one statement out of a formula. The step is identified by the :gives formula (the statement) and the :because step's :gives formula (the formula extracted from). Conjunction elimination The formula given was derived from parsing a resource. parsing A Proof step is the last step in the proof, a step which :gives that which was to be proved. Typically a document will assert just one :Proof, which a checker can then check and turn into the Formula proved - Q.E.D. . proof A step in a proof. See :gives for the arc to the formula proved at this step. proof step gives the step whose data was input to this step. because This binding binds its variable to this term. bound to A step whose data was used in building this conjunction component gives The source document which was parsed. source The given string is that used as the identifier of the variable which is bound by this binding. The variable name has to be given as a string, rather than the variable being put here, or the variable would be treated as a variable. variable