The RISC ProofNavigator Tutorial and Manual -- E Context Directory

E Context Directory

The system generates the following files in the context directory:

cvcl.log

A log file describing the interaction between the system and the CVCL instance used for automatically verifying the type checking conditions generated in declaration mode. This file can be erased after a session without consequence.

cvcl0.log

A log file describing the interaction between the system and the CVCL instances used to simplify formulas in a proof state respectively close a proof state. This file can be erased after a session without consequence (and perhaps should be erased, since it can become very large).

*.xhtml

A collection of files presenting the declarations and proof states in XHTML+MathML format. The files use the following DOCTYPE declaration specified by W3C (see Section "A.2.3 MathML as a DTD Module" of [6]):

<!DOCTYPE html PUBLIC 
  "-//W3C//DTD XHTML 1.1 plus MathML 2.0//EN" 
  "http://www.w3.org/TR/MathML2/dtd/xhtml-math11-f.dtd">

The files are primarily intended for internal use by the graphical user interface of the system. However, after a session they can be also copied to another location for the persistent presentation of declarations and proofs. The files can be viewed by any Web browser that understands above document type, e.g. the browsers of the Mozilla suite (as well the former Mozilla browser as the current Firefox and SeaMonkey browsers). Most notably, the MicroSoft Internet Explorer Version 6 does not understand these declarations and thus cannot be used for viewing the files. The entry files to the presentations are:

decl-list.xhtml: The list of declarations issued in declaration mode.
F.xhtml: The proof of formula F.

kind_name_*.*

For every declaration of a constant name of a particular kind (type, value, formula), four files are generated that are mainly used to maintain declaration and proof dependencies across different sessions of the system and thus allow to assess the status of a proof generated in a previous session with respect to the declarations of the current session.

kind_name_decl.xgz: This is an XML file compressed with the compression tool gzip; its plain XML content can be printed with the tool zcat. The file contains an OMDoc [10] representation of the declaration with mathematical objects represented according to the OpenMath (OM) standard [5] using as far as possible symbols from standard OM content dictionaries; if for some concept of the specification language no appropriate standard symbol exists, an ad-hoc symbol with the content dictionary prefix fmrisc is used instead. These files are actually not (yet) used by the system; in a future version they may provide a bridge to third-party tools understanding OMDoc.
kind_name_hash.txt: This is a text file that contains a single decimal number representing a hash code for the declaration. If the hash code of the declaration in the current session coincides with the value stored in this file in a previous session, it is assumed that this declaration has not changed since then.
kind_name_time.txt: This is a text file that contains a single decimal number representing the time stamp when the corresponding constant declaration has been generated respectively the definition of the constant has most recently changed.
kind_name_refs.xml: This is an XML file that lists all entities referenced by the corresponding constant together with the values of their time stamps. If the definition of a referenced entity changes in a subsequent session, the value in its time stamp file is updated and does not coincide any more with the value listed in this file. This discrepancy is consequently detected and reflected in the status of a proof depending on this constant.

proof_name_*.*

For every proof of formula name, two files are generated that allow to assess the status of a proof in a later session (with respect to the declarations of that session) and to replay the proof.

proof_name_decl.xgz: This is an XML file compressed with the compressed with the compression tool gzip; its plain XML content can be printed with the tool zcat. The file describes the tree structure of the proof including the proof commands issued at every node of the tree in an ad-hoc XML format. Specification language entities used in these commands are described according to to the OpenMath (OM) standard [5] using as far as possible symbols from standard OM content dictionaries; if for some concept of the specification language no appropriate standard symbol exists, an ad-hoc symbol with the content dictionary prefix fmrisc is used instead.
proof_name_refs.xgz: This is an XML file that lists all entities referenced by the proof together with the values of their time stamps (as already discussed above).

For illustration of the content of the *_decl.xgz files, let us consider the example of Section 3.1 with declarations

sum: NAT->NAT;
S1: AXIOM sum(0)=0;
S2: AXIOM FORALL(n:NAT): n>0 => sum(n)=n+sum(n-1);
S: FORMULA FORALL(n:NAT): sum(n) = (n+1)*n/2;

and proof

[tca]: induction n byu
  [dbj]: proved (CVCL)
  [ebj]: auto
    [k5f]: proved (CVCL)

The contents of the correspondingly generated declaration and proof files are (after uncompression) as follows:

value_sum_decl.xgz

<?xml version="1.0" encoding="UTF-8"?>
<omdoc:omgroup 
  xmlns:omdoc="http://www.mathweb.org/omdoc" 
  xmlns:fmrisc="http://www.risc.uni-linz.ac.at/FM-RISC" 
  xmlns:om="http://www.openmath.org/OpenMath">
  <omdoc:symbol kind="object" name="sum">
    <omdoc:type system="simply_typed" xml:id="sum_type">
      <om:OMA>
        <om:OMS cd="sts" name="mapsto"/>
        <om:OMA>
          <om:OMS cd="set1" name="cartesian_product"/>
          <om:OMS cd="setname1" name="N"/>
        </om:OMA>
        <om:OMS cd="setname1" name="N"/>
      </om:OMA>
    </omdoc:type>
  </omdoc:symbol>
</omdoc:omgroup>

formula_S1_decl.xgz

<?xml version="1.0" encoding="UTF-8"?>
<omdoc:omgroup 
  xmlns:omdoc="http://www.mathweb.org/omdoc" 
  xmlns:fmrisc="http://www.risc.uni-linz.ac.at/FM-RISC" 
  xmlns:om="http://www.openmath.org/OpenMath">
  <omdoc:assertion type="axiom" xml:id="S1">
    <om:FMP>
      <om:OMA>
        <om:OMS cd="relation1" name="eq"/>
        <om:OMA>
          <om:OMV name="sum"/>
          <om:OMI>0</om:OMI>
        </om:OMA>
         <om:OMI>0</om:OMI>
      </om:OMA>
     </om:FMP>
   </omdoc:assertion>
</omdoc:omgroup>

formula_S2_decl.xgz

<?xml version="1.0" encoding="UTF-8"?>
<omdoc:omgroup 
  xmlns:omdoc="http://www.mathweb.org/omdoc" 
  xmlns:fmrisc="http://www.risc.uni-linz.ac.at/FM-RISC" 
  xmlns:om="http://www.openmath.org/OpenMath">
  <omdoc:assertion type="axiom" xml:id="S2">
    <om:FMP>
      <om:OMBIND>
        <om:OMS cd="quant1" name="forall"/>
        <om:OMBVAR>
          <om:OMATTR>
            <om:OMATP>
              <om:OMS cd="sts" name="type"/>
              <om:OMS cd="setname1" name="N"/>
            </om:OMATP>
            <om:OMV name="n"/>
          </om:OMATTR>
        </om:OMBVAR>
        <om:OMA>
          <om:OMS cd="logic1" name="implies"/>
          <om:OMA>
            <om:OMS cd="relation1" name="gt"/>
            <om:OMV name="n"/>
            <om:OMI>0</om:OMI>
          </om:OMA>
          <om:OMA>
            <om:OMS cd="relation1" name="eq"/>
            <om:OMA>
              <om:OMV name="sum"/>
              <om:OMV name="n"/>
            </om:OMA>
            <om:OMA>
              <om:OMS cd="arith1" name="plus"/>
              <om:OMV name="n"/>
              <om:OMA>
                <om:OMV name="sum"/>
                <om:OMA>
                  <om:OMS cd="arith1" name="minus"/>
                  <om:OMV name="n"/>
                  <om:OMI>1</om:OMI>
                </om:OMA>
              </om:OMA>
            </om:OMA>
          </om:OMA>
        </om:OMA>
      </om:OMBIND>
    </om:FMP>
  </omdoc:assertion>
</omdoc:omgroup>

formula_S_decl.xgz

<?xml version="1.0" encoding="UTF-8"?>
<omdoc:omgroup 
  xmlns:omdoc="http://www.mathweb.org/omdoc" 
  xmlns:fmrisc="http://www.risc.uni-linz.ac.at/FM-RISC" 
  xmlns:om="http://www.openmath.org/OpenMath">
  <omdoc:assertion type="formula" xml:id="S">
    <om:FMP>
      <om:OMBIND>
        <om:OMS cd="quant1" name="forall"/>
        <om:OMBVAR>
          <om:OMATTR>
            <om:OMATP>
              <om:OMS cd="sts" name="type"/>
              <om:OMS cd="setname1" name="N"/>
            </om:OMATP>
            <om:OMV name="n"/>
          </om:OMATTR>
        </om:OMBVAR>
        <om:OMA>
          <om:OMS cd="relation1" name="eq"/>
          <om:OMA>
            <om:OMV name="sum"/>
            <om:OMV name="n"/>
          </om:OMA>
          <om:OMA>
            <om:OMS cd="arith1" name="divide"/>
            <om:OMA>
              <om:OMS cd="arith2" name="times"/>
              <om:OMA>
                <om:OMS cd="arith1" name="plus"/>
                <om:OMV name="n"/>
                <om:OMI>1</om:OMI>
              </om:OMA>
              <om:OMV name="n"/>
            </om:OMA>
            <om:OMI>2</om:OMI>
          </om:OMA>
        </om:OMA>
      </om:OMBIND>
    </om:FMP>
  </omdoc:assertion>
</omdoc:omgroup>

proof_S_decl.xgz

<?xml version="1.0" encoding="UTF-8"?>
<fmrisc:proof 
  xmlns:fmrisc="http://www.risc.uni-linz.ac.at/FM-RISC" 
  xmlns:om="http://www.openmath.org/OpenMath" 
  closed="true" autosimplify="true" name="S">
  <fmrisc:state>
    <fmrisc:command name="induction">
      <om:OMV name="n"/>
      <fmrisc:label>byu</fmrisc:label>
    </fmrisc:command>
    <fmrisc:state>
      <fmrisc:command name="proved">CVCL</fmrisc:command>
    </fmrisc:state>
    <fmrisc:state>
      <fmrisc:command name="auto"/>
      <fmrisc:state>
        <fmrisc:command name="proved">CVCL</fmrisc:command>
      </fmrisc:state>
    </fmrisc:state>
  </fmrisc:state>
</fmrisc:proof>

E Context Directory