Inductive assertion method for logic pograms

DOI10.1016/0304-3975(88)90099-0zbMATHOpenAlexMaRDI QIDQ1105352FDO

Authors Włodzimierz Drabent, Jan Maluszyński

Publication date 1988

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

Full work available at URL https://doi.org/10.1016/0304-3975(88)90099-0

zbMATH Keywords

backtrackingpartial correctnessProloglogic programsdeclarative semanticsinductive assertion methodOR-parallelism

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 4037276
• Logic programs as specifications in the inductive verification of logic programs
• Proof methods of declarative properties of definite programs
• scientific article; zbMATH DE number 2085284
• Assertion based inductive verification methods for logic programs

Cites work

• scientific article; zbMATH DE number 3872640 (Why is no real title available?)
• scientific article; zbMATH DE number 3924108 (Why is no real title available?)
• scientific article; zbMATH DE number 4037276 (Why is no real title available?)
• scientific article; zbMATH DE number 44976 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• A language of specified programs
• An axiomatic basis for computer programming
• Contributions to the Theory of Logic Programming
• Derivation of Logic Programs
• Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming
• Relating logic programs and attribute grammars
• Some global optimizations for a PROLOG compiler

Cited in

(15)

• scientific article; zbMATH DE number 3874578 (Why is no real title available?)
• The Prolog debugger and declarative programming
• On definite program answers and least Herbrand models
• scientific article; zbMATH DE number 4037276 (Why is no real title available?)
• On the verification of finite failure
• Proof method of partial correctness and weak completeness for normal logic programs
• Norms on terms and their use in proving universal termination of a logic program
• S-semantics -- an example
• Reasoning about prolog programs: From modes through types to assertions
• Logic programs as specifications in the inductive verification of logic programs
• A simple correctness proof for magic transformation
• Proving completeness of logic programs with the cut
• Weakest preconditions for pure Prolog programs
• Correctness and completeness of logic programs
• Inductive assertions and operational semantics

This page was built for publication: Inductive assertion method for logic pograms

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