Change search
ReferencesLink to record
Permanent link

Direct link
A simple correctness proof for magic transformation
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
2012 (English)In: Theory and Practice of Logic Programming, ISSN 1471-0684, E-ISSN 1475-3081, Vol. 12, no 6, 929-936 p.Article in journal (Refereed) Published
Abstract [en]

The paper presents a simple and concise proof of correctness of the magic transformation. We believe that 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.

Place, publisher, year, edition, pages
Cambridge University Press (CUP) , 2012. Vol. 12, no 6, 929-936 p.
Keyword [en]
program correctness, logic programming, magic transformation, declarative semantics, LD-resolution, operational semantics
National Category
Engineering and Technology
URN: urn:nbn:se:liu:diva-86115DOI: 10.1017/S1471068411000032ISI: 000310854200004OAI: diva2:574981
Available from: 2012-12-07 Created: 2012-12-07 Last updated: 2012-12-21

Open Access in DiVA

fulltext(172 kB)119 downloads
File information
File name FULLTEXT01.pdfFile size 172 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Drabent, Wlodzimierz
By organisation
Software and SystemsThe Institute of Technology
In the same journal
Theory and Practice of Logic Programming
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 119 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 90 hits
ReferencesLink to record
Permanent link

Direct link