🚀 go-pugleaf

On Jun 12, 9:12 pm, Jan Burse <janbu...@fastmail.fm> wrote:
> Alan Smaill schrieb:
>
> > Not in general, the way you go about it.
>
> > What happens in the example you were just asked about?
> > (rather than in the ones you have already worked out, where
> > the set of positive solutions is finite).
>
> Comprehension also doesn't work when the intended
> set is finite and when negative information
> is lacking.
>
> Compare:
>
>         p(1).                      /* I */
>
> With:
>
>         forall X (p'(X) <-> X=1).  /* II */
>
> They are two different kettle of fish. And we are
> here touching the very basics of FOL. Namely that
> an primeformula:
>
>      p(t)
>
> Only makes a statement about what should be in
> an interpretation, and doesn't make a statement
> for what is not in the interpretation. To say
> that something is not in the interpretation we
> would need the negation of a primeformula:
>
>     ~p(t)
>
> The above makes a statement about what should not
> be in an interpretation, but similarly it doesn't
> make a statement about what is in the interpretation.
>
> The p' definition can actually be expanded into:
>
>        forall X ((p'(X) <- X=1) & (p'(X) -> X = 1))
>
> Which can expanded into:
>
>        forall X (p'(1) & (~p'(X) <- X != 1))
>
> So it is a positive and a negative statememt. The
> positive statement is:
>
>        p'(1).                       /* IIa */
>
> The negative statement is:
>
>        forall X (~p'(X) <- X != 1). /* IIb */
>
> Whereby what we are saying about p is only a positive
> statement, namely:
>
>        p(1).                        /* I */
>
> As a result, assuming the domain is natural numbers,
> we cannot deduce the following:
>
>     T |- ~(2 in { x in nat | p(x) })
>
> Proof: There is a model where p(2). Simply take
> M[p] = {1,2}. This model satisifies the formula p(1).
>
> But we can deduce the following:
>
>     T |- ~(2 in { x in nat | p'(x) })
>
> Proof: The only model that satisfies p' is
> M[p'] = {1}.
>
> So when Prolog does the following:
>
>     p(1).
>
>     ?- setof(X,p(X),L).
>     L = [1]
>
> Then this is quite an illusion that the above is
> based on Horn clauses solely.
>
> Bye
>

You don't seem to be listening.

[1]

~tail <- ~head

directly follows from

head <- tail

============


[2]

Contrapositive Modus Ponens captures this information from [1]

theorem ( ~(X) ) :-
  rule( X , Y )
  theorem ( ~(Y) ).

It's closer to Proof by Contradiction than Modus Ponens

IF X->Y
AND ~Y

then X must be wrong!

============

I agree TUPLE-AT-A-TIME HORN CLAUSES

cannot do negative logic

because it cannot do SUBSET

or set theory, or membership of distinct classes

===========

I am using BREADTH WIDTH UNIFY!

 *ALL* matching clauses must return TRUE!
NO I DON"T WANT TO HEAR WHAT LOGIC THEORY THIS VIOLATES and what it
can't do...  It can't do this and it can't do that because it's never
been programmed before!!

I am using:

SET-AT-A-TIME HORN CLAUSES

more powerful than YOUR PROLOG

There are 2 Horn Styles.   Tuple A.A.T. and Set A.A.T.

In MY PROLOG I can do this:

subset S1 S2  :-
   e(all_X , S1)
   e(X,S2)

You haven't got this far!

You haven't even ATTEMPTED Set Specification in Prolog!


===================

N.S.T.

e( X , set )   <->   p(X)

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

Z.F.C

e(X , set )    ->  p(X)

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

PROLOG Set Theory

e(X , set )   <-   p(X)



==================


Since you are all 20 years of technology behind me I will come back in
20 years after my Fishing Expedition!


Thank you and Good Night!


Herc

--

http://phpPROLOG.com
A.I. Software / Database on the Web!


         DATABASE                    QUERY
    id      ref     term           ref     term
   ----------------------        ----------------
    6       1       test1
    6       2       aaa
    7       1       test1   <=>    1       test1
    7       2       bbb     <=>    2       bbb
   ----------------------        ----------------

               GOAL-AT-A-TIME UNIFY