Proving termination properties of prolog programs: A semantic approach

DOI10.1016/0743-1066(92)90045-5MaRDI QIDQ4015950zbMATH OpenOpenAlexFDO

Authors Marianne Baudinet

Publication date 10 November 1992

Published in The Journal of Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0743-1066(92)90045-5

zbMATH Keywords

minimizationcutstructural inductionfirst order propertiesfirst order theorem provingfunctional semantics of Prolog

Mathematics Subject Classification ID

Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 3924108
• Proving termination of general Prolog programs
• Reasoning about termination of pure Prolog programs
• Transformational methodology for proving termination of logic programs
• scientific article; zbMATH DE number 879005

Cited in

(13)

• Automated modular termination proofs for real Prolog programs
• Reasoning about termination of pure Prolog programs
• A declarative approach for first-order built-in's of Prolog
• A logical semantics for depth-first Prolog with ground negation
• scientific article; zbMATH DE number 1973223 (Why is no real title available?)
• Verifying termination and reduction properties about higher-order logic programs
• Proof methods of declarative properties of definite programs
• MetateM: An introduction
• Proving termination of general Prolog programs
• Inference of Termination Conditions for Numerical Loops in Prolog
• A transformation of propositional Prolog programs into classical logic
• scientific article; zbMATH DE number 3995083 (Why is no real title available?)
• scientific article; zbMATH DE number 3924108 (Why is no real title available?)

This page was built for publication: Proving termination properties of prolog programs: A semantic approach

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4015950)