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

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

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