A simple correctness proof for magic transformation

DOI10.1017/S1471068411000032zbMath1255.68050arXiv1012.2299OpenAlexW2134148399MaRDI QIDQ4897705

Włodzimierz Drabent

Publication date: 27 December 2012

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1012.2299

zbMATH Keywords

operational semanticslogic programmingprogram correctnessdeclarative semanticsLD-resolutionmagic transformation

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Abstract interpretation: a kind of magic
• Proof methods of declarative properties of definite programs
• Inductive assertion method for logic pograms
• Reasoning about prolog programs: From modes through types to assertions
• On the power of magic
• Magic templates: a spellbinding approach to logic programs
• The s-semantics approach: Theory and applications
• Proving correctness and completeness of normal programs – a declarative approach

This page was built for publication: A simple correctness proof for magic transformation