Norms on terms and their use in proving universal termination of a logic program

DOI10.1016/0304-3975(92)00019-NzbMath0795.68040MaRDI QIDQ1318707

M. Fabris, Annalisa Bossi, Nicoletta Cocco

Publication date: 5 April 1994

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

universal terminationsubstitutionproof methodordering functionspre/post specificationspure Prolog programssemi-linear norms

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17)

Related Items (5)

A decidable subclass of finitary programs ⋮ Loop checking in SLD-derivations by well-quasi-ordering of goals ⋮ Termination Analysis of Logic Programs Based on Dependency Graphs ⋮ Computable Functions in ASP: Theory and Implementation ⋮ Automated modular termination proofs for real Prolog programs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Inductive assertion method for logic pograms
• Termination proofs for logic programs
• Reasoning about termination of pure Prolog programs

This page was built for publication: Norms on terms and their use in proving universal termination of a logic program