Certificates use an s-expression based format.
| ⟨nat⟩ ::= | 0 | 1 | 2 | ... | ||
| ⟨trs⟩ ::= | ⟨nat⟩ | ⟨nat⟩- | ||
| ⟨gtt⟩ ::= | (root-step(⟨trs⟩+ )) | (gsteps(⟨trs⟩+ )) | (inverse⟨gtt⟩) | ||
| | | (union⟨gtt⟩⟨gtt⟩) | (acomp⟨gtt⟩⟨gtt⟩) | (gcomp⟨gtt⟩⟨gtt⟩) | ||
| | | (inter⟨gtt⟩⟨gtt⟩) | (atc⟨gtt⟩) | (gtc⟨gtt⟩) | (acomplement⟨gtt⟩) | ||
| ⟨pos⟩ ::= | >= | e | > | ||
| ⟨num⟩ ::= | >= | 1 | > | ||
| ⟨rr1⟩ ::= | (terms) | (nf(⟨trs⟩+ )) | (inf⟨rr2⟩) | ||
| | | (proj(1|2)⟨rr2⟩) | (union⟨rr1⟩⟨rr1⟩) | ||
| | | (inter⟨rr1⟩⟨rr1⟩) | (diff⟨rr1⟩⟨rr1⟩) | ||
| ⟨rr2⟩ ::= | (gtt⟨gtt⟩⟨pos⟩⟨num⟩) | (product⟨rr1⟩⟨rr1⟩) | (id⟨rr1⟩) | ||
| | | (union⟨rr2⟩⟨rr2⟩) | (inter⟨rr2⟩⟨rr2⟩) | (diff⟨rr2⟩⟨rr2⟩) | ||
| | | (comp⟨rr2⟩⟨rr2⟩) | (inverse⟨rr2⟩) | (equality) | (reflcl⟨rr2⟩) | ||
| | | (step(⟨trs⟩+ )) | (step=(⟨trs⟩+ )) | (step+(⟨trs⟩+ )) | ||
| | | (step*(⟨trs⟩+ )) | (step!(⟨trs⟩+ )) | (par-step(⟨trs⟩+ )) | ||
| | | (root-step(⟨trs⟩+ )) | (root-step=(⟨trs⟩+ )) | ||
| | | (root-step+(⟨trs⟩+ )) | (root-step*(⟨trs⟩+ )) | ||
| | | (non-root-step(⟨trs⟩+ )) | (non-root-step=(⟨trs⟩+ )) | ||
| | | (non-root-step+(⟨trs⟩+ )) | (non-root-step*(⟨trs⟩+ )) | ||
| | | (meet(⟨trs⟩+ )) | (join(⟨trs⟩+ )) | ||
| ⟨term⟩ ::= | ⟨nat⟩ | ||
| ⟨formula⟩ ::= | (rr1⟨rr1⟩⟨term⟩) | (rr2⟨rr2⟩⟨term⟩⟨term⟩) | ||
| | | (and⟨formula⟩*) | (or⟨formula⟩*) | (not⟨formula⟩) | ||
| | | (forall⟨formula⟩) | (exists⟨formula⟩) | (true) | (false) | ||
| | | (restrict⟨formula⟩(⟨trs⟩+ )) | ||
| ⟨item⟩ ::= | ⟨nat⟩ | ||
| ⟨inference⟩ ::= | (rr1⟨rr1⟩⟨term⟩) | (rr2⟨rr2⟩⟨term⟩⟨term⟩) | (and⟨itemref⟩*) | ||
| | | (or⟨item⟩*) | (not⟨item⟩) | (exists⟨item⟩) | (nnf⟨itemref⟩) | ||
| ⟨info⟩ ::= | (size⟨nat⟩⟨nat⟩⟨nat⟩) | ||
| ⟨certificate⟩ ::= | (⟨item⟩⟨inference⟩⟨formula⟩⟨info⟩*)⟨certificate⟩ | ||
| | | (empty)⟨item⟩) | (nonempty⟨item⟩) | ||