TypiCal

We give a new elegant proof that decreasing diagrams imply conflu-
ence based on a proof reduction technique, which is then the basis of a novel
completion method which proof-reduction relation transforms arbitrary proofs
into rewrite proofs even in presence of non-terminating reductions. Unlike pre-
vious methods, no ordering of the set of terms is required, but can be used if
available. Unlike ordered completion, rewrite proofs are closed under
instantiation. Examples are presented, including Kleene’s and Huet’s classical examples
showing that non-terminating local-confluent relations may not be confluent.

Joint work with Vincent van Oostrom (cf. ICALP 09)