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.independent

Topic: Set Theorists use EXTENSIONALITY ..... Logic Programmers UNIFY!
Replies: 4   Last Post: Jun 12, 2013 6:25 AM

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,246
Registered: 5/20/10
Re: Set Theorists use EXTENSIONALITY ..... Logic Programmers UNIFY!
Posted: Jun 11, 2013 4:21 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Jun 11, 7:42 pm, Jan Burse <janbu...@fastmail.fm> wrote:
> Graham Cooper schrieb:
>

> > This is not a logical problem in any discipline and is trivially
> > solved with categorical negation with set specification.

>
> But then your "categorical negation with set specification"
> is not anymore the following set of Horn Clauses as a
> starting point theory T:
>



Horn Clauses are a single value logic - 1 truth value.

TRUE (in this system)

or not found (not supported in this system)





>
>         nat(n).
>         forall X (nat(s(X)) <- nat(X)).
>
> You then start with another theory T', which must be
> not equivalent to T, since everything which is equivalent
> to T doesn't work, since we have:
>
>          T |/- ~nat(dog).
>
> But we want:
>
>          T' |- ~nat(dog)
>



How do you know T |- ~nat(dog) Jan?

What Inferences is your own mind using?

Does:

JAN |- ~nat(dog)

Why?



>  > Clarks Completeness is Totally Irresponsible NON-LOGIC
>
> What is the difference between catnegsetspec(T) (your T')
> and comp(T) (the T' of Clark). Which one is simpler and
> solves the dog problem and explains Prolog?


It's a gross oversimplification and missed freebie!

Like BAGOF!

Here is SQL

SELECT NAME, SNAME, TOWN from CLIENTS where TOWN='LA'

RESULT
------------
NAME | SNAME | TOWN
------------------------------------
tom smith LA
tim brady LA
mick brady LA



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

Here is PROLOG - a more powerful relational language than SQL

?- clients( NAME , SNAME , AGE , COMPANY , STREET , la ).

RESULT
------------
NAME = tom
SNAME = smith


< CLICK FOR NEXT RESULT >


Wait! You can PIPE ALL RESULTS into a LIST!

bagof( client( NAME ....

==>

display( [ row1 | rest ] , .... )

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

Prolog calculates SETS of results... and the U/I doesn't!


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

Clark's Completion is RUBBISH!

How do you get NOT(X)

given X->Y


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

USE

X <-> Y instead! WOT ROT!





>
> I don't think your catnegsetspec() explains negation as
> failure in Prolog. Its something different, based on
> defining domains etc..
>
> Bye



**** unsnip *****
The mechanize the above, one has to first drop
the idea of simply defined predicates by Horn
clauses, and then maybe look for new inference
rules.


You can't!

HORN CLAUSES *ARE* INFERENCE RULES.

HORN CLAUSE + NEW_INFERENCE RULE = HORN CLAUSE


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

Here is how LOGIC THEORY WORKS.

AXIOM
predicate( arg1 , arg2 , arg 3 ).

INFERENCE RULE

left ( arg1 , arg2 , arg3 ) -> right ( arg1 , arg2 , arg 3 )

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

MODUS PONENS:

left ^ left->right -> right


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

You need 2 algorithms to make it work.

Pattern Matching 1 formula to another

UNIFY( p1 , p2 ) ==> common-p


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

All inferencing systems above propositional level require unify
algorithm.

Applying modus ponens (backward chaining) *IS* Tail recursion

the 2nd component of UNIFY( query , ALL(heads):database )


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

You CANT invent anything more powerful than modus ponens,
MP is the heart of inference chaining.

Unless you can come up with SOME tangible facet of a demonstrable
weakness (via lack of negation logic) then i'll assume

Contrapositive Modus Ponens allows full logical negation on the horn
clause platform.



Herc


--


prv [ ! L ] [ z Z ] :-
if L R
prv [ ! R ] Z

CMP
if L implies R (and ~R)
then L is false




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.