This is the
talk page for discussing improvements to the
Automated theorem proving article. This is not a forum for general discussion of the article's subject. |
Article policies
|
Find sources: Google ( books · news · scholar · free images · WP refs) · FENS · JSTOR · TWL |
This article is rated Start-class on Wikipedia's
content assessment scale. It is of interest to the following WikiProjects: | ||||||||||||||||||||||||||||
|
To-do list for Automated theorem proving:
|
there's a large (and important) class of techniques and provers that are barely even mentioned in this article, namely inductive theorem provers. i've searched, but cannot find an article on inductive theorem proving and the techniques in use in that field. should this article be expanded beyond first order theorem proving and model checking? 137.195.27.231 16:01, 29 October 2007 (UTC)
Should this article be merged with Computer-assisted proof? S Sepp 14:33, 21 January 2006 (UTC)
No: computer-assisted proofs also include interactive theorem provers which are, by def., not automated. Vincent Aravantinos ( talk) 18:33, 20 October 2011 (UTC)
I don't think it's a good idea to have this 'important people' list included. Such a list is almost always biased. E.g. in this list, there are not even all winners of the Herbrand award, the most prestigious award in the field, included.
I propose to delete this list.
Ulrich Furbach
If one is going to have an important people list, at least an effort should be made to make it reasonable. Nahaj 02:16:07, 2005-08-31 (UTC)
Better to have a history of automated theorem proving list. The "important people" will stand out without having to explicitly say they are important. —Preceding unsigned comment added by 94.173.19.247 ( talk) 10:48, 14 February 2011 (UTC)
I also think this list of important/notable people is not very appropriate. It doesn't fit the general style of Wikipedia (I cannot remember any other Wikipedia page where there is such a long list of people). It makes the article ugly (the list of people is almost as long as the sum of all other textual subsections in the beginning of the article). Finally, it also gives a bad impression of the Automated Deduction community (a visitor has the feeling that this community is more interested in promoting themselves and their colleagues by making a list of notable people, than in improving the quality of the article itself). A user who searches for ``automated deduction in an encyclopedia is mostly interested in a definition of automated deduction and in an overview of the existing techniques, not in seeing a long list of names that he has never seen before. It would suggest removing this list and creating a new textual section (or eventually a new separate article) called ``History of Automated Deduction. My knowledge of history of the field is not good enough (yet). Does any of you know someone with historical knowledge and willing to write this section? -- Ceilican ( talk) 07:05, 27 June 2011 (UTC)
Hi,
I'm not particularly happy with all of the recent edits. In particular, no serious ATP system enumerates all possible proof trees - all implement a refutation-complete calculus with redundancy criteria, and use a fair derivation strategy.
I also think that we are now moving to many details into the introduction.
Any comments?
-- Stephan Schulz 16:58, 12 September 2005 (UTC)
I dont know if this is the right place to ask, but i quite dont understand something: if the problem is recursively enumerable you can not always halt for sentences in the language. Then, how is it decidible? BTW, i belive this article also should be merged with automated reasoning. -- VyNiL 11:45, 14 August 2006 (UTC)
I don't know what the policy on spelling proper names is, but the theorem prover listed as "Vampire" is spelt "Vampyre" by the project itself (see http://www.cs.ucla.edu/~rupak/Vampyre/). Perhaps a spell-change is in order? —Preceding unsigned comment added by 74.130.8.62 ( talk • contribs)
Hi,
I'm missing some seemingly relevant references to Schmidhuber's universal self-referential Gödel-machines. They are `machines' (not `incarnated' as in the Turing Machine) that can rewrite themselves based on expected progress of a proof. I'm not an expert of this research in particular, but I think it is certainly relevant and a candidate for inclusion on this page.
A pointer for Schmidhubers work can be found here: http://www.idsia.ch/~juergen/goedelmachine.html
Regards, Erik de Bruijn —Preceding unsigned comment added by 85.147.200.8 ( talk) 17:51, 28 October 2007 (UTC)
Could someone that speaks Chinese possibly check the link to his home page to determine his institutional affiliation? (None is listed) Nahaj ( talk) 14:50, 14 August 2008 (UTC)
From the webpages of Wu Wenjun (Wu Wentsun) or some webpage concerned with him (such as the webpage of his affiliation),
http://sourcedb.amss.cas.cn/zw/zjrck/200907/t20090713_2065285.html http://www.mmrc.iss.ac.cn/~wtwu/ http://www.mmrc.iss.ac.cn/~wtwu/main.html http://www.cas.cn/ky/kjjl/gjzgkxjsj/2000n/wwj/ http://english.amss.cas.cn/pe/
his affiliation is:
Academy of Mathematics and Systems Science (AMSS) in the Chinese Academy of Sciences (CAS).
Liwenwei1980 ( talk) 16:57, 19 January 2016 (UTC)
In the section on "decidability" there is a reference to the "first-order theory of the natural numbers" used in Gödel's incompleteness theorem. I couldn't find a reference for this theory in itself. Is it just Peano arithmetic? If you know, please fix the link. —Preceding unsigned comment added by Ezrakilty ( talk • contribs) 13:36, 19 August 2008 (UTC)
The article should have a section on results from algebraic geometry on theorem proving, e.g. Characteristic set and Wu's method. A good introductory reference is Cox, Little and O'Shea's Ideals, Varieties and Algorithms. Akriasas ( talk) 12:32, 21 December 2008 (UTC)
I fail to see why deontic theorem proving is given a special section. Any modal logic "extends the first-order predicate calculus". Other than to showcase this one specific author, what does this section add to the page? (And if it is necessary, why wouldn't the same logic apply to any of categories of logics?) —Preceding unsigned comment added by 155.101.224.65 ( talk) 20:38, 20 May 2009 (UTC)
I agree and removed the section. Any non-standard logic should be added otherwise. Vincent Aravantinos ( talk) 18:30, 20 October 2011 (UTC)
I recently removed several interactive theorem provers ( diff) from the list, but someone added them back. In my opinion, those don't belong there, because
If there are no objections within the next couple of days, I will re-remove them. – Adrian Willenbücher ( talk) 05:26, 6 September 2010 (UTC)
The section confuses decidability and complexity issues, and needs to be rewritten.
The following changes should be made:
The section needs to define properly "decidability" - that is, giving a true/false (yes/no) answer to any question, and related concept of "semi-decidability" - that true (viz. false) can be answered, but not necessarily that false (viz. true) can be answered in all cases. Refer to Gödel incompleteness and the halting problem.
Note that the incompleteness theorem and halting problem show the non-existence of "universal" functions that can decide on all functions at all inputs. That does not imply the non-existence of functions which can decide about some functions and some inputs. In practice, one can decide many problems precisely by limiting the scope of functions or inputs.
Complexity classes are not related to decidability, so belong in a separate section. (Whether or not a problem is decidable is unrelated to how hard a problem is.) It's better to give a brief discussion about the difficulty (measured in time and space, i.e. memory usage) of solving problems and refer to a separate page about complexity classes. —Preceding unsigned comment added by 94.173.19.247 ( talk) 10:45, 14 February 2011 (UTC)
I think the authors of Jape are Bornat and Sufrin, not Neto. See the links. Rmkeller ( talk) 00:12, 28 February 2011 (UTC)
G. Gonthier might be added to the notable people. — Preceding unsigned comment added by 93.97.194.200 ( talk) 15:19, 10 June 2011 (UTC)
This article really needs a section on the history and development of the field. I came here looking for information on how it got started - and there's nothing on that. Noel (talk) 23:14, 1 September 2012 (UTC)
{{
citation}}
: URL–wikilink conflict (
help)). I'll see if I can cobble something together. --
Stephan Schulz (
talk) 00:36, 2 September 2012 (UTC)I've been working on various AI articles: inference engine, expert systems, etc. and needed to link to this page. BTW, this article is in great shape compared to what some of the AI articles were like. But I want to cast a strong vote to get rid of the "notable people" section. There is no such section on other articles that I've edited. We don't have a list of the notable inference engine or expert system people. If they are notable they are talked about and/or referenced in the article itself and if not then they aren't that notable. These lists are IMO just vanity or buddy lists where everyone adds themselves or their favorite researchers. Especially when they have lots of red links, I think the red links should just go immediately without further discussion but I'm not going to do it as I'm editing other articles now but just wanted to voice my opinion. RedDog ( talk) 14:29, 6 December 2013 (UTC)
"DPLL" is only a special algorithms for the propositional satisfiability problem (SAT), and a more appropriate link, under "Popular techniques", should be to /info/en/?search=Boolean_satisfiability_problem Oliver Kullmann ( talk) 17:11, 5 June 2016 (UTC)
Under "See also" it seems sensible to add a link to /info/en/?search=List_of_long_mathematical_proofs since this contains proofs found by ATP (especially SAT solving). — Preceding unsigned comment added by Oliver Kullmann ( talk • contribs) 17:13, 5 June 2016 (UTC)
I noticed that someone has added yet another person to this section that I've never heard of. I've edited several pages like this (e.g., Expert system Artificial intelligence Knowledge-based system Knowledge-based software assistant and none of them have a section like this. If someone is truly notable their name will come up and can be linked to somewhere in the actual body of the article. Just having a laundry list like this seems to be of no value to me and seems like it's primarily about people adding their names or names of their friends or people they really like for some reason. I don't see any objective criteria used to determine who gets put in that section and who doesn't. E.g., someone like David Luckham is very well known but most of the other names are not. I think we should just get rid of this section all together or if not we should at least have some criteria so that people aren't just adding vanity references to little known researchers. -- MadScientistX11 ( talk) 17:03, 10 September 2019 (UTC)
Recently, OpenAI and Meta have created AI models that automatically write proofs, using the Lean proof assistant/language. I think this could at least be mentioned in Applications, after the sentence on automated theorem provers being integrated with proof assistants.
https://openai.com/research/formal-math
https://ai.meta.com/blog/ai-math-theorem-proving/ RedrickSchu ( talk) 19:27, 14 March 2024 (UTC)
This is the
talk page for discussing improvements to the
Automated theorem proving article. This is not a forum for general discussion of the article's subject. |
Article policies
|
Find sources: Google ( books · news · scholar · free images · WP refs) · FENS · JSTOR · TWL |
This article is rated Start-class on Wikipedia's
content assessment scale. It is of interest to the following WikiProjects: | ||||||||||||||||||||||||||||
|
To-do list for Automated theorem proving:
|
there's a large (and important) class of techniques and provers that are barely even mentioned in this article, namely inductive theorem provers. i've searched, but cannot find an article on inductive theorem proving and the techniques in use in that field. should this article be expanded beyond first order theorem proving and model checking? 137.195.27.231 16:01, 29 October 2007 (UTC)
Should this article be merged with Computer-assisted proof? S Sepp 14:33, 21 January 2006 (UTC)
No: computer-assisted proofs also include interactive theorem provers which are, by def., not automated. Vincent Aravantinos ( talk) 18:33, 20 October 2011 (UTC)
I don't think it's a good idea to have this 'important people' list included. Such a list is almost always biased. E.g. in this list, there are not even all winners of the Herbrand award, the most prestigious award in the field, included.
I propose to delete this list.
Ulrich Furbach
If one is going to have an important people list, at least an effort should be made to make it reasonable. Nahaj 02:16:07, 2005-08-31 (UTC)
Better to have a history of automated theorem proving list. The "important people" will stand out without having to explicitly say they are important. —Preceding unsigned comment added by 94.173.19.247 ( talk) 10:48, 14 February 2011 (UTC)
I also think this list of important/notable people is not very appropriate. It doesn't fit the general style of Wikipedia (I cannot remember any other Wikipedia page where there is such a long list of people). It makes the article ugly (the list of people is almost as long as the sum of all other textual subsections in the beginning of the article). Finally, it also gives a bad impression of the Automated Deduction community (a visitor has the feeling that this community is more interested in promoting themselves and their colleagues by making a list of notable people, than in improving the quality of the article itself). A user who searches for ``automated deduction in an encyclopedia is mostly interested in a definition of automated deduction and in an overview of the existing techniques, not in seeing a long list of names that he has never seen before. It would suggest removing this list and creating a new textual section (or eventually a new separate article) called ``History of Automated Deduction. My knowledge of history of the field is not good enough (yet). Does any of you know someone with historical knowledge and willing to write this section? -- Ceilican ( talk) 07:05, 27 June 2011 (UTC)
Hi,
I'm not particularly happy with all of the recent edits. In particular, no serious ATP system enumerates all possible proof trees - all implement a refutation-complete calculus with redundancy criteria, and use a fair derivation strategy.
I also think that we are now moving to many details into the introduction.
Any comments?
-- Stephan Schulz 16:58, 12 September 2005 (UTC)
I dont know if this is the right place to ask, but i quite dont understand something: if the problem is recursively enumerable you can not always halt for sentences in the language. Then, how is it decidible? BTW, i belive this article also should be merged with automated reasoning. -- VyNiL 11:45, 14 August 2006 (UTC)
I don't know what the policy on spelling proper names is, but the theorem prover listed as "Vampire" is spelt "Vampyre" by the project itself (see http://www.cs.ucla.edu/~rupak/Vampyre/). Perhaps a spell-change is in order? —Preceding unsigned comment added by 74.130.8.62 ( talk • contribs)
Hi,
I'm missing some seemingly relevant references to Schmidhuber's universal self-referential Gödel-machines. They are `machines' (not `incarnated' as in the Turing Machine) that can rewrite themselves based on expected progress of a proof. I'm not an expert of this research in particular, but I think it is certainly relevant and a candidate for inclusion on this page.
A pointer for Schmidhubers work can be found here: http://www.idsia.ch/~juergen/goedelmachine.html
Regards, Erik de Bruijn —Preceding unsigned comment added by 85.147.200.8 ( talk) 17:51, 28 October 2007 (UTC)
Could someone that speaks Chinese possibly check the link to his home page to determine his institutional affiliation? (None is listed) Nahaj ( talk) 14:50, 14 August 2008 (UTC)
From the webpages of Wu Wenjun (Wu Wentsun) or some webpage concerned with him (such as the webpage of his affiliation),
http://sourcedb.amss.cas.cn/zw/zjrck/200907/t20090713_2065285.html http://www.mmrc.iss.ac.cn/~wtwu/ http://www.mmrc.iss.ac.cn/~wtwu/main.html http://www.cas.cn/ky/kjjl/gjzgkxjsj/2000n/wwj/ http://english.amss.cas.cn/pe/
his affiliation is:
Academy of Mathematics and Systems Science (AMSS) in the Chinese Academy of Sciences (CAS).
Liwenwei1980 ( talk) 16:57, 19 January 2016 (UTC)
In the section on "decidability" there is a reference to the "first-order theory of the natural numbers" used in Gödel's incompleteness theorem. I couldn't find a reference for this theory in itself. Is it just Peano arithmetic? If you know, please fix the link. —Preceding unsigned comment added by Ezrakilty ( talk • contribs) 13:36, 19 August 2008 (UTC)
The article should have a section on results from algebraic geometry on theorem proving, e.g. Characteristic set and Wu's method. A good introductory reference is Cox, Little and O'Shea's Ideals, Varieties and Algorithms. Akriasas ( talk) 12:32, 21 December 2008 (UTC)
I fail to see why deontic theorem proving is given a special section. Any modal logic "extends the first-order predicate calculus". Other than to showcase this one specific author, what does this section add to the page? (And if it is necessary, why wouldn't the same logic apply to any of categories of logics?) —Preceding unsigned comment added by 155.101.224.65 ( talk) 20:38, 20 May 2009 (UTC)
I agree and removed the section. Any non-standard logic should be added otherwise. Vincent Aravantinos ( talk) 18:30, 20 October 2011 (UTC)
I recently removed several interactive theorem provers ( diff) from the list, but someone added them back. In my opinion, those don't belong there, because
If there are no objections within the next couple of days, I will re-remove them. – Adrian Willenbücher ( talk) 05:26, 6 September 2010 (UTC)
The section confuses decidability and complexity issues, and needs to be rewritten.
The following changes should be made:
The section needs to define properly "decidability" - that is, giving a true/false (yes/no) answer to any question, and related concept of "semi-decidability" - that true (viz. false) can be answered, but not necessarily that false (viz. true) can be answered in all cases. Refer to Gödel incompleteness and the halting problem.
Note that the incompleteness theorem and halting problem show the non-existence of "universal" functions that can decide on all functions at all inputs. That does not imply the non-existence of functions which can decide about some functions and some inputs. In practice, one can decide many problems precisely by limiting the scope of functions or inputs.
Complexity classes are not related to decidability, so belong in a separate section. (Whether or not a problem is decidable is unrelated to how hard a problem is.) It's better to give a brief discussion about the difficulty (measured in time and space, i.e. memory usage) of solving problems and refer to a separate page about complexity classes. —Preceding unsigned comment added by 94.173.19.247 ( talk) 10:45, 14 February 2011 (UTC)
I think the authors of Jape are Bornat and Sufrin, not Neto. See the links. Rmkeller ( talk) 00:12, 28 February 2011 (UTC)
G. Gonthier might be added to the notable people. — Preceding unsigned comment added by 93.97.194.200 ( talk) 15:19, 10 June 2011 (UTC)
This article really needs a section on the history and development of the field. I came here looking for information on how it got started - and there's nothing on that. Noel (talk) 23:14, 1 September 2012 (UTC)
{{
citation}}
: URL–wikilink conflict (
help)). I'll see if I can cobble something together. --
Stephan Schulz (
talk) 00:36, 2 September 2012 (UTC)I've been working on various AI articles: inference engine, expert systems, etc. and needed to link to this page. BTW, this article is in great shape compared to what some of the AI articles were like. But I want to cast a strong vote to get rid of the "notable people" section. There is no such section on other articles that I've edited. We don't have a list of the notable inference engine or expert system people. If they are notable they are talked about and/or referenced in the article itself and if not then they aren't that notable. These lists are IMO just vanity or buddy lists where everyone adds themselves or their favorite researchers. Especially when they have lots of red links, I think the red links should just go immediately without further discussion but I'm not going to do it as I'm editing other articles now but just wanted to voice my opinion. RedDog ( talk) 14:29, 6 December 2013 (UTC)
"DPLL" is only a special algorithms for the propositional satisfiability problem (SAT), and a more appropriate link, under "Popular techniques", should be to /info/en/?search=Boolean_satisfiability_problem Oliver Kullmann ( talk) 17:11, 5 June 2016 (UTC)
Under "See also" it seems sensible to add a link to /info/en/?search=List_of_long_mathematical_proofs since this contains proofs found by ATP (especially SAT solving). — Preceding unsigned comment added by Oliver Kullmann ( talk • contribs) 17:13, 5 June 2016 (UTC)
I noticed that someone has added yet another person to this section that I've never heard of. I've edited several pages like this (e.g., Expert system Artificial intelligence Knowledge-based system Knowledge-based software assistant and none of them have a section like this. If someone is truly notable their name will come up and can be linked to somewhere in the actual body of the article. Just having a laundry list like this seems to be of no value to me and seems like it's primarily about people adding their names or names of their friends or people they really like for some reason. I don't see any objective criteria used to determine who gets put in that section and who doesn't. E.g., someone like David Luckham is very well known but most of the other names are not. I think we should just get rid of this section all together or if not we should at least have some criteria so that people aren't just adding vanity references to little known researchers. -- MadScientistX11 ( talk) 17:03, 10 September 2019 (UTC)
Recently, OpenAI and Meta have created AI models that automatically write proofs, using the Lean proof assistant/language. I think this could at least be mentioned in Applications, after the sentence on automated theorem provers being integrated with proof assistants.
https://openai.com/research/formal-math
https://ai.meta.com/blog/ai-math-theorem-proving/ RedrickSchu ( talk) 19:27, 14 March 2024 (UTC)