Termination proofs for logic programs

zbMath0705.68090MaRDI QIDQ1188722

Lutz Plümer

Publication date: 23 January 1993

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

zbMATH Keywords

recursionlogic programsSLD-resolutiontermination proofsHerbrand universepredicate inequalities

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Logic programming (68N17)

Related Items (12)

On proving the termination of algorithms by machine ⋮ Verifying termination and reduction properties about higher-order logic programs ⋮ Proving termination of general Prolog programs ⋮ A logical semantics for depth-first Prolog with ground negation ⋮ A framework for incremental learning of logic programs ⋮ A general criterion for avoiding infinite unfolding during partial deduction ⋮ \(\exists\)-Universal termination of logic programs ⋮ Some classes of Prolog programs inferable from positive data ⋮ Termination Analysis of Logic Programs Based on Dependency Graphs ⋮ Norms on terms and their use in proving universal termination of a logic program ⋮ Deriving fold/unfold transformations of logic programs using extended OLDT-based abstract interpretation ⋮ Termination analysis for partial functions

This page was built for publication: Termination proofs for logic programs