Will cetera use a different format than ceta?
right now, yes. See example below. That's part laziness - I just write "deriving (Read, Show)", and part design - I do like this format, it is less verbose, and more readable, than CPF. Well, this only matters for small certificates. Regardless of size - a Haskell data declaration is a much nicer specification than an XML schema (more concise, easier to machine-check). I think.
We use a uniform input format for solvers, so I guess it would be nice to have a uniform input format for certifiers as well (if possible)?
yes that is also a nice goal. I'm not too sure about running matchbox+cetera in termcomp now. It would just be a demonstration. If it's too much work for you, then we postpone. Another complication (for termcomp - for me, it's a simplification) is that I have Haskell syntax for SRS as well (see example) and letters must be natural numbers. Let's do "--cert" (meaning CPF/Ceta) for now (as you suggested) and discuss choice of formats/verifiers later (at WST). There _were_ several options for verification in the past. Then XML won? Cf. https://termination-portal.org/wiki/WScT08 (2008) - Johannes Certificate { system = [ Rule { lhs = [0,0,1,1], rhs = [1,1,1,0,0,0] } ] , reason = MatrixInterpretation { minterpretation = MatrixInterpretation { dim = 5 , int = [ (0, [[1,0,0,1,0] ,[0,0,0,2,0] ,[0,0,0,1,0] ,[0,0,1,0,0] ,[0,0,0,0,1]]) , (1, [[1,0,0,0,0] ,[0,0,1,2,1] ,[0,1,0,0,0] ,[0,0,0,0,0] ,[0,0,0,0,1]]) ] } , remove = [ Rule { lhs = [0,0,1,1], rhs = [1,1,1,0,0,0] } ] , sub = Certificate { system = [] , reason = Empty } } }