Proof methods of declarative properties of definite programs

DOI10.1016/0304-3975(93)90107-5zbMath0783.68078OpenAlexW2094612221MaRDI QIDQ685395

Pierre Deransart

Publication date: 20 March 1994

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

Full work available at URL: https://hal.inria.fr/inria-00075310/file/RR-1248.pdf

zbMATH Keywords

specificationattribute grammarannotationinductive specificationpartial correctness of a logic program

Mathematics Subject Classification ID

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

Related Items (8)

Weakest preconditions for pure Prolog programs ⋮ On Correctness and Completeness of an n Queens Program ⋮ Logic + control: On program construction and verification ⋮ A simple correctness proof for magic transformation ⋮ An operational formal definition of PROLOG: A specification method and its application ⋮ Proving completeness of logic programs with the cut ⋮ Assertion based Inductive Verification Methods for Logic Programs ⋮ Modules and specifications

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Equational problems and disunification
• Definite clause grammars for language analysis - A survey of the formalism and a comparison with augmented transition networks
• An operational formal definition of PROLOG: A specification method and its application
• Attribute grammars. Definitions, systems and bibliography
• Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming
• A lattice-theoretical fixpoint theorem and its applications
• Equivalent logic programs
• Relating logic programs and attribute grammars
• Error diagnosis in logic programming an adaptation of E.Y. Shapiro's method
• Derivation of Logic Programs
• Contributions to the Theory of Logic Programming
• Proving termination properties of prolog programs: A semantic approach
• A New Incompleteness Result for Hoare's System
• Soundness and Completeness of an Axiom System for Program Verification
• Semantics of context-free languages: Correction

This page was built for publication: Proof methods of declarative properties of definite programs