Termination and Reduction Checking for Higher-Order Logic Programs

10 years 7 months ago
Termination and Reduction Checking for Higher-Order Logic Programs
In this paper, we present a syntax-directed termination and reduction checker for higher-order logic programs. The reduction checker verifies parametric higher-order subterm orderings describing relations between input and output of well-moded predicates. These reduction constraints are exploited during termination checking to infer that a specified termination order holds. To reason about parametric higher-order subterm orderings, we introduce a deductive system as a logical foundation for proving termination. This allows the study of proof-theoretical properties, such as consistency, local soundness and completeness and decidability. We concentrate here on proving consistency of the presented inference system. The termination and reduction checker are implemented as part of the Twelf system and enable us to verify proofs by complete induction.
Brigitte Pientka
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2001
Where CADE
Authors Brigitte Pientka
Comments (0)