|
|
DisProof By COUNTER-EXAMPLE in Prolog!
Posted:
Feb 24, 2013 8:01 PM
|
|
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
|
|
