left

Techniques working on CSRs

right
AProVE Help SystemTechniquesTechniques working on CSRs

The (innermost) termination analysis of Context Sensitive Term Rewriting Systems(CSRs) begins with the transformation of the given CSR to a TRS.

For termination all transformations are sound so it is sufficient to prove the termination of the original CSR by proving termination of the TRS.

For innermost termination the situation is different. Not all transformations are sound for innermost termination. The prover switches back to full termination after an unsound transformation was applied.

The prover also cares about the completeness. If (innermost) termination (for the transformed TRS) is disproved and the CSR to TRS-transformation is incomplete the prover discard the non-termination proof.

Transformations

transformation termination innermost
termination
Trivial
Lucas
Zantema
Ferreira-Ribeiro
incomplete Giesl-Middeldorp
Giesl-Middeldorp
Innermost-Giesl-Middeldorp
sound complete
yesno
yesno
yesno
yesno
yesno
yesyes
yesno
sound complete
nono
nono
nono
nono
yesno
yesno
yesyes
See [GM '02] for more details.