Using Weil-Founded Relations for Proving Operational Termination

摘要

In this paper, we study operational termination, a proof theoretical notion for capturing the termination behavior of computational systems. We prove that operational termination can be characterized at different levels by means of well-founded relations on specific formulas which can be obtained from the considered system. We show how to obtain such well-founded relations from logical models which can be automatically generated using existing tools.