An Isabelle/HOL Formalization of Rewriting 
for Certified Tool Assertions 
Overview Developers Input Format Related Work Versions Experiments TermFun

XML-Format (versions 1.02 - 1.05)

CeTA requires two input files, the first being the TRS, the second being the proof. The TRS has to be provided in the upcoming XML format for TPDB. There also is a converter to transform TPDB files to the XML format. (call java -jar tpdb2xtc.jar input.trs)

For the proof, the following XML format (schema, schema in graphical representation, XSLT translation to HTML, examples) is required where '*' denotes arbitrary repetition (including zero times), '+' denotes at least one repetition, and '?' means that the previous item is optional (i.e., occurs exactly once or not at all). A detailed description of each element can be found below:

⟨proof⟩≡<proof>⟨trsProof⟩</proof>
|<proof>⟨trsDisproof⟩</proof>
⟨trsProof⟩≡<rIsEmpty/>
|⟨ruleRemoval⟩
|⟨dpTrans⟩
⟨trsDisproof⟩≡<loop>⟨substitution⟩⟨context⟩⟨term⟩*</loop>
|<notWellFormed/>
⟨dpProof⟩≡<pIsEmpty/>
|⟨depGraphProc⟩
|⟨redPairProc⟩
|⟨redPairUrProc⟩
|⟨monoRedPairProc⟩
|⟨monoRedPairUrProc⟩
|⟨unlabProc⟩
|⟨semlabProc⟩
|⟨spscProc⟩
⟨depGraphProc⟩≡<depGraphProc>⟨component⟩*</depGraphProc>
⟨component⟩≡<component>⟨dps⟩⟨dpProof⟩?</component>
⟨dps⟩≡<dps><rules>⟨rule⟩*</rules></dps>
⟨trs⟩≡<trs><rules>⟨rule⟩*</rules></trs>
⟨usableRules⟩≡<usableRules><rules>⟨rule⟩*</rules></usableRules>
⟨rule⟩≡<rule><lhs>⟨term⟩</lhs><rhs>⟨term⟩</rhs></rule>
⟨redPairProc⟩≡<redPairProc>⟨redPair⟩⟨dps⟩⟨dpProof⟩</redPairProc>
⟨redPairUrProc⟩≡<redPairUrProc>⟨redPair⟩⟨dps⟩⟨usableRules⟩⟨dpProof⟩</redPairUrProc>
⟨monoRedPairProc⟩≡<monoRedPairProc>⟨redPair⟩⟨dps⟩⟨trs⟩⟨dpProof⟩</monoRedPairProc>
⟨monoRedPairUrProc⟩≡<monoRedPairUrProc>⟨redPair⟩⟨dps⟩⟨trs⟩⟨usableRules⟩⟨dpProof⟩</monoRedPairUrProc>
⟨unlabProc⟩≡<unlabProc>⟨dps⟩⟨trs⟩⟨dpProof⟩</unlabProc>
⟨semlabProc⟩≡<semlabProc>⟨model⟩⟨dps⟩⟨trs⟩⟨dpProof⟩</semlabProc>
⟨spscProc⟩≡<spscProc>⟨simpleProjection⟩⟨dps⟩⟨dpProof⟩</spscProc>
⟨ruleRemoval⟩≡<ruleRemoval>⟨redPair⟩⟨trs⟩⟨trsProof⟩</ruleRemoval>
⟨dpTrans⟩≡<dpTrans>⟨dps⟩⟨dpProof⟩</dpTrans>
⟨redPair⟩≡<redPair><interpretation>⟨type⟩⟨domain⟩⟨interpret⟩*</interpretation></redPair>
⟨type⟩≡<type><linearPolynomial/></type>
⟨domain⟩≡<domain><naturals/></domain>
⟨interpret⟩≡<interpret>⟨name⟩<arity>nonNegativeInteger</arity>⟨function⟩</interpret>
⟨function⟩≡<function><linearPolynomial>⟨constant⟩⟨coefficient⟩*</linearPolynomial></function>
⟨constant⟩≡<constant><number>integer</number></constant>
⟨coefficient⟩≡<coefficient>⟨natural⟩</coefficient>
⟨model⟩≡<model><carrierSize>positiveInteger</carrierSize>⟨interpret'⟩*</model>
⟨interpret'⟩≡<interpret>⟨name⟩<arity>nonNegativeInteger</arity>⟨arithFunction⟩</interpret>
⟨arithFunction⟩≡⟨natural⟩
|<variable>positiveInteger</variable>
|<sum>⟨arithFunction⟩+</sum>
|<product>⟨arithFunction⟩+</product>
|<minimum>⟨arithFunction⟩+</minimum>
|<maximum>⟨arithFunction⟩+</maximum>
⟨simpleProjection⟩≡<simpleProjection>⟨projEntry⟩*</simpleProjection>
⟨projEntry⟩≡<projEntry>⟨name⟩<argument>nonNegativeInteger</argument></projEntry>
⟨substitution⟩≡<substitution>(<substEntry>⟨var⟩⟨term⟩</substEntry>)*</substitution>
⟨context⟩≡<box/>
|<funContext>⟨name⟩⟨before⟩⟨context⟩⟨after⟩</funContext>
⟨before⟩≡<before>⟨term⟩*</before>
⟨after⟩≡<after>⟨term⟩*</after>
⟨term⟩≡⟨var⟩
|<funapp>⟨name⟩⟨arg⟩*</funapp>
⟨var⟩≡<var>string</var>
⟨name⟩≡<name>string⟨label⟩*</name>
|<name sharp=bool>string⟨label⟩*</name>
⟨label⟩≡<label>⟨natural⟩*</label>
⟨natural⟩≡<natural>nonNegativeInteger</natural>
⟨arg⟩≡<arg>⟨term⟩</arg>

Description

Processors

Input for versions < 1.02

TRSs are Haskell expressions of type 

[(Term String String, Term String String)]
Proofs have to be provided as Haskell expressions of type 
TRSProof String String
 A detailed description of the (Haskell) input format can be found below. Examples are provided on the results page (click on CeTA format for a TRS and on some green entry of the TTT2 column for a proof). One can either download all TRSs of TPDB 5.0 in CeTA format, or use these converters which transform TPDB files (in the current or the upcoming XML format for TPDB) into CeTA format. The converters require Java and xsltproc.

The following code contains all required data types. 

data Nat =
   Suc Nat
 | Zero_nat

newtype RedPair a = Polo [(a, (Nat, [Nat]))]

data Term a b =
   Fun a [Term a b]
 | Var b

data Ctxt a b =
   More a [Term a b] (Ctxt a b) [Term a b]
 | Hole

data Shp a =
   Plain a
 | Sharp a

data DPProof a b =
   DepGraphProc [(Maybe (DPProof a b), [(Term a b, Term a b)])]
 | RedPairProc (RedPair a) [(Term a b, Term a b)] (DPProof a b)
 | PisEmpty

data TRSProof a b =
   DPTrans [(Term (Shp a) b, Term (Shp a) b)] (DPProof (Shp a) b)
 | Loop ([Term a b], (Ctxt a b, [(Term a b, Term a b)]))

Description