Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.1 6/24/83; site fortune.UUCP
Path: utzoo!linus!security!genrad!decvax!duke!mcnc!rpw3@fortune.UUCP
From: rpw3@fortune.UUCP
Newsgroups: net.ai
Subject: Re: Re: a trivial reasoning problem? - (nf)
Message-ID: <2135@fortune.UUCP>
Date: Sun, 1-Jan-84 04:01:50 EST
Article-I.D.: fortune.2135
Posted: Sun Jan  1 04:01:50 1984
Date-Received: Mon, 2-Jan-84 02:18:23 EST
Sender: notes@fortune.UUCP
Organization: Fortune Systems, Redwood City, CA
Lines: 53

#R:sri-arpa:-1496200:fortune:21500006:000:2210
fortune!rpw3    Dec 31 20:31:00 1983

Gee, and to a non-Prolog person (me) your problem seemed so simple
(even given the no-exhaustive-search rule). Let's see,

	1. At least one of A or B is on = (A v B)
	2. If A is on, B is not		= (A -> ~B) = (~A v (~B)) [def'n of ->]
	3. A and B are binary conditions.

>From #3, we are allowed to use first-order Boolean algebra (WFF'n'PROOF game).
(That is, #3 is a meta-condition.)

So, #1 and #2 together is just (#1) ^ (#2) [using caret ^ for disjunction]

or,		#1 ^ #2	= (A v B) ^ (~A v ~B)
(distributivity)	= (A ^ ~A) v (A ^ ~B) v (B ^ ~A) v (B ^ ~B)
(from #3 and ^-axiom)	= (A ^ ~B) v (B ^ ~A)
(def'n of xor)		= A xor B

Hmmm... Maybe I am missing your original question altogether. Is your real
question "How does one enumerate the elements of a state-space (powerset)
for which a certain logical proposition is true without enumerating (examining)
elements of the state-space for which the proposition is false?"?

To me (an ignorant "non-ai" person), this seems excluded by a version of the
First Law of Thermodynamics, namely, the Law of the Excluded Miraculous Sort
(i.e. to tell which of two elements is bigger, you have to look at both).

It seems to me that you must at least look at SOME of the states for which the
proposition is false, or equivalently, you must use the structure of the
formula itself to do the selection (say, while doing a tree-walk). The problem
of the former approach is that the number of "bad" states should be kept
small (for efficiency), leading to all kinds of pruning heuristics; while
for the latter method the problem of elimination of duplicates (assuming
parallel processing) leads to the former method!

In either case, however, reasoning about the variables does not seem to
solve the problem; one must reason about the formulae. If Prolog admits
of constructing such meta-rules, you may have a chance. (I.e., "For all
true formula 'X xor Y', only X need be considered when ~Y, & v-v.)

In any event, I think your problem can be simplified to:

	1'. A xor B
	2'. A, B are binary variables.


Rob Warnock

UUCP:	{sri-unix,amd70,hpda,harpo,ihnp4,allegra}!fortune!rpw3
DDD:	(415)595-8444
USPS:	Fortune Systems Corp, 101 Twin Dolphins Drive, Redwood City, CA 94065