[net.ai] a trivial reasoning problem?

marcel.uiuc%Rand-Relay@sri-unix.UUCP (12/28/83)

This is an elaboration of why a problem I submitted to the AIList seems
to be unsolvable using regular Horn clause logic, as in Prolog. First I'll
present the problem (of my own devising), then my comments, for your critique.

        Suppose you are shown two lamps, 'a' and 'b', and you
        are told that, at any time,

                1. at least one of 'a' or 'b' is on.
                2. whenever 'a' is on, 'b' is off.
                3. each lamp is either on or off.

        WITHOUT using an exhaustive generate-and-test strategy,
        enumerate the possible on-off configurations of the two
        lamps.

If it were not for the exclusion of dumb-search-and-filter solutions, this
problem would be trivial. The exclusion has left me baffled, even though
the problem seems so logical. Check me on my thinking about why it's so
difficult.

1. The first constraint (one or both lamps on) is not regular Horn clause
   logic. I would like to be able to state (as a fact) that

        on(a) OR on(b)

   but since regular Horn clauses are restricted to at most one positive
   literal I have to recode this. I cannot assert two independent facts
   'on(a)', 'on(b)' since this suggests that 'a' and 'b' are always both
   on. I can however express it in regular Horn clause form:

        not on(b) IMPLIES on(a)
        not on(a) IMPLIES on(b)

   As it happens, both of these are logically equivalent to the original
   disjunction. So let's write them as Prolog:

        on(a) :- not on(b).
        on(b) :- not on(a).

   First, this is not what the disjunction meant. These rules say that 'a'
   is provably on only when 'b' is not provably on, and vice versa, when in
   fact 'a' could be on no matter what 'b' is.

   Second, a question   ?- on(X).  will result in an endless loop.

   Third, 'a' is not known to be on except when 'b' is not known to be on
   (which is not the same as when 'b' is known to be off). This sounds as
   if the closed-world assumption might let us get away with not being able
   to prove anything (if we can't prove something we can always assume its
   negation). Not so. We do not know ANYTHING about whether 'a' or 'b' are
   on OR off; we only know about constraints RELATING their states. Hence
   we cannot even describe their possible states, since that would require
   filling in (by speculative hypothesis) the states of the lamps.

   What is wanted is a non-regular Horn clause, but some of the nice
   properties of Logic Programming (eg completeness and consistency under the
   closed-world assumption, alias a reasonable negation operator) do not apply
   to non-regular Horn clauses.

2. The second constraint (whenever 'a' is on, 'b' is off) shares some of the
   above problems, and a new one. We want to say

        on(a) IMPLIES not on(b),   or    not on(b) :- on(a).

   but this is not possible in Prolog; we have to say it in what I feel to
   be a rather contrived manner, namely

        on(b) :- on(a), !, fail.

   Unfortunately this makes no sense at all to a theoretician. It is trying
   to introduce negative information, but under the closed-world assumption,
   saying that something is NOT true is just the same as not saying it at all,
   so the clause is meaningless.

   Alternative: define a new predicate off(X) which is complementary to on(X).
   That is the conceptualization suggested by the third problem constraint.

3.      off(X) :- not on(X).
        on(X)  :- not off(X).

   This idea has all the problems of the first constraint, including the
   creation of another endless loop.

It seems this problem is beyond the capabilities of present-day logic
programming. Please let me know if you can find a solution, or if you think
my analysis of the difficulties is inaccurate.

                                        Marcel Schoppers
                                        U of Illinois at Urbana-Champaign
                                        {pur-ee|ihnp4}!uiucdcs!marcel

marcel@uiucdcs.UUCP (marcel ) (12/28/83)

#N:uiucdcs:32300014:000:919
uiucdcs!marcel    Dec 27 16:23:00 1983

Here's a problem I'd like some comments on. As far as I know this problem is
not solvable using regular Horn clause logic (see my note on net.lang.prolog).
If you have an inference engine capable of solving it, please tell me about
it; otherwise, please let me know why its difficult. The problem is of my own
devising.

	Suppose you are shown two lamps, 'a' and 'b', and you
	are told that, at any time,

		1. at least one of 'a' or 'b' is on.
		2. whenever 'a' is on, 'b' is off.
		3. each lamp is either on or off.
	
	WITHOUT using an exhaustive generate-and-test strategy,
	enumerate the possible on-off configurations of the two
	lamps.

If it were not for the exclusion of dumb-search-and-filter solutions, this
problem would be trivial. The exclusion has left me baffled, even though
the problem seems so logical.

					Marcel Schoppers
					U of Illinois at Urbana-Champaign
					{pur-ee|ihnp4}!uiucdcs!marcel

rpw3@fortune.UUCP (01/01/84)

#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