A Simple Correctness Proof for Magic Transformation
Logic in Computer Science
2010-12-13 v1 Databases
Programming Languages
Abstract
The paper presents a simple and concise proof of correctness of the magic transformation. We believe it may provide a useful example of formal reasoning about logic programs. The correctness property concerns the declarative semantics. The proof, however, refers to the operational semantics (LD-resolution) of the source programs. Its conciseness is due to applying a suitable proof method.
Keywords
Cite
@article{arxiv.1012.2299,
title = {A Simple Correctness Proof for Magic Transformation},
author = {Wlodzimierz Drabent},
journal= {arXiv preprint arXiv:1012.2299},
year = {2010}
}
Comments
Submitted to "Theory and Practice of Logic Programming"