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.

• Type: Conference
• Year: 2001
• Where: CADE
• Authors: Brigitte Pientka
• Keywords: Automated Reasoning, CADE 2001, Orderings Describing Relations, Presented Inference System, Reduction Checker