School of Computing

Mutual Exclusion by Interpolation

Jael Kriener and Andy King

In Tom Schrijvers and Peter Thiemann, editors, Eleventh International Symposium on Functional and Logic Programming, volume 7294 of Lecture Notes in Computer Science, pages 182-196, Kobe, Japan, May 2012. Springer.

Abstract

The question of what constraints must hold for a predicate to behave as a (partial) function, is key to understanding the behaviour of a logic program. It has been shown how this question can be answered by combining backward analysis, a form of analysis that propagates determinacy requirements against the control flow, with a component for deriving so-called mutual exclusion conditions. The latter infers conditions sufficient to ensure that if one clause yields an answer then another cannot. This paper addresses the challenge of how to compute these conditions by showing that this problem can be reformulated as that of vertex enumeration. Whilst directly applicable in logic programming, the method might well also find application in reasoning about type classes.

Download publication 355 kbytes (PDF)

Bibtex Record

@inproceedings{3201,
author = {Jael Kriener and Andy King},
title = {Mutual {E}xclusion by {I}nterpolation},
month = {May},
year = {2012},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2012/3201},
    publication_type = {inproceedings},
    submission_id = {26084_1328691067},
    booktitle = {Eleventh International Symposium on Functional and Logic Programming},
    editor = {Tom Schrijvers and Peter Thiemann},
    series = {Lecture Notes in Computer Science},
    address = {Kobe, Japan},
    publisher = {Springer},
    refereed = {yes},
    volume = {7294},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014