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



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)
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 NONLOGIC > > 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 ) ==> commonp

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



