Computer Science – Logic in Computer Science
Scientific paper
2000-12-21
Computer Science
Logic in Computer Science
Submission to ACM Transactions on Computational Logic
Scientific paper
We consider the problem of searching for proofs in sequential presentations of logics with multiplicative (or intensional) connectives. Specifically, we start with the multiplicative fragment of linear logic and extend, on the one hand, to linear logic with its additives and, on the other, to the additives of the logic of bunched implications, BI. We give an algebraic method for calculating the distribution of the side-formulae in multiplicative rules which allows the occurrence or non-occurrence of a formula on a branch of a proof to be determined once sufficient information is available. Each formula in the conclusion of such a rule is assigned a Boolean expression. As a search proceeds, a set of Boolean constraint equations is generated. We show that a solution to such a set of equations determines a proof corresponding to the given search. We explain a range of strategies, from the lazy to the eager, for solving sets of constraint equations. We indicate how to apply our methods systematically to large family of relevant systems.
Harland James
Pym David
No associations
LandOfFree
Resource-distribution via Boolean constraints does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Resource-distribution via Boolean constraints, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Resource-distribution via Boolean constraints will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-662554