Date: Feb 24, 2013 8:01 PM
Author: Graham Cooper
Subject: DisProof By COUNTER-EXAMPLE in Prolog!

Prolog is good at searching for a solution, or SEVERAL solutions one
at a time..

but ALL(records)  uses a higher SET LEVEL of LOGIC!

But using the EQUIVALENCE of

~ALL(X) p(X)   <->  EXIST(X) ~p(X)

Prolog can do some rudimentary ALL Quantifier negation, by finding a
counter example!

PROLOG - "NO!  NOT ALL!"
- - - - - - - - - - - - - - - - - - - -

First we need to REWORD ALL(X) into an ATOMIC PREDICATE.

{ X | p(X) }   stands for ALL(X) too!  So we can use the predicate
SUBSET!

------------------------

EX 1 - ARE ALL COOKS WOMEN?
40
woman(mary, blond, 25)
woman(jill, redhead, 33)
woman(betty, brunet, 30)

cook( mary, rice )
cook( mary, pizza )
cook( jill , rice )
cook( tom, burgers )

man(tom, 40, football, dog)
man(tim, 30, cricket, cat)

Are ALL Cooks WOMEN?

Next we DEFINE THE SETS women, cooks, men

e( A , women ) <- woman( A , X, Y)
e( A , cooks ) <- cook( X, A )
e( A , men ) <- men( A , X , Y , Z)

This is where we specify which parameter of the predicate
is Quantified over for Sets!

e.g. another set pets could be defined on the same predicate man.

e(A, pets) <- men( X, Y, Z, A)

X, Y, Z will match anything!  Don't Care!

Now we REWORD the QUANTIFIED EXPRESSION into a SUBSET!

ALL COOKS ARE WOMEN!
ALL members of COOKS are WOMEN!
ALL members of COOKS are members of WOMEN

COOKS C WOMEN

To Disprove this we'll need a counterexample to WOMEN who is a Cook!

intersect( cooks, not(women) )
intersect( cooks, men )

COUNTEREXAMPLE = tom


----------------------------------------

EX 2:  ALL NUMBERS ARE EVEN!

All members of NATS are EVEN
All members of NATS are members of EVENS

NATS C EVENS


*
*** DEFINE Nat Numbers

nat(0).
nat(s(X)) :- nat(X).


*
*** DEFINE Even Numbers

even(0).
even(s(s(X))) :- even(X).

*
** DEFINE Odd Numbers

odd(s(0)).
odd(s(s(X))) :- odd(X).


*
** DEFINE SETS  nats, odds, evens

e(A,nats) :- nat(A).
e(A,evens) :- even(A).
e(A,odds) :- odd(A).


*
**  DEFINE Counter Example Sets

e(A, not(evens)) :- e(A, odds).
e(A, not(odds)) :- e(A, evens).


*
** DEFINE Set Intersection

insets(S1,S2) :- e(A,S1),e(A,S2).

*
** Define Negative ALL

not(ss( S1 , S2 )) :- insets( S1, not(S2) ).


**********************************

That's it!

Now Prolog can Prove that not all numbers are even!

?- not(ss(nats,evens))
YES


You'll need a Program Trace to see the counterexample value = s(0)

Herc
--
www.BLoCKROLOG.com