From: Daniel G. "Govende" McGrath
Subject: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <egnhn1lghp5tpm3oan7ar1o63tt84k1704@4ax.com>
Hello everyone. I keep wanting to become "famous", perhaps by proving
something in advanced mathematics. The reason is that a lot of people
do not understand how severely disabled I can be, even though I am
very smart in some ways, and if I became famous the autism that _I_
have in its precise form could become more widely known than it is
now. By the people that do not understand, I mostly mean the staff at
the residential facility that I have resided at for over 2 years
(because of my disabilities). I try to explain all about it to the
staff, and they're just not convinced.
Thus, to go about "proving" something, I need to basically learn
mathematics over from scratch. I learned calculus around age 9 or 10,
but when I was about 12, I found that I could no longer take anything
"for granted". Now you see--some time ago, one of the staff who work
with me gave me a copy of Irving M. Copi's _Introduction to Logic_
(7th ed.). I found it interesting to be reading a book on logic,
since it seems that all of the notation used in mathematics could
somehow be expressed as logical formulas. (In other words, logic is
the whole basis of mathematics.) Have any of you folks on sci.logic
read Copi's book? I keep looking on page 381, noting how he neatly
created a "vocabulary" that could be used to translate English
proverbs into the symbolic language that he uses for logic.
However, I don't exactly think that his notation is the best choice (I
don't think I can explain why). It would be nicer if this was
expressed as more like a form that one would use on a computer. That
is what I am used to, and I would be more comfortable with
that--specifically, something related to the LISP programming language
(hence the crossposting) would be good. I am quite knowledgeable
about LISP, and given the nature of the programming language it would
seem that logical statements could be represented easily by most
people. Just not by me--what I need to do first is rewrite Copi's
symbolic notation in the form of LISP lists, or some such thing.
Maybe someone can help me with that.
- Daniel al-Autistiqui
--
Daniel Gerard McGrath: a/k/a "Govende"
I have the developmental disability Autism.
To e-mail me, remove the six upper-case letters at
the beginning of my address.
[This signature is under construction.]
Daniel G. "Govende" McGrath wrote:
> However, I don't exactly think that his notation is the best choice (I
> don't think I can explain why). It would be nicer if this was
> expressed as more like a form that one would use on a computer. That
> is what I am used to, and I would be more comfortable with
> that--specifically, something related to the LISP programming language
> (hence the crossposting) would be good. I am quite knowledgeable
> about LISP, and given the nature of the programming language it would
> seem that logical statements could be represented easily by most
> people. Just not by me--what I need to do first is rewrite Copi's
> symbolic notation in the form of LISP lists, or some such thing.
> Maybe someone can help me with that.
You should take a look at KIF, the Knowledge Interchange Format. It is
a lisp-like prefix notation for first order predicate calculus.
The link to check out is
http://www-ksl.stanford.edu/knowledge-sharing/kif/
and a good published summary reference is
M. R. Genesereth. Knowledge Interchange Format. Principles of Knowledge
Representation and Reasoning: Proceedings of the Second International
Conference, Cambridge, MA, pages 599-600. Morgan Kaufmann, 1991.
There is also an effort to turn KIF into an ANSI standard.
On 14 Nov 2005 11:57:13 -0800, Tom Russ <···@isi.edu> said:
> You should take a look at KIF, the Knowledge Interchange Format. It is
> a lisp-like prefix notation for first order predicate calculus.
>
> The link to check out is
>
> http://www-ksl.stanford.edu/knowledge-sharing/kif/
>
> and a good published summary reference is
>
> M. R. Genesereth. Knowledge Interchange Format. Principles of Knowledge
> Representation and Reasoning: Proceedings of the Second International
> Conference, Cambridge, MA, pages 599-600. Morgan Kaufmann, 1991.
>
> There is also an effort to turn KIF into an ANSI standard.
That effort has been superseded by the Common Logic project, which is
currently pursuing ISO standardization: http://cl.tamu.edu .
From: Cameron MacKinnon
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <49idnf8Kx-APe-XeRVn-vQ@rogers.com>
Daniel G. "Govende" McGrath wrote:
> However, I don't exactly think that his notation is the best choice (I
> don't think I can explain why). It would be nicer if this was
> expressed as more like a form that one would use on a computer. That
> is what I am used to, and I would be more comfortable with
> that--specifically, something related to the LISP programming language
> (hence the crossposting) would be good. I am quite knowledgeable
> about LISP, and given the nature of the programming language it would
> seem that logical statements could be represented easily by most
> people.
You should check out Douglas Hofstadter's book 'Godel, Escher, Bach: An
Eternal Golden Braid'
Cameron MacKinnon wrote:
> Daniel G. "Govende" McGrath wrote:
>
>> However, I don't exactly think that his notation is the best choice (I
>> don't think I can explain why). It would be nicer if this was
>> expressed as more like a form that one would use on a computer. That
>> is what I am used to, and I would be more comfortable with
>> that--specifically, something related to the LISP programming language
>> (hence the crossposting) would be good. I am quite knowledgeable
>> about LISP, and given the nature of the programming language it would
>> seem that logical statements could be represented easily by most
>> people.
>
>
> You should check out Douglas Hofstadter's book 'Godel, Escher, Bach: An
> Eternal Golden Braid'
And you're in luck, it's just recently been reprinted in a 20th
anniversary edition, so it's easily available.
From: Pascal Bourguignon
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <87iruvj9jl.fsf@thalassa.informatimago.com>
"Daniel G. \"Govende\" McGrath" <···············@hotmail.com> writes:
> However, I don't exactly think that his notation is the best choice (I
> don't think I can explain why). It would be nicer if this was
> expressed as more like a form that one would use on a computer. That
> is what I am used to, and I would be more comfortable with
> that--specifically, something related to the LISP programming language
> (hence the crossposting) would be good. I am quite knowledgeable
> about LISP, and given the nature of the programming language it would
> seem that logical statements could be represented easily by most
> people. Just not by me--what I need to do first is rewrite Copi's
> symbolic notation in the form of LISP lists, or some such thing.
> Maybe someone can help me with that.
A logic is basically a set of formulas, and a set of rules that allow
you to deduce new formulas from given formulas or axioms.
The set of formulas is often described in a constructive way: some
atoms are listed, and rules to build further formulas are given.
This is a language with a grammar. You can easily write a program to
generate words in a language defined by a grammar (formulas), or to
check if a given string is a word of the language (if a string is a
formula).
Then since you have rules to deduce new formulas, you can write a
program to generate automatically new formulas from the given
axiomatic formulas, or, it's generally harder but also feasible, to
find a chain of rules applications to deduce a given formula from
given axiomatic formulas (ie, to demonstrate a theorem).
If his notation is not ambiguous, that is if he is actually using a
properly defined grammar, then we can also write a translator from his
language to another, more to your taste.
There is no difficulty. Just identify the atoms of his language, and
the rules he use to build further formulas.
For example, for the basic Boolean logic, the atoms are:
true, false (logical literals)
p, q, r, ... (logical variables)
and or not ==> <=> (logical connectors)
The atoms are the logical literals union the logical variables.
The rule to make new formulas is:
If x is a formula and y is a formula,
then (not x), (x and y), (x or y), (x ==> y) and (x <=> y) are formulas.
That's all you need to write the basic formulas of the boolean logic.
(x and y or z) is not a formula
((x and y) or z) is a formula
(false ==> true) is a formula
etc...
If you prefer to use a prefix notation like in lisp, you can map the rules to:
If x is a formula and y is a formula,
then (not x), (and x y), (or x y), (==> x y) and (<=> x y) are formulas.
then you can automatically parse an old formula
((x and y) or z)
applying the rule x and y are formulas
--> (x and y) is a formula
with x = x and y = y.
( a or z)
applying the rule x and y are formulas
--> (x or y) is a formula
with x = a and y = z.
b
then construct the new formula, applyting the corresponding rules:
b
applying the rule x and y are formulas
--> (or x y) is a formula
with x = a and y = z.
(or a z)
applying the rule x and y are formulas
--> (and x y) is a formula
with x = x and y = y.
(or (and x y) z)
--
__Pascal Bourguignon__ http://www.informatimago.com/
This is a signature virus. Add me to your signature and help me to live
From: Daniel G. "Govende" McGrath
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <oc6kn1pn20e47mr0ud21m3c2eb3qv00602@4ax.com>
On Mon, 14 Nov 2005 20:47:58 +0100, Pascal Bourguignon
<····@mouse-potato.com> wrote:
>"Daniel G. \"Govende\" McGrath" <···············@hotmail.com> writes:
>> However, I don't exactly think that his notation is the best choice (I
>> don't think I can explain why). It would be nicer if this was
>> expressed as more like a form that one would use on a computer. That
>> is what I am used to, and I would be more comfortable with
>> that--specifically, something related to the LISP programming language
>> (hence the crossposting) would be good. I am quite knowledgeable
>> about LISP, and given the nature of the programming language it would
>> seem that logical statements could be represented easily by most
>> people. Just not by me--what I need to do first is rewrite Copi's
>> symbolic notation in the form of LISP lists, or some such thing.
>> Maybe someone can help me with that.
>
>A logic is basically a set of formulas, and a set of rules that allow
>you to deduce new formulas from given formulas or axioms.
>
>
>The set of formulas is often described in a constructive way: some
>atoms are listed, and rules to build further formulas are given.
>This is a language with a grammar. You can easily write a program to
>generate words in a language defined by a grammar (formulas), or to
>check if a given string is a word of the language (if a string is a
>formula).
>
>Then since you have rules to deduce new formulas, you can write a
>program to generate automatically new formulas from the given
>axiomatic formulas, or, it's generally harder but also feasible, to
>find a chain of rules applications to deduce a given formula from
>given axiomatic formulas (ie, to demonstrate a theorem).
>
>
>If his notation is not ambiguous, that is if he is actually using a
>properly defined grammar, then we can also write a translator from his
>language to another, more to your taste.
>
>There is no difficulty. Just identify the atoms of his language, and
>the rules he use to build further formulas.
>
>For example, for the basic Boolean logic, the atoms are:
>
>true, false (logical literals)
>p, q, r, ... (logical variables)
>and or not ==> <=> (logical connectors)
>
>The atoms are the logical literals union the logical variables.
>The rule to make new formulas is:
> If x is a formula and y is a formula,
> then (not x), (x and y), (x or y), (x ==> y) and (x <=> y) are formulas.
>
>That's all you need to write the basic formulas of the boolean logic.
>
> (x and y or z) is not a formula
> ((x and y) or z) is a formula
> (false ==> true) is a formula
>
>etc...
>
>
>If you prefer to use a prefix notation like in lisp, you can map the rules to:
>
> If x is a formula and y is a formula,
> then (not x), (and x y), (or x y), (==> x y) and (<=> x y) are formulas.
>
>then you can automatically parse an old formula
>
> ((x and y) or z)
> applying the rule x and y are formulas
> --> (x and y) is a formula
> with x = x and y = y.
> ( a or z)
> applying the rule x and y are formulas
> --> (x or y) is a formula
> with x = a and y = z.
> b
>
>then construct the new formula, applyting the corresponding rules:
>
> b
> applying the rule x and y are formulas
> --> (or x y) is a formula
> with x = a and y = z.
> (or a z)
> applying the rule x and y are formulas
> --> (and x y) is a formula
> with x = x and y = y.
> (or (and x y) z)
Hmmm...maybe my problem is mainly just some difficulty in deciding
what kind of a notation I should use, what to name some of the
operations, etc. (I tend to have trouble making choices a lot,
including in real life.)
At least I'm fairly sure, as of right now, that LISP is the
programming language that I want to use as the basis for my system. I
might have settled on my choice of LISP when I was comparing two
editions--I have both first and third--of Winston and Horn's _LISP_ (a
rather well-known book, I believe). The first edition, given to me by
a friend a long, long time ago, has always seemed sort of hard to read
every time I look at it, but of course it dealt with MacLISP so maybe
some aspects of the language were confusing in those days. The newer
edition that covered Common LISP was bought for me later when I saw it
in a bookstore. So I was looking at the MacLISP edition and I noticed
something about "theorem proving" (I think that's what they called it)
in the chapter on pattern matching, including a function called PROVE.
I don't really know if this had so much relation to the kind of logic
that I am trying to get interested in, but it was indeed a logic
system and there must have been some similarities (I saw something
about AND, OR, and NOT).
You see, a PROVE-type-of function seems very interesting to me, and I
always seem to want to figure it out, but parts of it are confusing,
and there are things that don't make sense because I wouldn't have
expected them in a PROVE function! As I said above, maybe any series
of lines of MacLISP code can distract me a little bit. Alas, the part
about theorem proving had apparently gotten removed by the time the
third (Common LISP) edition came out! I thought that maybe my kind of
proving function could possibly get built based on a sort of
pattern-matching mechanism too. But the stuff on theorem proving that
they have in Winston and Horn 1st Ed. doesn't seem to me to be exactly
right.
- Daniel al-Autistiqui
--
Daniel Gerard McGrath: a/k/a "Govende"
I have the developmental disability Autism.
To e-mail me, remove the six upper-case letters at
the beginning of my address.
[This signature is under construction.]
Dan,
I probably haven't got the space for this; but you can have a look at
Qi (www.lambdassociates.org) which was originally invented for work
in theorem-proving. See chapters 14 onwards for how to build ATPs
(automated theorem-provers) with Qi. Also see the study series on
practical uses of ATP technology particularly study #2 on type checking
and study #4 on quantifier machines.
Reading; tons of stuff in the area but 3 classics
a. Chang and Lee on Automatic Theorem Proving
b. Boyer and Moore on Inductive Theorem Proving
c. Milner, Gordon, Wadsworth on Tactics in the LCF
I think the full references are in the online Qi text.
Sorry for not giving ISBNs etc. but its late here & I'm
tired. Qi is better than Lisp for this work but less
mainstream. But Lisp is a fine language in its own
right, so you could do worse.
Mark
From: Daniel G. "Govende" McGrath
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <du49o1dathomg1i43jh39s6gskgtidrqsd@4ax.com>
On Tue, 15 Nov 2005 13:29:45 -0500, "Daniel G. \"Govende\" McGrath"
<···············@hotmail.com> wrote:
>At least I'm fairly sure, as of right now, that LISP is the
>programming language that I want to use as the basis for my system. I
>might have settled on my choice of LISP when I was comparing two
>editions--I have both first and third--of Winston and Horn's _LISP_ (a
>rather well-known book, I believe). The first edition, given to me by
>a friend a long, long time ago, has always seemed sort of hard to read
>every time I look at it, but of course it dealt with MacLISP so maybe
>some aspects of the language were confusing in those days. The newer
>edition that covered Common LISP was bought for me later when I saw it
>in a bookstore. So I was looking at the MacLISP edition and I noticed
>something about "theorem proving" (I think that's what they called it)
>in the chapter on pattern matching, including a function called PROVE.
>I don't really know if this had so much relation to the kind of logic
>that I am trying to get interested in, but it was indeed a logic
>system and there must have been some similarities (I saw something
>about AND, OR, and NOT).
>
>You see, a PROVE-type-of function seems very interesting to me, and I
>always seem to want to figure it out, but parts of it are confusing,
>and there are things that don't make sense because I wouldn't have
>expected them in a PROVE function! As I said above, maybe any series
>of lines of MacLISP code can distract me a little bit. Alas, the part
>about theorem proving had apparently gotten removed by the time the
>third (Common LISP) edition came out! I thought that maybe my kind of
>proving function could possibly get built based on a sort of
>pattern-matching mechanism too. But the stuff on theorem proving that
>they have in Winston and Horn 1st Ed. doesn't seem to me to be exactly
>right.
>
>- Daniel al-Autistiqui
After reading more closely and thoroughly the third edition of Winston
and Horn's book (as opposed to that horrible MacLISP edition), I seem
to have found the part in which they discuss what I need: it's chapter
26 titled "Rule-Based Expert Systems and Forward Chaining". It seems
that their notions of "rules" and "assertions" must really come in
handy. I have come up with a tentative notation system for assertions
that "translates" what Irving Copi uses; it's designed to be used
together with the LISP forward-chaining system in W&H. I have written
down "translations" on paper for each of Copi's proverbs (pgs. 381-2)
for which a solution is given in the back of the book; those are the
"Assertions". I also have a series of "Rules", modeled on the first
nine of Copi's "Rules of Inference" (see pgs. 311-12). I'll now try
posting both the rules and the assertions.
Here are the rules. Note that I have styled them in LISP notation;
the function REMEMBER-RULE is W&H's and adds new rules into the "rule
stream" (the value of global variable *RULES*):
;;; Rules begin here.
(remember-rule '(modus-ponens
(implies (? papa) (? quebec))
(? papa)
(? quebec)))
(remember-rule '(modus-tollens
(implies (? papa) (? quebec))
(not (? quebec))
(not (? papa))))
(remember-rule '(hypothetical-syllogism
(implies (? papa) (? quebec))
(implies (? quebec) (? romeo))
(implies (? papa) (? romeo))))
(remember-rule '(disjunctive-syllogism
(or (? papa) (? quebec))
(not (? papa))
(? quebec)))
(remember-rule '(constructive-dilemma
(and (implies (? papa) (? quebec))
(implies (? romeo) (? sierra)))
(or (? papa) (? romeo))
(or (? quebec) (? sierra))))
(remember-rule '(absorption
(implies (? papa) (? quebec))
(implies (? papa) (and (? papa) (? quebec)))))
(remember-rule '(simplification
(and (? papa) (? quebec))
(? papa)))
(remember-rule '(conjunction
(? papa)
(? quebec)
(and (? papa) (? quebec))))
(remember-rule '(addition
(? papa)
(or (? papa) (? quebec))))
;;; Rules end here.
Now here are the assertions; as noted above, they represent the
logical formulations of the five proverbs for which Copi has supplied
a translation into plain English. In each case I have indicated the
proverb in a comment. REMEMBER-ASSERTION is another function from
W&H's book; it's almost like REMEMBER-RULE but here the global
variable is *ASSERTIONS*, the assertion stream:
;;; Assertions begin here.
;; Every dog has his day.
(remember-assertion
'(alambda (xray)
(implies (funcall *big-delta* xray)
(ilambda (yankee)
(and (funcall *big-yankee* yankee)
(funcall *big-bravo* yankee xray))))))
;; All things come to him who waits.
(remember-assertion
'(alambda (xray)
(implies (and (funcall *big-papa* xray)
(funcall *big-zulu* xray))
(alambda (yankee)
(funcall *big-uniform* yankee xray)))))
;; A person is judged by the company he keeps.
(remember-assertion
'(alambda (xray)
(implies (funcall *big-papa* xray)
(alambda (yankee)
(implies (funcall *big-quebec* xray yankee)
(funcall *big-oscar* yankee xray))))))
;; It's an ill wind that blows nobody any good.
(remember-assertion
'(alambda (xray)
(implies
(and
(funcall *big-whiskey* xray)
(alambda (yankee)
(implies
(funcall *big-papa* yankee)
(not (ilambda (zulu)
(and (funcall *big-november* zulu)
(funcall *big-papa* xray zulu yankee)))))))
(funcall *big-india* xray))))
;; Nobody borrows everything from everybody.
(remember-assertion
'(alambda (xray)
(implies
(funcall *big-papa* xray)
(ilambda (yankee)
(and (funcall *big-papa* yankee)
(ilambda (zulu)
(not (funcall *big-bravo* xray zulu yankee))))))))
;;; Assertions end here.
What do you think of the notation I used above (in place of Copi's
notation) for representing rules and assertions? Am I off to a good
start?
Well, it took me a long time to type all this and now I've got to go.
"HAPPY THANKSGIVING"!!!!
- Daniel al-Autistiqui
--
Daniel Gerard McGrath: a/k/a "Govende"
I have the developmental disability Autism.
To e-mail me, remove the six upper-case letters at
the beginning of my address.
[This signature is under construction.]
From: Daniel G. "Govende" McGrath
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <s0emo1puoh7gqhf7d51k0m60fcv1ppjnkm@4ax.com>
On Tue, 15 Nov 2005 13:29:45 -0500, "Daniel G. \"Govende\" McGrath"
<···············@hotmail.com> wrote:
>At least I'm fairly sure, as of right now, that LISP is the
>programming language that I want to use as the basis for my system. I
>might have settled on my choice of LISP when I was comparing two
>editions--I have both first and third--of Winston and Horn's _LISP_ (a
>rather well-known book, I believe). The first edition, given to me by
>a friend a long, long time ago, has always seemed sort of hard to read
>every time I look at it, but of course it dealt with MacLISP so maybe
>some aspects of the language were confusing in those days. The newer
>edition that covered Common LISP was bought for me later when I saw it
>in a bookstore. So I was looking at the MacLISP edition and I noticed
>something about "theorem proving" (I think that's what they called it)
>in the chapter on pattern matching, including a function called PROVE.
>I don't really know if this had so much relation to the kind of logic
>that I am trying to get interested in, but it was indeed a logic
>system and there must have been some similarities (I saw something
>about AND, OR, and NOT).
>
>You see, a PROVE-type-of function seems very interesting to me, and I
>always seem to want to figure it out, but parts of it are confusing,
>and there are things that don't make sense because I wouldn't have
>expected them in a PROVE function! As I said above, maybe any series
>of lines of MacLISP code can distract me a little bit. Alas, the part
>about theorem proving had apparently gotten removed by the time the
>third (Common LISP) edition came out! I thought that maybe my kind of
>proving function could possibly get built based on a sort of
>pattern-matching mechanism too. But the stuff on theorem proving that
>they have in Winston and Horn 1st Ed. doesn't seem to me to be exactly
>right.
>
>- Daniel al-Autistiqui
After reading more closely and thoroughly the third edition of Winston
and Horn's book (as opposed to that horrible MacLISP edition), I seem
to have found the part in which they discuss what I need: it's chapter
26 titled "Rule-Based Expert Systems and Forward Chaining". It seems
that their notions of "rules" and "assertions" must really come in
handy. I have come up with a tentative notation system for assertions
that "translates" what Irving Copi uses; it's designed to be used
together with the LISP forward-chaining system in W&H. I have written
down "translations" on paper for each of Copi's proverbs (pgs. 381-2)
for which a solution is given in the back of the book; those are the
"Assertions". I also have a series of "Rules", modeled on the first
nine of Copi's "Rules of Inference" (see pgs. 311-12). I'll now try
posting both the rules and the assertions.
Here are the rules. Note that I have styled them in LISP notation;
the function REMEMBER-RULE is W&H's and adds new rules into the "rule
stream" (the value of global variable *RULES*):
;;; Rules begin here.
(remember-rule '(modus-ponens
(implies (? papa) (? quebec))
(? papa)
(? quebec)))
(remember-rule '(modus-tollens
(implies (? papa) (? quebec))
(not (? quebec))
(not (? papa))))
(remember-rule '(hypothetical-syllogism
(implies (? papa) (? quebec))
(implies (? quebec) (? romeo))
(implies (? papa) (? romeo))))
(remember-rule '(disjunctive-syllogism
(or (? papa) (? quebec))
(not (? papa))
(? quebec)))
(remember-rule '(constructive-dilemma
(and (implies (? papa) (? quebec))
(implies (? romeo) (? sierra)))
(or (? papa) (? romeo))
(or (? quebec) (? sierra))))
(remember-rule '(absorption
(implies (? papa) (? quebec))
(implies (? papa) (and (? papa) (? quebec)))))
(remember-rule '(simplification
(and (? papa) (? quebec))
(? papa)))
(remember-rule '(conjunction
(? papa)
(? quebec)
(and (? papa) (? quebec))))
(remember-rule '(addition
(? papa)
(or (? papa) (? quebec))))
;;; Rules end here.
Now here are the assertions; as noted above, they represent the
logical formulations of the five proverbs for which Copi has supplied
a translation into plain English. In each case I have indicated the
proverb in a comment. REMEMBER-ASSERTION is another function from
W&H's book; it's almost like REMEMBER-RULE but here the global
variable is *ASSERTIONS*, the assertion stream:
;;; Assertions begin here.
;; Every dog has his day.
(remember-assertion
'(alambda (xray)
(implies (funcall *big-delta* xray)
(ilambda (yankee)
(and (funcall *big-yankee* yankee)
(funcall *big-bravo* yankee xray))))))
;; All things come to him who waits.
(remember-assertion
'(alambda (xray)
(implies (and (funcall *big-papa* xray)
(funcall *big-zulu* xray))
(alambda (yankee)
(funcall *big-uniform* yankee xray)))))
;; A person is judged by the company he keeps.
(remember-assertion
'(alambda (xray)
(implies (funcall *big-papa* xray)
(alambda (yankee)
(implies (funcall *big-quebec* xray yankee)
(funcall *big-oscar* yankee xray))))))
;; It's an ill wind that blows nobody any good.
(remember-assertion
'(alambda (xray)
(implies
(and
(funcall *big-whiskey* xray)
(alambda (yankee)
(implies
(funcall *big-papa* yankee)
(not (ilambda (zulu)
(and (funcall *big-november* zulu)
(funcall *big-papa* xray zulu yankee)))))))
(funcall *big-india* xray))))
;; Nobody borrows everything from everybody.
(remember-assertion
'(alambda (xray)
(implies
(funcall *big-papa* xray)
(ilambda (yankee)
(and (funcall *big-papa* yankee)
(ilambda (zulu)
(not (funcall *big-bravo* xray zulu yankee))))))))
;;; Assertions end here.
What do you think of the notation I used above (in place of Copi's
notation) for representing rules and assertions? Am I off to a good
start?
Well, it took me a long time to type all this and now I've got to go.
"HAPPY THANKSGIVING"!!!!
- Daniel al-Autistiqui
--
Daniel Gerard McGrath: a/k/a "Govende"
I have the developmental disability Autism.
To e-mail me, remove the six upper-case letters at
the beginning of my address.
[This signature is under construction.]
From: Daniel G. "Govende" McGrath
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <u4emo19cbp0ggjlmr7uagrehv2ccukvhkb@4ax.com>
[The 3rd time posting this long message--I strongly desire a response:
come on, it could make me become famous more quickly!]
On Tue, 15 Nov 2005 13:29:45 -0500, "Daniel G. \"Govende\" McGrath"
<···············@hotmail.com> wrote:
>At least I'm fairly sure, as of right now, that LISP is the
>programming language that I want to use as the basis for my system. I
>might have settled on my choice of LISP when I was comparing two
>editions--I have both first and third--of Winston and Horn's _LISP_ (a
>rather well-known book, I believe). The first edition, given to me by
>a friend a long, long time ago, has always seemed sort of hard to read
>every time I look at it, but of course it dealt with MacLISP so maybe
>some aspects of the language were confusing in those days. The newer
>edition that covered Common LISP was bought for me later when I saw it
>in a bookstore. So I was looking at the MacLISP edition and I noticed
>something about "theorem proving" (I think that's what they called it)
>in the chapter on pattern matching, including a function called PROVE.
>I don't really know if this had so much relation to the kind of logic
>that I am trying to get interested in, but it was indeed a logic
>system and there must have been some similarities (I saw something
>about AND, OR, and NOT).
>
>You see, a PROVE-type-of function seems very interesting to me, and I
>always seem to want to figure it out, but parts of it are confusing,
>and there are things that don't make sense because I wouldn't have
>expected them in a PROVE function! As I said above, maybe any series
>of lines of MacLISP code can distract me a little bit. Alas, the part
>about theorem proving had apparently gotten removed by the time the
>third (Common LISP) edition came out! I thought that maybe my kind of
>proving function could possibly get built based on a sort of
>pattern-matching mechanism too. But the stuff on theorem proving that
>they have in Winston and Horn 1st Ed. doesn't seem to me to be exactly
>right.
>
>- Daniel al-Autistiqui
After reading more closely and thoroughly the third edition of Winston
and Horn's book (as opposed to that horrible MacLISP edition), I seem
to have found the part in which they discuss what I need: it's chapter
26 titled "Rule-Based Expert Systems and Forward Chaining". It seems
that their notions of "rules" and "assertions" must really come in
handy. I have come up with a tentative notation system for assertions
that "translates" what Irving Copi uses; it's designed to be used
together with the LISP forward-chaining system in W&H. I have written
down "translations" on paper for each of Copi's proverbs (pgs. 381-2)
for which a solution is given in the back of the book; those are the
"Assertions". I also have a series of "Rules", modeled on the first
nine of Copi's "Rules of Inference" (see pgs. 311-12). I'll now try
posting both the rules and the assertions.
Here are the rules. Note that I have styled them in LISP notation;
the function REMEMBER-RULE is W&H's and adds new rules into the "rule
stream" (the value of global variable *RULES*):
;;; Rules begin here.
(remember-rule '(modus-ponens
(implies (? papa) (? quebec))
(? papa)
(? quebec)))
(remember-rule '(modus-tollens
(implies (? papa) (? quebec))
(not (? quebec))
(not (? papa))))
(remember-rule '(hypothetical-syllogism
(implies (? papa) (? quebec))
(implies (? quebec) (? romeo))
(implies (? papa) (? romeo))))
(remember-rule '(disjunctive-syllogism
(or (? papa) (? quebec))
(not (? papa))
(? quebec)))
(remember-rule '(constructive-dilemma
(and (implies (? papa) (? quebec))
(implies (? romeo) (? sierra)))
(or (? papa) (? romeo))
(or (? quebec) (? sierra))))
(remember-rule '(absorption
(implies (? papa) (? quebec))
(implies (? papa) (and (? papa) (? quebec)))))
(remember-rule '(simplification
(and (? papa) (? quebec))
(? papa)))
(remember-rule '(conjunction
(? papa)
(? quebec)
(and (? papa) (? quebec))))
(remember-rule '(addition
(? papa)
(or (? papa) (? quebec))))
;;; Rules end here.
Now here are the assertions; as noted above, they represent the
logical formulations of the five proverbs for which Copi has supplied
a translation into plain English. In each case I have indicated the
proverb in a comment. REMEMBER-ASSERTION is another function from
W&H's book; it's almost like REMEMBER-RULE but here the global
variable is *ASSERTIONS*, the assertion stream:
;;; Assertions begin here.
;; Every dog has his day.
(remember-assertion
'(alambda (xray)
(implies (funcall *big-delta* xray)
(ilambda (yankee)
(and (funcall *big-yankee* yankee)
(funcall *big-bravo* yankee xray))))))
;; All things come to him who waits.
(remember-assertion
'(alambda (xray)
(implies (and (funcall *big-papa* xray)
(funcall *big-zulu* xray))
(alambda (yankee)
(funcall *big-uniform* yankee xray)))))
;; A person is judged by the company he keeps.
(remember-assertion
'(alambda (xray)
(implies (funcall *big-papa* xray)
(alambda (yankee)
(implies (funcall *big-quebec* xray yankee)
(funcall *big-oscar* yankee xray))))))
;; It's an ill wind that blows nobody any good.
(remember-assertion
'(alambda (xray)
(implies
(and
(funcall *big-whiskey* xray)
(alambda (yankee)
(implies
(funcall *big-papa* yankee)
(not (ilambda (zulu)
(and (funcall *big-november* zulu)
(funcall *big-papa* xray zulu yankee)))))))
(funcall *big-india* xray))))
;; Nobody borrows everything from everybody.
(remember-assertion
'(alambda (xray)
(implies
(funcall *big-papa* xray)
(ilambda (yankee)
(and (funcall *big-papa* yankee)
(ilambda (zulu)
(not (funcall *big-bravo* xray zulu yankee))))))))
;;; Assertions end here.
What do you think of the notation I used above (in place of Copi's
notation) for representing rules and assertions? Am I off to a good
start?
Well, it took me a long time to type all this and now I've got to go.
"HAPPY THANKSGIVING"!!!!
- Daniel al-Autistiqui
--
Daniel Gerard McGrath: a/k/a "Govende"
I have the developmental disability Autism.
To e-mail me, remove the six upper-case letters at
the beginning of my address.
[This signature is under construction.]
From: Daniel G. "Govende" McGrath
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <bhemo1pp6qs4ae4kfk1b04nchc4qvs8t7d@4ax.com>
[The 4th time posting this long message--I strongly desire a response:
come on, it could make me become famous more quickly!]
On Tue, 15 Nov 2005 13:29:45 -0500, "Daniel G. \"Govende\" McGrath"
<···············@hotmail.com> wrote:
>At least I'm fairly sure, as of right now, that LISP is the
>programming language that I want to use as the basis for my system. I
>might have settled on my choice of LISP when I was comparing two
>editions--I have both first and third--of Winston and Horn's _LISP_ (a
>rather well-known book, I believe). The first edition, given to me by
>a friend a long, long time ago, has always seemed sort of hard to read
>every time I look at it, but of course it dealt with MacLISP so maybe
>some aspects of the language were confusing in those days. The newer
>edition that covered Common LISP was bought for me later when I saw it
>in a bookstore. So I was looking at the MacLISP edition and I noticed
>something about "theorem proving" (I think that's what they called it)
>in the chapter on pattern matching, including a function called PROVE.
>I don't really know if this had so much relation to the kind of logic
>that I am trying to get interested in, but it was indeed a logic
>system and there must have been some similarities (I saw something
>about AND, OR, and NOT).
>
>You see, a PROVE-type-of function seems very interesting to me, and I
>always seem to want to figure it out, but parts of it are confusing,
>and there are things that don't make sense because I wouldn't have
>expected them in a PROVE function! As I said above, maybe any series
>of lines of MacLISP code can distract me a little bit. Alas, the part
>about theorem proving had apparently gotten removed by the time the
>third (Common LISP) edition came out! I thought that maybe my kind of
>proving function could possibly get built based on a sort of
>pattern-matching mechanism too. But the stuff on theorem proving that
>they have in Winston and Horn 1st Ed. doesn't seem to me to be exactly
>right.
>
>- Daniel al-Autistiqui
After reading more closely and thoroughly the third edition of Winston
and Horn's book (as opposed to that horrible MacLISP edition), I seem
to have found the part in which they discuss what I need: it's chapter
26 titled "Rule-Based Expert Systems and Forward Chaining". It seems
that their notions of "rules" and "assertions" must really come in
handy. I have come up with a tentative notation system for assertions
that "translates" what Irving Copi uses; it's designed to be used
together with the LISP forward-chaining system in W&H. I have written
down "translations" on paper for each of Copi's proverbs (pgs. 381-2)
for which a solution is given in the back of the book; those are the
"Assertions". I also have a series of "Rules", modeled on the first
nine of Copi's "Rules of Inference" (see pgs. 311-12). I'll now try
posting both the rules and the assertions.
Here are the rules. Note that I have styled them in LISP notation;
the function REMEMBER-RULE is W&H's and adds new rules into the "rule
stream" (the value of global variable *RULES*):
;;; Rules begin here.
(remember-rule '(modus-ponens
(implies (? papa) (? quebec))
(? papa)
(? quebec)))
(remember-rule '(modus-tollens
(implies (? papa) (? quebec))
(not (? quebec))
(not (? papa))))
(remember-rule '(hypothetical-syllogism
(implies (? papa) (? quebec))
(implies (? quebec) (? romeo))
(implies (? papa) (? romeo))))
(remember-rule '(disjunctive-syllogism
(or (? papa) (? quebec))
(not (? papa))
(? quebec)))
(remember-rule '(constructive-dilemma
(and (implies (? papa) (? quebec))
(implies (? romeo) (? sierra)))
(or (? papa) (? romeo))
(or (? quebec) (? sierra))))
(remember-rule '(absorption
(implies (? papa) (? quebec))
(implies (? papa) (and (? papa) (? quebec)))))
(remember-rule '(simplification
(and (? papa) (? quebec))
(? papa)))
(remember-rule '(conjunction
(? papa)
(? quebec)
(and (? papa) (? quebec))))
(remember-rule '(addition
(? papa)
(or (? papa) (? quebec))))
;;; Rules end here.
Now here are the assertions; as noted above, they represent the
logical formulations of the five proverbs for which Copi has supplied
a translation into plain English. In each case I have indicated the
proverb in a comment. REMEMBER-ASSERTION is another function from
W&H's book; it's almost like REMEMBER-RULE but here the global
variable is *ASSERTIONS*, the assertion stream:
;;; Assertions begin here.
;; Every dog has his day.
(remember-assertion
'(alambda (xray)
(implies (funcall *big-delta* xray)
(ilambda (yankee)
(and (funcall *big-yankee* yankee)
(funcall *big-bravo* yankee xray))))))
;; All things come to him who waits.
(remember-assertion
'(alambda (xray)
(implies (and (funcall *big-papa* xray)
(funcall *big-zulu* xray))
(alambda (yankee)
(funcall *big-uniform* yankee xray)))))
;; A person is judged by the company he keeps.
(remember-assertion
'(alambda (xray)
(implies (funcall *big-papa* xray)
(alambda (yankee)
(implies (funcall *big-quebec* xray yankee)
(funcall *big-oscar* yankee xray))))))
;; It's an ill wind that blows nobody any good.
(remember-assertion
'(alambda (xray)
(implies
(and
(funcall *big-whiskey* xray)
(alambda (yankee)
(implies
(funcall *big-papa* yankee)
(not (ilambda (zulu)
(and (funcall *big-november* zulu)
(funcall *big-papa* xray zulu yankee)))))))
(funcall *big-india* xray))))
;; Nobody borrows everything from everybody.
(remember-assertion
'(alambda (xray)
(implies
(funcall *big-papa* xray)
(ilambda (yankee)
(and (funcall *big-papa* yankee)
(ilambda (zulu)
(not (funcall *big-bravo* xray zulu yankee))))))))
;;; Assertions end here.
What do you think of the notation I used above (in place of Copi's
notation) for representing rules and assertions? Am I off to a good
start?
Well, it took me a long time to type all this and now I've got to go.
"HAPPY THANKSGIVING"!!!!
- Daniel al-Autistiqui
--
Daniel Gerard McGrath: a/k/a "Govende"
I have the developmental disability Autism.
To e-mail me, remove the six upper-case letters at
the beginning of my address.
[This signature is under construction.]
From: Daniel G. "Govende" McGrath
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <riemo15ubkik6kv0hl03e45bskugp9i183@4ax.com>
[The 5th time posting this long message--I strongly desire a response:
come on, it could make me become famous more quickly!]
On Tue, 15 Nov 2005 13:29:45 -0500, "Daniel G. \"Govende\" McGrath"
<···············@hotmail.com> wrote:
>At least I'm fairly sure, as of right now, that LISP is the
>programming language that I want to use as the basis for my system. I
>might have settled on my choice of LISP when I was comparing two
>editions--I have both first and third--of Winston and Horn's _LISP_ (a
>rather well-known book, I believe). The first edition, given to me by
>a friend a long, long time ago, has always seemed sort of hard to read
>every time I look at it, but of course it dealt with MacLISP so maybe
>some aspects of the language were confusing in those days. The newer
>edition that covered Common LISP was bought for me later when I saw it
>in a bookstore. So I was looking at the MacLISP edition and I noticed
>something about "theorem proving" (I think that's what they called it)
>in the chapter on pattern matching, including a function called PROVE.
>I don't really know if this had so much relation to the kind of logic
>that I am trying to get interested in, but it was indeed a logic
>system and there must have been some similarities (I saw something
>about AND, OR, and NOT).
>
>You see, a PROVE-type-of function seems very interesting to me, and I
>always seem to want to figure it out, but parts of it are confusing,
>and there are things that don't make sense because I wouldn't have
>expected them in a PROVE function! As I said above, maybe any series
>of lines of MacLISP code can distract me a little bit. Alas, the part
>about theorem proving had apparently gotten removed by the time the
>third (Common LISP) edition came out! I thought that maybe my kind of
>proving function could possibly get built based on a sort of
>pattern-matching mechanism too. But the stuff on theorem proving that
>they have in Winston and Horn 1st Ed. doesn't seem to me to be exactly
>right.
>
>- Daniel al-Autistiqui
After reading more closely and thoroughly the third edition of Winston
and Horn's book (as opposed to that horrible MacLISP edition), I seem
to have found the part in which they discuss what I need: it's chapter
26 titled "Rule-Based Expert Systems and Forward Chaining". It seems
that their notions of "rules" and "assertions" must really come in
handy. I have come up with a tentative notation system for assertions
that "translates" what Irving Copi uses; it's designed to be used
together with the LISP forward-chaining system in W&H. I have written
down "translations" on paper for each of Copi's proverbs (pgs. 381-2)
for which a solution is given in the back of the book; those are the
"Assertions". I also have a series of "Rules", modeled on the first
nine of Copi's "Rules of Inference" (see pgs. 311-12). I'll now try
posting both the rules and the assertions.
Here are the rules. Note that I have styled them in LISP notation;
the function REMEMBER-RULE is W&H's and adds new rules into the "rule
stream" (the value of global variable *RULES*):
;;; Rules begin here.
(remember-rule '(modus-ponens
(implies (? papa) (? quebec))
(? papa)
(? quebec)))
(remember-rule '(modus-tollens
(implies (? papa) (? quebec))
(not (? quebec))
(not (? papa))))
(remember-rule '(hypothetical-syllogism
(implies (? papa) (? quebec))
(implies (? quebec) (? romeo))
(implies (? papa) (? romeo))))
(remember-rule '(disjunctive-syllogism
(or (? papa) (? quebec))
(not (? papa))
(? quebec)))
(remember-rule '(constructive-dilemma
(and (implies (? papa) (? quebec))
(implies (? romeo) (? sierra)))
(or (? papa) (? romeo))
(or (? quebec) (? sierra))))
(remember-rule '(absorption
(implies (? papa) (? quebec))
(implies (? papa) (and (? papa) (? quebec)))))
(remember-rule '(simplification
(and (? papa) (? quebec))
(? papa)))
(remember-rule '(conjunction
(? papa)
(? quebec)
(and (? papa) (? quebec))))
(remember-rule '(addition
(? papa)
(or (? papa) (? quebec))))
;;; Rules end here.
Now here are the assertions; as noted above, they represent the
logical formulations of the five proverbs for which Copi has supplied
a translation into plain English. In each case I have indicated the
proverb in a comment. REMEMBER-ASSERTION is another function from
W&H's book; it's almost like REMEMBER-RULE but here the global
variable is *ASSERTIONS*, the assertion stream:
;;; Assertions begin here.
;; Every dog has his day.
(remember-assertion
'(alambda (xray)
(implies (funcall *big-delta* xray)
(ilambda (yankee)
(and (funcall *big-yankee* yankee)
(funcall *big-bravo* yankee xray))))))
;; All things come to him who waits.
(remember-assertion
'(alambda (xray)
(implies (and (funcall *big-papa* xray)
(funcall *big-zulu* xray))
(alambda (yankee)
(funcall *big-uniform* yankee xray)))))
;; A person is judged by the company he keeps.
(remember-assertion
'(alambda (xray)
(implies (funcall *big-papa* xray)
(alambda (yankee)
(implies (funcall *big-quebec* xray yankee)
(funcall *big-oscar* yankee xray))))))
;; It's an ill wind that blows nobody any good.
(remember-assertion
'(alambda (xray)
(implies
(and
(funcall *big-whiskey* xray)
(alambda (yankee)
(implies
(funcall *big-papa* yankee)
(not (ilambda (zulu)
(and (funcall *big-november* zulu)
(funcall *big-papa* xray zulu yankee)))))))
(funcall *big-india* xray))))
;; Nobody borrows everything from everybody.
(remember-assertion
'(alambda (xray)
(implies
(funcall *big-papa* xray)
(ilambda (yankee)
(and (funcall *big-papa* yankee)
(ilambda (zulu)
(not (funcall *big-bravo* xray zulu yankee))))))))
;;; Assertions end here.
What do you think of the notation I used above (in place of Copi's
notation) for representing rules and assertions? Am I off to a good
start?
Well, it took me a long time to type all this and now I've got to go.
"HAPPY THANKSGIVING"!!!!
- Daniel al-Autistiqui
--
Daniel Gerard McGrath: a/k/a "Govende"
I have the developmental disability Autism.
To e-mail me, remove the six upper-case letters at
the beginning of my address.
[This signature is under construction.]
From: Coby Beck
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <wzJif.133391$S4.116489@edtnps84>
"Daniel G. "Govende" McGrath" <···············@hotmail.com> wrote in message
·······································@4ax.com...
> [The 5th time posting this long message--I strongly desire a response:
> come on, it could make me become famous more quickly!]
That is actually more likely to piss people off than get a quick response!
Cheers,
--
Coby Beck
(remove #\Space "coby 101 @ bigpond . com")
From: Daniel G. "Govende" McGrath
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <shvoo151l5k78e4klhs0g6oltushq47cm7@4ax.com>
On Mon, 28 Nov 2005 20:15:24 GMT, "Coby Beck" <·····@mercury.bc.ca>
wrote:
>"Daniel G. "Govende" McGrath" <···············@hotmail.com> wrote in message
>·······································@4ax.com...
>> [The 5th time posting this long message--I strongly desire a response:
>> come on, it could make me become famous more quickly!]
>
>That is actually more likely to piss people off than get a quick response!
>
>Cheers,
Well, someone please _tell_ me--why did I proceed to type a rather
long message before the start of Thanksgiving vacation, only to find
to my disappointment, in checking when I got back, that not a single
response appeared? Besides, it _did_ ask a question--I was hoping
that someone might give me an answer and perhaps also help me a little
bit further with my project.
Perhaps someday we'll need to have a new parameter on Usenet messages,
an integer that measures how much desire the poster has that people
should respond. Then everyone will try to look at all the posts
designated as, say, 1000 and they won't need to concentrate so much on
those that carry a lower number, such as 1. We could add to all the
newsreaders a function that "sorts" all messages that appear by these
values so that the 1000's and such would be easier to recognize.
- Daniel al-Autistiqui
--
Daniel Gerard McGrath: a/k/a "Govende"
I have the developmental disability Autism.
To e-mail me, remove the six upper-case letters at
the beginning of my address.
[This signature is under construction.]
Daniel G. "Govende" McGrath wrote:
> Well, someone please _tell_ me--why did I proceed to type a rather
> long message before the start of Thanksgiving vacation,
I suspect because you wanted a response.
> only to find
> to my disappointment, in checking when I got back, that not a single
> response appeared?
Because no one felt like giving you a response.
> Perhaps someday we'll need to have a new parameter on Usenet messages,
> an integer that measures how much desire the poster has that people
> should respond.
You don't have much experience with actual people, do you?
> Then everyone will try to look at all the posts
> designated as, say, 1000 and they won't need to concentrate so much on
> those that carry a lower number, such as 1.
Why would they do that instead of doing as they do today, namely
responding
to those messages that they want to respond to?
People don't owe you a response. Your desires are not other people's
obligations.
-andy
From: Pascal Bourguignon
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <87d5kjnzvn.fsf@thalassa.informatimago.com>
"Daniel G. \"Govende\" McGrath" <···············@hotmail.com> writes:
> On Mon, 28 Nov 2005 20:15:24 GMT, "Coby Beck" <·····@mercury.bc.ca>
> wrote:
>
>>"Daniel G. "Govende" McGrath" <···············@hotmail.com> wrote in message
>>·······································@4ax.com...
>>> [The 5th time posting this long message--I strongly desire a response:
>>> come on, it could make me become famous more quickly!]
>>
>>That is actually more likely to piss people off than get a quick response!
>>
>>Cheers,
>
> Well, someone please _tell_ me--why did I proceed to type a rather
> long message before the start of Thanksgiving vacation, only to find
> to my disappointment, in checking when I got back, that not a single
> response appeared? Besides, it _did_ ask a question--I was hoping
> that someone might give me an answer and perhaps also help me a little
> bit further with my project.
>
> Perhaps someday we'll need to have a new parameter on Usenet messages,
> an integer that measures how much desire the poster has that people
> should respond. Then everyone will try to look at all the posts
> designated as, say, 1000 and they won't need to concentrate so much on
> those that carry a lower number, such as 1. We could add to all the
> newsreaders a function that "sorts" all messages that appear by these
> values so that the 1000's and such would be easier to recognize.
You can get answers in two cases:
- somebody know already the answer and can give it fast enough (short
answer, or existing reference).
- someone has time and taste to search an answer either on google
(yes, yes, some people ask questions answered by google), or
developing the answer himself, doing the research and development.
I don't know for others, but sorry, I don't know the answer to your
question, and I don't have the time I estimate I would need to study
your problem and develop a solution. (I'm guessing it can't be found
on google).
--
__Pascal Bourguignon__ http://www.informatimago.com/
Kitty like plastic.
Confuses for litter box.
Don't leave tarp around.
From: Alan Crowe
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <86y8357tty.fsf@cawtech.freeserve.co.uk>
"Daniel G. \"Govende\" McGrath" <···············@hotmail.com> writes:
> Well, someone please _tell_ me--why did I proceed to type a rather
> long message before the start of Thanksgiving vacation, only to find
> to my disappointment, in checking when I got back, that not a single
> response appeared? Besides, it _did_ ask a question--I was hoping
> that someone might give me an answer and perhaps also help me a little
> bit further with my project.
I sympathise. I often write long posts that get no
reply. The basic problem is that life is short. People read
the short posts first, and run out of time before they get
to the long ones, especially the long ones with lots of
difficult details.
My approach is to only write a long posts that I either
enjoy writing, or that serve my own purposes. That way I
don't mind so much if no-one replies.
For example, I've just replied to "keyboard" suggesting that
he use REDUCE in his code. However the real story is that I
think that my code would be better if I used REDUCE more, so
writing the post is mainly about fixing the point in my
memory so that I don't miss chances to use REDUCE in my own
code.
So I'm not spending my time handing out free advice in a
spirit of self sacrifice (and if my advice is bad, it is
atleast sincere)
I think hardly anyone has the time to respond to long,
detailed posts, except in the rare cases that the post
co-incides with what they are already working on, and
wrting a reply serves a dual purpose, both engaging in dialogue
and clarifying thoughts they would be wrestling with as part
of their already scheduled work.
Whoops. I've just written "...hardly anyone has the time to
respond to long, detailed posts,..." But "......hardly
anyone has the time to read long, detailed posts,..." would
be closer to the truth.
Summary: Usenet is for fun chit-chat not technically
detailed collaboration.
Alan Crowe
Edinburgh
Scotland
From: Dan Christensen
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <Z1def.1798$hW.152@tor-nn1>
"Daniel G. "Govende" McGrath" <···············@hotmail.com> wrote in message
·······································@4ax.com...
> Hello everyone. I keep wanting to become "famous", perhaps by proving
> something in advanced mathematics. The reason is that a lot of people
> do not understand how severely disabled I can be, even though I am
> very smart in some ways, and if I became famous the autism that _I_
> have in its precise form could become more widely known than it is
> now. By the people that do not understand, I mostly mean the staff at
> the residential facility that I have resided at for over 2 years
> (because of my disabilities). I try to explain all about it to the
> staff, and they're just not convinced.
>
> Thus, to go about "proving" something, I need to basically learn
> mathematics over from scratch. I learned calculus around age 9 or 10,
> but when I was about 12, I found that I could no longer take anything
> "for granted". Now you see--some time ago, one of the staff who work
> with me gave me a copy of Irving M. Copi's _Introduction to Logic_
> (7th ed.). I found it interesting to be reading a book on logic,
> since it seems that all of the notation used in mathematics could
> somehow be expressed as logical formulas. (In other words, logic is
> the whole basis of mathematics.) Have any of you folks on sci.logic
> read Copi's book? I keep looking on page 381, noting how he neatly
> created a "vocabulary" that could be used to translate English
> proverbs into the symbolic language that he uses for logic.
>
> However, I don't exactly think that his notation is the best choice (I
> don't think I can explain why). It would be nicer if this was
> expressed as more like a form that one would use on a computer.
[snip]
I have developed a notation that uses only the standard computer keyboard,
the only exception being the epsilon (set membership) which is mapped to the
·@" character. The notation was designed to be easily learned by students.
It is used in my DC Proof software, which is available at my website. See
the User Reference Guide for a full explanation of the notation. You may
also be interested in the tutorial which can be used as an introduction to
formal logic (natural deduction) and the foundations of mathematics (based
on a simplified set theory).
Dan
Download my DC Proof software at http://www.dcproof.com (Last updated
2005-08-08)
From: David Steuber
Subject: Re: Notation of symbolic logic can be confusing!!! Computer-languages? LISP????
Date:
Message-ID: <87d5l2gui7.fsf@david-steuber.com>
"Daniel G. \"Govende\" McGrath" <···············@hotmail.com> writes:
> However, I don't exactly think that his notation is the best choice (I
> don't think I can explain why). It would be nicer if this was
> expressed as more like a form that one would use on a computer. That
> is what I am used to, and I would be more comfortable with
> that--specifically, something related to the LISP programming language
> (hence the crossposting) would be good. I am quite knowledgeable
> about LISP, and given the nature of the programming language it would
> seem that logical statements could be represented easily by most
> people. Just not by me--what I need to do first is rewrite Copi's
> symbolic notation in the form of LISP lists, or some such thing.
> Maybe someone can help me with that.
If you don't already have a copy, you should get Peter Norvig's
Paradigms of Artificial Intelligence Programming: Case Studies in
Common Lisp. Not only will it give you a quick review of Lisp, it has
all sorts of good stuff in it including a Prolog implementation.
I also second the recommendation for Godel, Escher, Bach.
Comp.lang.lisp has also had some various ML examples posted. The AST
transforms are something Lisp should be quite suitable for and you can
build a theorem prover using that style of representation as an
embedded DSL in Lisp.
--
http://www.david-steuber.com/
The UnBlog: An island of conformity in a sea of quirks.
http://www.david-steuber.com/snippets/Boycott_Sony/
Daniel G. "Govende" McGrath wrote:
> However, I don't exactly think that his notation is the best choice (I
> don't think I can explain why). It would be nicer if this was
> expressed as more like a form that one would use on a computer. That
> is what I am used to, and I would be more comfortable with
> that--specifically, something related to the LISP programming language
> (hence the crossposting) would be good.
One resource that might be good for you to check out: Gregory J.
Chaitin's book, _The Limits of Mathematics_.
http://www.umcs.maine.edu/~chaitin/lm.html