Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.



6 QUANTIFIER ELIMINATION METHODS!
Posted:
May 11, 2013 8:04 PM


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 setwiseapproach to Inductive Proofs.

Herc  www.BLoCKPROLOG.com



