Well, you need to know what the right heuristics for
the mathematical domain are. *Consistency* and
*Unification* (maths that links togther two or more
previously seperate areas) seem like two good core
heuristical principles. Good maths is maths which is
consistent and maths which links
--- Ben Goertzel [EMAIL PROTECTED] wrote:
Marc,
Welcome to the AGI list, but could you please post
in text only, not in HTML? HTML posts make it hard
for others to post responses...
Regarding your point that
Another point is that some forms of mathematics are
much more complex
--- Ben Goertzel [EMAIL PROTECTED] wrote:
Marc,
The
most complex math I know of is in the domain of
algebraic topology and algebraic geometry -- for
instance, the stuff used in Wiles's proof of
Fermat's Last Theorem. IMO that math is much
deeper
and more complex than any of
Yeeehaaa!
A new AGI list for me to post to! Hey hey hey there guys! Hee hee
Though it may seem sterile and formal to the nonmathematician, in fact theorem-proving is a rich domain, which immediately leads one into subtle issues of cognitive science. As the history
I think that correctly implementing those heuristics, is the main and only
source of complexity in theorem proving. I.e in correctly identifying
such things as
1) which lines of arguments are useful for the proof
2) which generalizations/induction assumptions are likely true
3) which special cases
Indeed a system based on genetic programming and BOA (afaik that's
what Novamente uses?) can show good results especially when there is a
good metric of program performance. Actually, I've looked into this
approach for quite some time already and it is very promising IMO.
What I'm trying to
Luke wrote:
Yes, but this is very difficult. In the theorem provers mentioned
above you can add tactics and make the prover try to prove
the theorem using a tactic. But to make it learn and deduce which
lines of arguments are better you need some meta-mathematical
representation of the process
What I'm trying to envision now, is some sort of programming system
where instead of writing procedural code, classes/modules/whatever are
specified purely declaratively, in a formal way. And the prover will
generate the implementation on its own. One can imagine a library of
specifications which
In a sense yes, what I want is some prolog on steroids. However I
have a feeling that a system that works would have little in common
with Prolog except the basic idea of pure declarative programming.
Prolog does not offer means to reason in the domain of computer
programs. One can make
Hi.
Does someone have any knowledge of the best automated reasoning
algorithms and techniques existing today? And what they are capable
of? From what I could find in Google, it seems that theorem proving is
successfully used in applied areas like integrated circuit
verification, but there is
I do believe your talking about multiple modules..
those of,Perception,Reasoning,Actions,
Perception modules recognizes and or understands the differences between
modules...
Reasoning is the logic behind any possable changes in those modules and
Actions is the goal based direction someone
Hello,
Does someone have any knowledge of the best automated reasoning
algorithms and techniques existing today? And what they are capable
of? From what I could find in Google, it seems that theorem proving is
successfully used in applied areas like integrated circuit
verification, but there
12 matches
Mail list logo
