© University of Kent - Contact | Feedback | Legal | FOI | Cookies
An Isomorphism between Abstract Polyhedral Cones and Definite Boolean Functions
F. Benoy and A. King
Technical Report 3-99, Computing Laboratory, University of Kent, March 1999.Abstract
Polyhedral cones can be represented by sets of linear inequalities that express inter-variable relationships. These inequalities express inter-variable relationships that are quantified by the ratios between the variable coefficients. However, linear inequalities over a non-negative variable domain with only unit variable coefficients and no constants other than zero can represent relationships that can be valid in non-numeric domains. For instance, if variables are either non-negative or zero itself, that is, a strictly two-point domain, then {0 <= x, 0 <= y, x <= y}, expresses a dependency between x and y, since if y is known to be zero, then so is x. By defining an abstraction operator that effectively puts aside the scaling coefficients whilst retaining the inter-variable aspect of these relationships polyhedral cones can express the same dependency information as Def, a class of Boolean function. Boolean functions are considered over a fixed finite set of variables and Def is a subset of the positive Boolean functions, which return the value true when every variable returns true. Def is a complete lattice ordered by logical consequence and it will be shown that the abstract cones also form a complete lattice, ordered by set inclusion, that is isomorphic to Def.
Download publication 88 kbytes
Bibtex Record
@techreport{707,
author = {F. Benoy and A. King},
title = {{A}n {I}somorphism between {A}bstract {P}olyhedral {C}ones and {D}efinite {B}oolean {F}unctions},
month = {March},
year = {1999},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1999/707},
address = {University of Kent},
institution = {Computing Laboratory},
number = {3-99},
}