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)

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

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)