Automated Theorem Proving
Author
I want to learn automated theorem proving to use it in a conversational agent. Although I have found a multitude of information using [google], I don't think I am qualified enough to choose what to read.
Till now, I found this PDF draft...
Plus, what should Prolog have to do with what I am trying to learn. Is it the thing am trying to implement, or does it help in implementing it...
How much time do you think it will take to learn such a vast subject
I'd suspect, Lots. :)
A friend of mine is working on his PhD in the area. Well, an easier question -- he's working on making a language whose programs are equivilent to proofs, last I checked.
AI is hard. Once something is easy enough to use, people stop calling it AI. ;)
A friend of mine is working on his PhD in the area. Well, an easier question -- he's working on making a language whose programs are equivilent to proofs, last I checked.
AI is hard. Once something is easy enough to use, people stop calling it AI. ;)
Quote:Original post by NotAYakkThe Curry-Howard isomorphism states programs are proofs, and types are propositions. Traditional languages don't support very detailed propositions, but those with dependent typing do - Epigram for example.
A friend of mine is working on his PhD in the area. Well, an easier question -- he's working on making a language whose programs are equivilent to proofs, last I checked.
If you are interested in this stuff, I suggest you check out the Epigram programming language and Coq or another theorem prover.
Author
I am sorry about the crosspost, but it seemed like the AI forum is a bit slow.
Anyway, in the long-term, the application of ATP should be interfaced with C++. Assuming I do develop algorithms in Prolog, is it possible to directly interface that results to a C++ application. I need to know about this before diving into Prolog.
Anyway, in the long-term, the application of ATP should be interfaced with C++. Assuming I do develop algorithms in Prolog, is it possible to directly interface that results to a C++ application. I need to know about this before diving into Prolog.
Quote:Original post by RebootedQuote:Original post by NotAYakkThe Curry-Howard isomorphism states programs are proofs, and types are propositions. Traditional languages don't support very detailed propositions, but those with dependent typing do - Epigram for example.
A friend of mine is working on his PhD in the area. Well, an easier question -- he's working on making a language whose programs are equivilent to proofs, last I checked.
If you are interested in this stuff, I suggest you check out the Epigram programming language and Coq or another theorem prover.
Fie. Turing tar-pit. Sure, a program is a proof -- but a proof of what?
The proof of a statement (like, there is an integer with property X), and the program that executes the implied problem (find the integer with property X), and having a nice bijection such that "nice proofs" and "efficient programs" map to each other...
Now that is interesting. :)
Quote:Original post by NotAYakkQuote:Original post by RebootedQuote:Original post by NotAYakkThe Curry-Howard isomorphism states programs are proofs, and types are propositions. Traditional languages don't support very detailed propositions, but those with dependent typing do - Epigram for example.
A friend of mine is working on his PhD in the area. Well, an easier question -- he's working on making a language whose programs are equivilent to proofs, last I checked.
If you are interested in this stuff, I suggest you check out the Epigram programming language and Coq or another theorem prover.
Fie. Turing tar-pit. Sure, a program is a proof -- but a proof of what?
The proof of a statement (like, there is an integer with property X), and the program that executes the implied problem (find the integer with property X), and having a nice bijection such that "nice proofs" and "efficient programs" map to each other...
Now that is interesting. :)
Yayy. But what measures the niceness of a proof? That seems to be a pretty objectively undefinable thing. What make a proof elegant and beautiful? Its simplicity and its shortness? If so, then one does not need to write a program explicitly as proof to know that it is elegant and beautiful - it will already be short and simple.
Besides, programs in Prolog are essentially already proofs in a first order logic (not sure of what type of logic specifically).
---
Can you be more specific? There exists an integer -> find integer with property x is pretty vague. This does not seem a good way to write general programs but it seems a brilliant way to attack programming problems of a strongly abstractly mathematical type. At the moment I am thinking Number theory and cryptology type stuff. But such a thing seems like something that can easily be built on top of an ML or Haskell type language rather than be its own language.
P.s. Have you seen Mizar?
Quote:Original post by arithma
I want to learn automated theorem proving to use it in a conversational agent. Although I have found a multitude of information using [google], I don't think I am qualified enough to choose what to read.
Till now, I found this PDF draft...
Plus, what should Prolog have to do with what I am trying to learn. Is it the thing am trying to implement, or does it help in implementing it...
How much time do you think it will take to learn such a vast subject
Might I ask why you would want to do this for a conversational agent? Forgive my ignorance but I find it difficult to imagine how an ATP might improve or make the implementation of your agent more efficient.
Prolog is a natural language to do logic programming in (as opposed to an imperative language like C++) and is the standard for such things. Just as Java is traditionally used to teach OOP and like the case of Java, the better offerings (smalltalk or ruby - *runs and hides*) are not used to teach because professors do not like keeping up to date with developments in technology.
[Edited by - Daerax on June 28, 2006 9:22:04 PM]
Quote:Original post by arithma
I am sorry about the crosspost, but it seemed like the AI forum is a bit slow.
Anyway, in the long-term, the application of ATP should be interfaced with C++. Assuming I do develop algorithms in Prolog, is it possible to directly interface that results to a C++ application. I need to know about this before diving into Prolog.
Why would you want to do such a thing in C++? It is certainly not an appropriate language for this type of thing. Nonetheless you can "interface prolog and c++" but be certain it will not be a smooth thing - which is as well a function of how you intend to use the ATP. Expand your horizons, learn Prolog regardless.
Quote:Original post by RebootedQuote:Original post by NotAYakkThe Curry-Howard isomorphism states programs are proofs, and types are propositions. Traditional languages don't support very detailed propositions, but those with dependent typing do - Epigram for example.
A friend of mine is working on his PhD in the area. Well, an easier question -- he's working on making a language whose programs are equivilent to proofs, last I checked.
If you are interested in this stuff, I suggest you check out the Epigram programming language and Coq or another theorem prover.
Coq is not a thereom prover, more an assister. Isabelle is the industry standard theorem prover.
On the converse side of things, I worked with some guys in Sydney who are verifying a microkernel OS with Isabelle (see e.g., http://www.ertos.nicta.com.au/research/l4.verified/).
But I am confused as to why an automated theorem prover would be beneficial for an agent. Full autonomy in theorem proving only exists atm for very simple logic. However you probably only need a deduction/resolution mechanism (as is found in e.g. prolog).
But I am confused as to why an automated theorem prover would be beneficial for an agent. Full autonomy in theorem proving only exists atm for very simple logic. However you probably only need a deduction/resolution mechanism (as is found in e.g. prolog).
This topic is closed to new replies.
Advertisement
Popular Topics
Advertisement
