Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Re: ALL(F):N->R is 2OL! NOT 1OL!!!!!!
23 views
Skip to first unread message
Graham Cooper
Nov 14, 2012, 11:43:54 PM11/14/12
to
> > > > > > CANTOR'S THEOREM
>
> > > > > > ALL(F):N->R E(r):r ALL(n):N F(n)=/=r
>
> > > > > I'm not trying to trim to aviod anything other than the brokeness
>
> > > > > of the google groups.
>
> > > > > I'm trying to understand what you wrote. It seems like you
>
> > > > > keep changing your symbolic language.
>
> > > > > Please verify: For all functions of a natural returning a real
>
> > > > > there exist a real such that for all natural numbers the function
>
> > > > > will not return that real.
F is just a LIST!
f(1) = 0.322323...
LIST ITEM 1 = REAL#1 = 0.322323...
>
> > > > > I believe that was his conclusion.
>
> > > > > I don't know how to write in that language yet. Does this make
>
> > > > > sense:
>
> > > > > EXISTS(G):F(N),N->R ALL(F):N->R ALL(m):N ALL(n):N F(n)=/=SUM(G(F(m),m))
>
> > > > G is just NXR->R
>
I'm just saying your TYPE of G is not well formulated.
If you are summing the digit positions into d1/10 + d2/100 + d3/1000
+ ....
that's fine!
If you want to put ALL FUNCTION at the start you are talking about a
bona-fide function here not my countable LIST:N->R of domain N.
>
> > > > (string-of-digits wise function)
>
> > > > or
>
> > > > {0..9}->{0..9)
>
> > > > (digit wise function)
>
> > > I'm not sure I understand.
>
> > > G takes then nth value of F and returns a real between
>
> > > .1^n and .1^(n+1) that differs from MOD(FLOOR(F(n),.1^(n+1)),.1^n)
>
> > > in a way where it will never be 9*(.1^(n+1)).
>
> > OK but you and George and all logicians are making the same mistake.
>
> I'm a computer programmer/systems analyst. I was deeply depressed when
> I took my symbolic logic classes so don't remember them very well. I'm
>
Lot's of students don't remember lectures very well for various
reasons! ;-)
>
> trying to relearn them as fast as I can. It's hard to do so given the
> diverse symbolic systems being used here and very bad assertions about
> the truth of the matter.
>
> Constructivist,http://en.wikipedia.org/wiki/Constructivism_(mathematics)
> make it very hard to talk about infinite sets. I never let my mathmatics
> be limited by the computers I've used and I never will. I do not accept
> there is no number if the system using numbers cannot encode it in native
> mode. Integers weren't limited to 256 just because that's all my 8080
> could handle.
>
> > ALL( FUNCTION ): DOMAIN->RANGE
> > ALL( FUNCTION OF FUNCTIONS ) DXR1 -> R2
> > for FUNCTIONS, i.e. LOGIC FORMULA use "D->R"
> > for SETS, i.e. ordered pairs use "DXR"
>
> Can you point me to a wikipedia page or .edu page
> using the syntax you are describing. I'd like to
>
Not really I am posting this to GG aswell as part of a high level
argument of misusing SETS for FUNCTIONS and calling 2OL 1OL.
>
> come up to speed as quickly as possible. I'm not
> sure I agree to these relative to what I intend to
> write. I take D to reference "domain". Do you take
> it as a given that an ordered pair includes a natural
> number as one of the items paired. where DXR would
> reference an ordered pair (N,R)? Would you use DXN
> if the pairing was (N,N)?
>
> > then you can safely make claims about super-infinite sets in FIRST
> > ORDER LOGIC about
>
> > SETS:DXR
>
> > without stuffing up the
> > FUNCTION:D->R
> > specs for us programmers.
>
> I keep reading what you write about microProlog and wff.
> I still disagree with your formulation since the compiler
> necessarily doesn't allow anything but wff into the system in
> the first place.
>
> What does:
>
> ?wff(this(
>
> return? Does it return no?
>
You seem to be referring to another of my meta-argument.
---8<----------
There was only one problem... PROLOG was a single logic value
language, 1 RECORD FOUND using backward chaining and the Theorem
Provers of the time were Resolution Based 2 valued logic where
Theorems were TRUE and Assumptions were reversed otherwise! Set
Theory adopted a construction system of Predicates, true or false,
as
long as they were well formed, functions were formulas, no sets, more
than infinity of them at any rate, don't try listing a function now-
a-
days... axioms were replaced as the theorem provider with |= missing
theorems from somewhere else, and every thing started with first
order
logic!
f(0).
t(1).
t(X) :- f(f(X)).
wff(X) :- t(X).
wff(X) :- f(X).
what(X,true) :- t(X).
what(X,false) :- f(X).
t(if(X,Y)) :- t(X), t(Y).
t(if(X,Y)) :- f(X), f(Y).
t(if(X,Y)) :- f(X), t(Y).
t(or(X,Y)) :- t(X).
t(or(X,Y)) :- t(Y).
t(and(X,Y)) :- t(X),t(Y).
t(iff(X,Y)) :- t(X),t(Y).
t(iff(X,Y)) :- f(X),f(Y).
t(xor(X,Y)) :- t(X),f(Y).
t(xor(X,Y)) :- f(X),t(Y).
f(if(X,Y)) :- t(X),f(Y).
f(or(X,Y)) :- f(X),f(Y).
f(and(X,Y)) :- f(X).
f(and(X,Y)) :- f(Y).
f(iff(X,Y)) :- t(X),f(Y).
f(iff(X,Y)) :- f(X),t(Y).
f(xor(X,Y)) :- t(X),t(Y).
f(xor(X,Y)) :- f(X),f(Y).
RESOLUTION
or(R,Q) :- if(L,R), or(L,Q).
or(R,Q) :- if(L,R), or(Q,L).
or(Q,R) :- if(L,R), or(L,Q).
or(Q,R) :- if(L,R), or(Q,L).
MODUS PONENS
t(R) :- if(L,R), t(L).
t(R) :- or(f(L),R), t(L).
t(R) :- or(R,f(L)), t(L).
INFERENCE RULE
if( if(t(S),f(R)) , if(t(R),f(S)) ).
if it's sunny then it's not raining
ergo
if it's raining then it's not sunny
--------8<------
This is PROLOG PROGRAMMING.
I am taking a *different approach*.
Rather than CONSTRUCTING ANY WFF that is TRUE OR FALSE.
I work out which is true and which is false by the very construction.
So I have WFFT and WFFF.
That way I can do LOGIC in PROLOG. Actual LOGIC! And Backtrack from
Normal Clauses to Horn Clauses, theorem proving capability PLUS axiom
back tracking derivation capability in the 1 system. Normal Clauses
OVER Horn Clauses. This is just MY Method but it looks like it would
have general Utility.
Herc
>
> > > > > > ALL(F):N->R E(r):r ALL(n):N F(n)=/=r
>
> > > > > I'm not trying to trim to aviod anything other than the brokeness
>
> > > > > of the google groups.
>
> > > > > I'm trying to understand what you wrote. It seems like you
>
> > > > > keep changing your symbolic language.
>
> > > > > Please verify: For all functions of a natural returning a real
>
> > > > > there exist a real such that for all natural numbers the function
>
> > > > > will not return that real.
F is just a LIST!
f(1) = 0.322323...
LIST ITEM 1 = REAL#1 = 0.322323...
>
> > > > > I believe that was his conclusion.
>
> > > > > I don't know how to write in that language yet. Does this make
>
> > > > > sense:
>
> > > > > EXISTS(G):F(N),N->R ALL(F):N->R ALL(m):N ALL(n):N F(n)=/=SUM(G(F(m),m))
>
> > > > G is just NXR->R
>
I'm just saying your TYPE of G is not well formulated.
If you are summing the digit positions into d1/10 + d2/100 + d3/1000
+ ....
that's fine!
If you want to put ALL FUNCTION at the start you are talking about a
bona-fide function here not my countable LIST:N->R of domain N.
>
> > > > (string-of-digits wise function)
>
> > > > or
>
> > > > {0..9}->{0..9)
>
> > > > (digit wise function)
>
> > > I'm not sure I understand.
>
> > > G takes then nth value of F and returns a real between
>
> > > .1^n and .1^(n+1) that differs from MOD(FLOOR(F(n),.1^(n+1)),.1^n)
>
> > > in a way where it will never be 9*(.1^(n+1)).
>
> > OK but you and George and all logicians are making the same mistake.
>
> I'm a computer programmer/systems analyst. I was deeply depressed when
> I took my symbolic logic classes so don't remember them very well. I'm
>
Lot's of students don't remember lectures very well for various
reasons! ;-)
>
> trying to relearn them as fast as I can. It's hard to do so given the
> diverse symbolic systems being used here and very bad assertions about
> the truth of the matter.
>
> Constructivist,http://en.wikipedia.org/wiki/Constructivism_(mathematics)
> make it very hard to talk about infinite sets. I never let my mathmatics
> be limited by the computers I've used and I never will. I do not accept
> there is no number if the system using numbers cannot encode it in native
> mode. Integers weren't limited to 256 just because that's all my 8080
> could handle.
>
> > ALL( FUNCTION ): DOMAIN->RANGE
> > ALL( FUNCTION OF FUNCTIONS ) DXR1 -> R2
> > for FUNCTIONS, i.e. LOGIC FORMULA use "D->R"
> > for SETS, i.e. ordered pairs use "DXR"
>
> Can you point me to a wikipedia page or .edu page
> using the syntax you are describing. I'd like to
>
Not really I am posting this to GG aswell as part of a high level
argument of misusing SETS for FUNCTIONS and calling 2OL 1OL.
>
> come up to speed as quickly as possible. I'm not
> sure I agree to these relative to what I intend to
> write. I take D to reference "domain". Do you take
> it as a given that an ordered pair includes a natural
> number as one of the items paired. where DXR would
> reference an ordered pair (N,R)? Would you use DXN
> if the pairing was (N,N)?
>
> > then you can safely make claims about super-infinite sets in FIRST
> > ORDER LOGIC about
>
> > SETS:DXR
>
> > without stuffing up the
> > FUNCTION:D->R
> > specs for us programmers.
>
> I keep reading what you write about microProlog and wff.
> I still disagree with your formulation since the compiler
> necessarily doesn't allow anything but wff into the system in
> the first place.
>
> What does:
>
> ?wff(this(
>
> return? Does it return no?
>
You seem to be referring to another of my meta-argument.
---8<----------
There was only one problem... PROLOG was a single logic value
language, 1 RECORD FOUND using backward chaining and the Theorem
Provers of the time were Resolution Based 2 valued logic where
Theorems were TRUE and Assumptions were reversed otherwise! Set
Theory adopted a construction system of Predicates, true or false,
as
long as they were well formed, functions were formulas, no sets, more
than infinity of them at any rate, don't try listing a function now-
a-
days... axioms were replaced as the theorem provider with |= missing
theorems from somewhere else, and every thing started with first
order
logic!
f(0).
t(1).
t(X) :- f(f(X)).
wff(X) :- t(X).
wff(X) :- f(X).
what(X,true) :- t(X).
what(X,false) :- f(X).
t(if(X,Y)) :- t(X), t(Y).
t(if(X,Y)) :- f(X), f(Y).
t(if(X,Y)) :- f(X), t(Y).
t(or(X,Y)) :- t(X).
t(or(X,Y)) :- t(Y).
t(and(X,Y)) :- t(X),t(Y).
t(iff(X,Y)) :- t(X),t(Y).
t(iff(X,Y)) :- f(X),f(Y).
t(xor(X,Y)) :- t(X),f(Y).
t(xor(X,Y)) :- f(X),t(Y).
f(if(X,Y)) :- t(X),f(Y).
f(or(X,Y)) :- f(X),f(Y).
f(and(X,Y)) :- f(X).
f(and(X,Y)) :- f(Y).
f(iff(X,Y)) :- t(X),f(Y).
f(iff(X,Y)) :- f(X),t(Y).
f(xor(X,Y)) :- t(X),t(Y).
f(xor(X,Y)) :- f(X),f(Y).
RESOLUTION
or(R,Q) :- if(L,R), or(L,Q).
or(R,Q) :- if(L,R), or(Q,L).
or(Q,R) :- if(L,R), or(L,Q).
or(Q,R) :- if(L,R), or(Q,L).
MODUS PONENS
t(R) :- if(L,R), t(L).
t(R) :- or(f(L),R), t(L).
t(R) :- or(R,f(L)), t(L).
INFERENCE RULE
if( if(t(S),f(R)) , if(t(R),f(S)) ).
if it's sunny then it's not raining
ergo
if it's raining then it's not sunny
--------8<------
This is PROLOG PROGRAMMING.
I am taking a *different approach*.
Rather than CONSTRUCTING ANY WFF that is TRUE OR FALSE.
I work out which is true and which is false by the very construction.
So I have WFFT and WFFF.
That way I can do LOGIC in PROLOG. Actual LOGIC! And Backtrack from
Normal Clauses to Horn Clauses, theorem proving capability PLUS axiom
back tracking derivation capability in the 1 system. Normal Clauses
OVER Horn Clauses. This is just MY Method but it looks like it would
have general Utility.
Herc
Hercules ofZeus
Nov 15, 2012, 1:44:42 AM11/15/12
to
On Nov 15, 4:24 pm, forbisga...@gmail.com wrote:
> ALL(A)[(EXISTS(w)(weA) AND EXISTS(x) ALL(w)(weA->w<=z))->
> EXISTS(x) ALL(y)([All(w)(weA->w<=y)]<->x<=y)]
>
> where <= is being used as "less than or equal to".
> I'm leaving the brackets in place because it appears
> some use it as a transform from true to 1 and false to 0.
> I dont get it in this context. It seems to mix some
> programming languages' coding for the comparison operators
> with their logical value.
>
Most people here use A(x) E(x) or Ax Ex
I *emphasised* ALL(F):
merely to imply the reading "ALL FUNCTIONS", since that was my point
about 2OL.
<= is definable using Peano Arithmetic
A(n) 0 <= n
A(m) A(n) s(m)<=s(n) -> m<=n
e.g.
s(0) <= s(s((0)) ?
m=0 n=s(0)
s(m)<=s(n) -> m<=n 2nd Axiom
0 <= s(0) 1st Axiom
Herc
> ALL(A)[(EXISTS(w)(weA) AND EXISTS(x) ALL(w)(weA->w<=z))->
> EXISTS(x) ALL(y)([All(w)(weA->w<=y)]<->x<=y)]
>
> where <= is being used as "less than or equal to".
> I'm leaving the brackets in place because it appears
> some use it as a transform from true to 1 and false to 0.
> I dont get it in this context. It seems to mix some
> programming languages' coding for the comparison operators
> with their logical value.
>
Most people here use A(x) E(x) or Ax Ex
I *emphasised* ALL(F):
merely to imply the reading "ALL FUNCTIONS", since that was my point
about 2OL.
<= is definable using Peano Arithmetic
A(n) 0 <= n
A(m) A(n) s(m)<=s(n) -> m<=n
e.g.
s(0) <= s(s((0)) ?
m=0 n=s(0)
s(m)<=s(n) -> m<=n 2nd Axiom
0 <= s(0) 1st Axiom
Herc
Graham Cooper
Nov 15, 2012, 2:39:14 AM11/15/12
to
> <= is definable using Peano Arithmetic
>
> A(n) 0 <= n
> A(m) A(n) s(m)<=s(n) -> m<=n
Other way around...
>
> A(n) 0 <= n
> A(m) A(n) s(m)<=s(n) -> m<=n
m<=n -> s(m)<=s(n)
I was thinking of PROLOG
s(m)<=s(n) :- m<n
FORWARD CHAINING
0 <= s(0) FROM AXIOM 1
0<=s(0) -> s(0)<=s(s(0)) FROM AXIOM 2
L & L->R -> R MODUS PONENS
L = 0<=s(0)
R = s(0)<=s(s(0))
==============
s(0)<=s(s(0))
Herc
Graham Cooper
Nov 15, 2012, 3:05:06 AM11/15/12
to
On Nov 15, 5:39 pm, forbisga...@gmail.com wrote:
>
> The bijection has to be done with a well ordered list.
> Cantor produced a well ordered list of reals. What makes
> a list well ordered isn't that the elements are in numeric
> order but that one of the elements is the first item on
> the list and all of the items on the list other than the
> first has a uniquely identified successor based upon their
> position on the list. In reality the position in the list
> alone identifies uniqueness not the element at that position.
> A problem can arise if the elements are not uniquely identified
> because the positional relationship <= (less than or equal to)
> can't be verified, for instance, giving the well ordered list
> {a, b, a, c} one cannot say a<=b without identifying which a
> one is talking about.
> f(1) = 1/3
> etc. is just fine for a function as long as all of the items
> on the list are uniquely associated with a set of natural numbers
> in their defined successor order starting with 0 and all natural
> numbers in the set are uniquely associated with the elements in the
> list. The
>
> ALL(F)N->R
>
> part says for all orderings of lists of reals...
> the pair of a particular function whose domain is a
> set of natural numbers and whose codomain is a set of reals
> and the particular natural number used to produce the particular
> real in the set of reals produced by the function. Details are
> important.
> be created to count them. I want to talk about all such possible
> functions for all orderings of the list. Certainly a countable
> list will have the same members no matter what order it's in.
> A function that finds a real not in the list in one ordering
> must not exist in a different ordering otherwise they wouldn't
> contain the same elements.
the set of all permutations of <1,2,3...> is considered un-countable
itself and isn't usually taken into consideration.
I devised a set of all computable orderings (of all functions).
www.tinyurl.com/BLUEPRINTS-PERM
>
> ...
> well formed by its form not its logical state or lack there of.
> By not using the standard definition your conclusions are off
> and this reduces the utility of your work.
>
I don't use the term WFF as I utilise it in PROLOG.
wff(X) :- t(X).
wff(X) :- f(X).
a formula is WFF is it is either t(...formula...) or f(...formula...)
wff is superfluous in my system.
in Predicate Calculus..
if F is a formula --> NOT(F) is a formula
this is a wasted opportunity definition, by keeping WFF-T separate to
WFF-F it allows you to decompose the truth values of any formula!
>
> I've been trying to relearn prolog as well so I can address some
> of the issues. I've had to move here because google doesn't allow
> cross posts any more and you don't read comp.ai.philosophy even though
> you add a cross post to it.
You can go back to old Google groups from the Options menu.
>
> As it turns out I learned prolog on a (now defunct) Bordland product
> that appears to be somewhat related to Visual Prolog. That version
> of Prolog had string functions. I could parse BNFhttp://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form
> to define a language's syntax then bind elements as needed to lists or
> functions. It was a lot of work and the limitations of my patience
> lead me to move on. Unix programmers have created lots of useful
> scripting languages to aid LALR compiler generation.
>
> http://en.wikipedia.org/wiki/LALR_parser
TRY
www.microPROLOG.com
[LIST]
[vert [pnt 1 2] [pnt 1 4]]?
--------------------
However that's as far as I got!!
I designed a new PROLOG ENGINE = ITERATIVE UNIFY
This wil be my 4th redesign, so give me a couple weeks!
Basically I'm going to parse all the Predicates into a SET of discreet
terms.
vert ( pnt( 1,2 ) pnt( 1,4 ) )
This will be
ID REF FIELD TYP
=================
1 11 vert H
1 12 pnt P
1 13 pnt P
1 121 1 T
1 122 2 T
1 131 1 T
1 132 4 T
Now there is NO RECURSION REQUIRED to unify 2 fomulas!
That is the set of facts when you make a QUERY.
All it has to do is UNIFY all those terms with the PROLOG RULE!
THE PROLOG RULE - Listed at microPROLOG!
vert ( pnt( X,Y ) pnt( X,Z ) )
ID REF FIELD TYP
=================
21 11 vert H
21 12 pnt P
21 13 pnt P
21 121 X V
21 122 Y V
21 131 X V
21 132 Z V
So all the PROLOG ENGINE has to do is check term against term!
Herc
--
--
> On Wednesday, November 14, 2012 8:43:55 PM UTC-8, Graham Cooper wrote:
> > > > > > > > CANTOR'S THEOREM
> > > > > > > > ALL(F):N->R E(r):r ALL(n):N F(n)=/=r
> > > > > > > I'm not trying to trim to aviod anything other than the brokeness
> > > > > > > of the google groups.
> > > > > > > I'm trying to understand what you wrote. It seems like you
> > > > > > > keep changing your symbolic language.
> > > > > > > Please verify: For all functions of a natural returning a real
> > > > > > > there exist a real such that for all natural numbers the function
> > > > > > > will not return that real.
>
> > F is just a LIST!
>
> Cantor deals with a well ordered list.
> > > > > > > > CANTOR'S THEOREM
> > > > > > > > ALL(F):N->R E(r):r ALL(n):N F(n)=/=r
> > > > > > > I'm not trying to trim to aviod anything other than the brokeness
> > > > > > > of the google groups.
> > > > > > > I'm trying to understand what you wrote. It seems like you
> > > > > > > keep changing your symbolic language.
> > > > > > > Please verify: For all functions of a natural returning a real
> > > > > > > there exist a real such that for all natural numbers the function
> > > > > > > will not return that real.
>
> > F is just a LIST!
>
>
> The bijection has to be done with a well ordered list.
> Cantor produced a well ordered list of reals. What makes
> a list well ordered isn't that the elements are in numeric
> order but that one of the elements is the first item on
> the list and all of the items on the list other than the
> first has a uniquely identified successor based upon their
> position on the list. In reality the position in the list
> alone identifies uniqueness not the element at that position.
> A problem can arise if the elements are not uniquely identified
> because the positional relationship <= (less than or equal to)
> can't be verified, for instance, giving the well ordered list
> {a, b, a, c} one cannot say a<=b without identifying which a
> one is talking about.
>
>
> > LIST ITEM 1 = REAL#1 = 0.322323...
>
> f(0) = 0.322323... = 0.32[23]
>
> > LIST ITEM 1 = REAL#1 = 0.322323...
>
> f(1) = 1/3
> etc. is just fine for a function as long as all of the items
> on the list are uniquely associated with a set of natural numbers
> in their defined successor order starting with 0 and all natural
> numbers in the set are uniquely associated with the elements in the
> list. The
>
> ALL(F)N->R
>
> part says for all orderings of lists of reals...
>
> > > > > > > I believe that was his conclusion.
> > > > > > > I don't know how to write in that language yet. Does this make
> > > > > > > sense:
> > > > > > > EXISTS(G):F(N),N->R ALL(F):N->R ALL(m):N ALL(n):N F(n)=/=SUM(G(F(m),m))
> > > > > > G is just NXR->R
>
> > I'm just saying your TYPE of G is not well formulated.
>
> Yes, I get that. I'm trying to restrict the domain of G to
> > > > > > > I believe that was his conclusion.
> > > > > > > I don't know how to write in that language yet. Does this make
> > > > > > > sense:
> > > > > > > EXISTS(G):F(N),N->R ALL(F):N->R ALL(m):N ALL(n):N F(n)=/=SUM(G(F(m),m))
> > > > > > G is just NXR->R
>
> > I'm just saying your TYPE of G is not well formulated.
>
> the pair of a particular function whose domain is a
> set of natural numbers and whose codomain is a set of reals
> and the particular natural number used to produce the particular
> real in the set of reals produced by the function. Details are
> important.
>
> > If you are summing the digit positions into d1/10 + d2/100 + d3/1000
>
> > + ....
>
> > that's fine!
>
> Yes, that's what I'm doing.
> > If you are summing the digit positions into d1/10 + d2/100 + d3/1000
>
> > + ....
>
> > that's fine!
>
>
> > If you want to put ALL FUNCTION at the start you are talking about a
> > bona-fide function here not my countable LIST:N->R of domain N.
>
> By saying the list is countable you are implying a function can
> > If you want to put ALL FUNCTION at the start you are talking about a
> > bona-fide function here not my countable LIST:N->R of domain N.
>
> be created to count them. I want to talk about all such possible
> functions for all orderings of the list. Certainly a countable
> list will have the same members no matter what order it's in.
> A function that finds a real not in the list in one ordering
> must not exist in a different ordering otherwise they wouldn't
> contain the same elements.
the set of all permutations of <1,2,3...> is considered un-countable
itself and isn't usually taken into consideration.
I devised a set of all computable orderings (of all functions).
www.tinyurl.com/BLUEPRINTS-PERM
>
> ...
>
> > That way I can do LOGIC in PROLOG. Actual LOGIC! And Backtrack from
> > Normal Clauses to Horn Clauses, theorem proving capability PLUS axiom
> > back tracking derivation capability in the 1 system. Normal Clauses
> > OVER Horn Clauses. This is just MY Method but it looks like it would
> > have general Utility.
>
> My issue is your use of WFF. It's non-standard. A formula is
> > That way I can do LOGIC in PROLOG. Actual LOGIC! And Backtrack from
> > Normal Clauses to Horn Clauses, theorem proving capability PLUS axiom
> > back tracking derivation capability in the 1 system. Normal Clauses
> > OVER Horn Clauses. This is just MY Method but it looks like it would
> > have general Utility.
>
> well formed by its form not its logical state or lack there of.
> By not using the standard definition your conclusions are off
> and this reduces the utility of your work.
>
I don't use the term WFF as I utilise it in PROLOG.
wff(X) :- t(X).
wff(X) :- f(X).
wff is superfluous in my system.
in Predicate Calculus..
if F is a formula --> NOT(F) is a formula
this is a wasted opportunity definition, by keeping WFF-T separate to
WFF-F it allows you to decompose the truth values of any formula!
>
> I've been trying to relearn prolog as well so I can address some
> of the issues. I've had to move here because google doesn't allow
> cross posts any more and you don't read comp.ai.philosophy even though
> you add a cross post to it.
You can go back to old Google groups from the Options menu.
>
> As it turns out I learned prolog on a (now defunct) Bordland product
> that appears to be somewhat related to Visual Prolog. That version
> of Prolog had string functions. I could parse BNFhttp://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form
> to define a language's syntax then bind elements as needed to lists or
> functions. It was a lot of work and the limitations of my patience
> lead me to move on. Unix programmers have created lots of useful
> scripting languages to aid LALR compiler generation.
>
> http://en.wikipedia.org/wiki/LALR_parser
TRY
www.microPROLOG.com
[LIST]
[vert [pnt 1 2] [pnt 1 4]]?
--------------------
However that's as far as I got!!
I designed a new PROLOG ENGINE = ITERATIVE UNIFY
This wil be my 4th redesign, so give me a couple weeks!
Basically I'm going to parse all the Predicates into a SET of discreet
terms.
vert ( pnt( 1,2 ) pnt( 1,4 ) )
This will be
ID REF FIELD TYP
=================
1 11 vert H
1 12 pnt P
1 13 pnt P
1 121 1 T
1 122 2 T
1 131 1 T
1 132 4 T
Now there is NO RECURSION REQUIRED to unify 2 fomulas!
That is the set of facts when you make a QUERY.
All it has to do is UNIFY all those terms with the PROLOG RULE!
THE PROLOG RULE - Listed at microPROLOG!
vert ( pnt( X,Y ) pnt( X,Z ) )
ID REF FIELD TYP
=================
21 11 vert H
21 12 pnt P
21 13 pnt P
21 121 X V
21 122 Y V
21 131 X V
21 132 Z V
So all the PROLOG ENGINE has to do is check term against term!
Herc
--
--
0 new messages