Search All of the Math Forum:

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

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

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

 Messages: [ Previous | Next ]
 Graham Cooper Posts: 4,495 Registered: 5/20/10
Re: Set Theorists use EXTENSIONALITY ..... Logic Programmers UNIFY!
Posted: Jun 11, 2013 4:21 PM

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)

>
>         nat(n).
>         forall X (nat(s(X)) <- nat(X)).
>
> 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

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

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

Date Subject Author
6/11/13 Graham Cooper
6/12/13 David Bernier
6/11/13 Graham Cooper