[Termtools] Termination Problem/Proof Formats (discussion at WScT08)

[Johannes Waldmann]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Dear colleagues,

here is a very short status report from the Workshop
on Certified Termination that was held in Leipzig recently.

In fact, you'll find all the information in the Wiki
http://termination-portal.org/wiki/WScT08
so I will only add one comment here,
on the direction of further activities.

We agreed that the current TPG (termination proof format)
should be extended to be more verbose,
to make life easier for the verifier,
and also to achieve compatibility with other backends.
The idea is: when in doubt, include more information.

I suggest an immediate step would be to enrich
the current "rainbow proof format" by making the nodes
self-contained. In other words, each node should contain
not only the proof, but also the property that is being proved.

For that, we need an (XML) format for termination properties
as they might appear during a many-step proof. (Rainbow already
contains a format for "initial" termination problems: problem.xsd,
and we may start there.)

This (XML) termination property format will also be needed
by the competition organiziers, for storing problems in the data base.
There is a proposal here:
http://termination-portal.org/wiki/TPDB_XML_Format
that necessarily contains both annotations (e.g. author, submitter, ...)
and semantics (set of rules, strategy, ...)
I think the "semantics part" and "rainbow:problem.xsd"
should converge.

This would simplify matters (only one format)
and also allow for modular provers and prover combinators
(i.e. the "control language" idea that comes up every now and then).

Best regards, Johannes.







-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.9 (GNU/Linux)
Comment: Using GnuPG with SUSE - http://enigmail.mozdev.org

iEYEARECAAYFAkhD+LgACgkQDqiTJ5Q4dm9+lwCfQThHWOSYuuQT9SbCTiJzxcwF
DY0AoJKUGDLZBLdeOrgh2DKRFHiRd0u3
=tGZm
-----END PGP SIGNATURE-----