Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math

Topic: 6 QUANTIFIER ELIMINATION METHODS!
Replies: 1   Last Post: May 11, 2013 9:11 PM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Graham Cooper

Posts: 4,348
Registered: 5/20/10
6 QUANTIFIER ELIMINATION METHODS!
Posted: May 11, 2013 8:04 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

6 QUANTIFIER ELIMINATION METHODS!

ForAll(x) is like the 80s GOTO!

Every formula with A(X) in it requires
every case of X to be considered.

A(X) A(Y) ....
has a O(n^2) Law in complexity

and A(X):N means you need to show some
property holds for Infinitely many values!

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

By Structuring the LOGIC statements, A(X)
can be eliminated once and For All!

.
.
.

1 ******************************

SKOLEM FUNCTIONS

if such and such EXISTS
some algorithm does it!

A(n) E(b) b>n

Replace b with a function

A(n) b()>n

b depends on n

b(n) > n

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

b is only PARTIALLY DEFINED

b = n+1
OR
b = n+2
OR
b = 2*n
OR
....

Since n+1>n is TRUE
A(n) E(b) b>n is TRUE

Skolemization is a popular automated theorem prover
method, but it requires extensive manipulation
of the formula, e.g. removing NOT() and putting into
PRENEX FORM - with all the quantifiers on the left.

.
.
.

2 ******************************

HORN CLAUSE FORM

AXIOM:
p1( p11, p12, ...)

INFERENCE RULE:
p2( p21, p22, ...) ^ p3( p31, p32, ...) ^ ... ^ pn( pn1, pn2, ...)
->
p1( p11, p12, .. )

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

E.G.
VERTICAL (POINT (X,Y) , POINT(X,Z) )

Use Backward Chaining!

Instead of calculating the transitive closure over inference
of ALL theorems:

AXIOMS --->InferenceRules---> THEOREMS
^__________________/

Just use MODUS PONENS in reverse to check
1 formula at a time whether it is a theorem.

R, IF L->R AND L


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

SUBSET AXIOM

ALL(S1) ALL(S2)
S1 C S2
<->
ALL(X) XeS1 -> XeS2

There is no need to check ALL SUBSETS in existence here!

The Axiom APPLIES to all subsets
but each result is independent.

Only 1 ALL(X) is needed to do Backward Chaining.

S1 C S2
<->
ALL(X) XeS1 -> XeS2

S1 and S2 will be bound to the Query Arguments.

.
.
.

3 ************************************

NEGATIVE QUANTIFIERS

To prove NOT(ALL( such and such ))
find one counterexample exists that
EXIST(NOT( such and such ))

~A(x) p(x) <-> E(x) ~p(x)

~A(x) x MOD 2 = 0

--->

E(x) x MOD 2 =/= 0

.
.
.

4 ************************************


SUBSETS

{ x | ..... }

AND

ALL(x) .....

both mean
ALL X SUCH THAT .....

-----------

A(n):N ISEVEN(n)

--->

N C E

-----------

For 2 outermost ALLS you'll need a set
of ordered pairs of all possible combinations
of the 2 ALL VARS.


A(X) A(Y) ....p(X,Y)....

---->

{ (X,Y) | domain(X,Y) }
C
{ (X,Y) | property(X,Y) }

.
.
.
.

5 ************************************

FINITE EXTENSION

A(m):MAMMALS FUR(mammal)

--->

FUR(dog) ^ FUR(cat) ^ .... ^ FUR(lion)

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


In PROLOG I will be adding FINITE ALL (@)
to the Language.

ss(S1, S2)
<- e( @A , S1 ) ^ e( A , S2 )

PROLOG currently handles ALL(X) in reverse
using NEGATION AS FAILURE. i.e. it tests
every value and instead of returning false
a NAF statement captures the failed query.

It should be simple just to put an AND(...)
on all the branches where @VAR is used.

i.e. ALL elements of S1 must also be an element of S2.

.
.
.

6 ***********************************

INDUCTION

A(X) : P(X)

--->

P(0) ^ A(N) P(N) -> P(S(N))



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

Take ZFC AXIOM OF INFINITY

E(N) 0eN ^ XeN->s(X)eN

In PROLOG this is

nat(0)
nat(s(X)) <- nat(X)

e(A, nats) <- nat(A)

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

By Inspecting the Defn of an Infinite Set,
and structuring the definitions then the
inductive step:

p(N) -> p(S(N))

can be used in calculations such as:

eq( NATS , EVENS U ODDS ) ?

Currently this is very hard to solve.

1/ The Infinite Set Definitions are unstructured.

2/ Induction type proofs take some lateral thinking
to find the inductive step.

e.g.
BASE STEP

0 e NATS <-> (0 e EVENS) or (0 e ODDS)

INDUCTIVE STEP

n e NATS <-> (n e EVENS) or (n e ODDS)
->
n+1 e NATS <-> (n+1 e EVENS) or (n+1 e ODDS)

CASE 1:

(n e EVENS)
->
(n+1 e ODDS)

CASE 2:

(n e ODDS)
->
(n+1 e EVENS)


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

That is a LOT OF ABSTRACT DEDUCTION taking place
to test the equality of 2 infinite sets.

eq( NATS, EVENS U ODDS) ?

DCProof has made some progress with a setwise-approach
to Inductive Proofs.

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

Herc
--
www.BLoCKPROLOG.com






Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.