Reasoning about termination of pure Prolog programs

DOI10.1006/inco.1993.1051zbMath0786.68021OpenAlexW2120869002MaRDI QIDQ1308986

Dino Pedreschi, Krzysztof R. Apt

Publication date: 12 December 1993

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/1494

zbMATH Keywords

verificationsemanticsterminationlogic programmingpartial correctnessacceptabilityinterpreterprologleast Herbrand model

Mathematics Subject Classification ID

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

Related Items (22)

Correctness and Completeness of Logic Programs ⋮ A declarative approach for first-order built-in's of Prolog ⋮ Logic programs and connectionist networks ⋮ Logic programs, iterated function systems, and recurrent radial basis function networks ⋮ First-order theories for pure Prolog programs with negation ⋮ Logic Programs under Three-Valued Łukasiewicz Semantics ⋮ A logical semantics for depth-first Prolog with ground negation ⋮ On Completeness of Logic Programs ⋮ A transformation of propositional Prolog programs into classical logic ⋮ Logic + control: On program construction and verification ⋮ Generalized metrics and uniquely determined logic programs. ⋮ Fully abstract compositional semantics for an algebra of logic programs ⋮ Proving completeness of logic programs with the cut ⋮ On the Coincidence of Semantics for Uniquely Determined Programs ⋮ \(\exists\)-Universal termination of logic programs ⋮ Semantics and expressive power of nondeterministic constructs in deductive databases ⋮ Totally correct logic program transformations via well-founded annotations ⋮ Termination prediction for general logic programs ⋮ Loop checking in SLD-derivations by well-quasi-ordering of goals ⋮ Some classes of Prolog programs inferable from positive data ⋮ Norms on terms and their use in proving universal termination of a logic program ⋮ Automated modular termination proofs for real Prolog programs

This page was built for publication: Reasoning about termination of pure Prolog programs