Date Added: Feb 2012
Logic programming has traditionally lacked devices for expressing mutually exclusive goals and queries. The authors address this limitation by adopting choice-disjunctive goal formulas of the form G1 - G2 where G1, G2 are goals and is a linear logic connective. These goals have the following operational semantics: choose and solve a true disjunct Gi where I (= 1 or 2) is chosen by the machine. It is worth noting that their operational semantics obtains mutual exclusion by choosing one between two disjuncts. Thus, their operational semantics of corresponds well to its declarative semantics known as the machine's choice.