E Context Directory |
The system generates the following files in the context directory:
<!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:
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:
<?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>
<?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>
<?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>
<?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>
<?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 |