Talk: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)Reply

Should this article be merged with Computer-assisted proof? S Sepp 14:33, 21 January 2006 (UTC)Reply

No: computer-assisted proofs also include interactive theorem provers which are, by def., not automated. Vincent Aravantinos (talk) 18:33, 20 October 2011 (UTC)Reply

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

I disagree. If you think it's biased, you can add other names who take an opposing viewpoint. Michael Hardy 20:19, 2 Dec 2004 (UTC)

I tend to agree with Uli. It's not that the list is biased, it's more that automated theorem proving is a large, diverse field, and hence the list is always bound to be incomplete. I could easily expand the size of the list by two, but very few of the people would be known outside the field. Moreover, currently, only one of the important persons has a Wikipedia entry of his own - this seems to indicate that there is not that much interest in the list or the people. Finally, many people are hard to classify - is e.g. Donald Knuth important in theorem proving? --Stephan Schulz 22:30, 2 Dec 2004 (UTC)

If one is going to have it, at least an effort should be made to make it have the main players. I've added Geoff Sutcliffe, given TPTP is mentioned... Nahaj 02:16:07, 2005-08-31 (UTC)

Couldn't the same arguments be made about the list of theorem provers that is being made about the list of people? Nahaj 02:16:07, 2005-08-31 (UTC)

The section "Availiable Theorem provers" has a lot of dead links. I would expect that if they are actually availiable, there should be a place from which they are availiable. My personal opinion is that the section should either be renamed "Known theorem provers" (second choice), or (my first choice) we should link to where they are availiable. Nahaj 11:22:10, 2005-09-09 (UTC)

I personally think that now that many of the entries point to the people doing current research, that the list is starting to be as useful as the list of current systems. (and thanks, Stephan, for useful additions.) Nahaj 02:23:05, 2005-09-04 (UTC)

I still the the demarkation problem, but as long as we have the list, it should at least be useful...--Stephan Schulz 09:04, 4 September 2005 (UTC)Reply

Since we are at the point where most folk are there with some sort of claim to fame, and meaningfull links, maybe it is time to remove the people that have neither? I don't know where the demarkation should be either... but "important people" without any listed accomplishments, and no pointer to anything meantingfull seems the place to cut to me. They can always be added again if someone wants to say why they are important, or wants to provide pointers to something that does. Nahaj 21:14:11, 2005-09-05 (UTC)

I don't have time to check all, but there are several on the list who have made important contributions. I've added info to some, and will do some more soon. --Stephan Schulz 01:07, 6 September 2005 (UTC)Reply

It would be nice also, in my opinion, to make link to actual citations for some folk. If a claim to fame is they won a prize, then a link to a list of the prize winners would be appropriate. If they are authors, a link to some place that lists their publications (such as their home pages) seems also appropriate. (Just my rambling) Nahaj 02:42:04, 2005-09-08 (UTC)

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)

I've added Geoff Sutcliffe, given that his baby, TPTP, is mentioned and important in my opinion. Nahaj 02:16:07, 2005-08-31 (UTC)

Fleshed in some reasons for some the "important people" that I recognised... some of the rest I've never heard of at all, or don't know enough about to comment on. Since many of ones that I did recognise were at places recognised as having Automated Reasoning connections, so I pointed the names at their personal web pages there, instead of to non-existant or stubbed wikipedia pages. That way people can check their accomplishments directly themselves. My apologies in advance to some that have accomplishments as long as my arm that I tried to summarize in one sentence. Nahaj 02:25:52, 2005-09-02 (UTC)

The Alan Robinson entry currently points to a wikipedia page for some other person named Alan Robinson I left it since I don't have a correct place to point it. Nahaj 02:33:13, 2005-09-02 (UTC)

Looks like someone "fixed" it... Note that The inventor of Resolution is properly John Alan Robinson, (publishing as J. Alan Robinson), not plain Alan Robinson as the link says. This can be checked by actually looking at the "author" line of the pager, or looking at almost any of the online citation services. He is emeritus at Syracuse. [Yes the original affiliation was wrong, he is not at Manchester, that is a different Alan Robinson (the mathematician) Nahaj 21:09:38, 2005-09-02 (UTC)

"Someone" is me. My priority was the get the wrong link out. Alan publishes both as J. Alan Robinson and as Alan Robinson (see e.g. the Handbook of Automated Reasoning). Since an article on him does not yet exist, we are free to create either one. But by what name is he best known? I have no strong feeling either way....--Stephan Schulz 22:00, 2 September 2005 (UTC)Reply

I'm not sure why the wrong link was a priority... it has been wrong for a long time. I think that my priority would personally be filling in why some of the alleged important people are considered so. Nahaj 01:25:38, 2005-09-03 (UTC)

His name is John Alan Robinson, although you are right that he publishes both J. Alan Robinson and as Alan Robinson (Notice the historic trend...). I would have thought it best to have his page use his actual name, and mention others he publishes under. (And I think that the full name is a better disambiguator than what's there now, since I believe that there is more than one computer scientist named Alan Robinson.) Nahaj 01:25:38, 2005-09-03 (UTC)

I might also argue the point of whether "inventor of resolution" is historically proper. Resolution is implicit in Carew Meredith's Condensed Detachment work in the early 1950's. (Under appreciated then, but valuable now.) Nahaj 01:25:38, 2005-09-03 (UTC)

Added Brandon Fitelson, linked to his home page. I consider his work on shortest axiom bases important both as significant automated logic work, and for the effect it has had on convincing new folk that there is still fun to be had in logic. I still have to wonder about who some of the remaining uncredited alleged "important people" are on that page. Nahaj 15:28:01, 2005-09-03 (UTC)

(Bill McCune -> William McCune) Making it the same way his home page has it. Nahaj 21:14:11, 2005-09-05 (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)Reply

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)Reply

Suggestion: instead of a list of people, how about an article entitled Timeline of automated theorem proving, (something like Timeline of artificial intelligence). If these people are sufficiently notable, then they'll appear in the timeline. pgr94 (talk) 10:40, 27 June 2011 (UTC)Reply

Yes. The timeline is a good alternative to the "history of automated deduction" that I had suggested. Again we need someone with historical knowledge of the field. — Preceding unsigned comment added by Ceilican (talk • contribs) 17:10, 30 June 2011 (UTC)Reply

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)Reply

I generally agree. As I read it, it miss-characterizes how Theorem Provers work (enumeration of proof trees), and uses this as a premise to make an argument (people will need to help them out) that seems unreated to anything there. And I totally agree with your second paragraph. Nahaj 00:24:42, 2005-09-13 (UTC)

Ok, I'll take most of this out. If anywhere, it should go into First-order logic, not here. --Stephan Schulz 20:40, 13 September 2005 (UTC)Reply

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)Reply

No, if it is recursively enumerable there is an algorithm that always holds for sentences in the language (i.e. in this case valid theorems, not all formulae!). It cannot hold on all sentences (and in first-order theorem proving we cannot guarantee termination for non-theorems).

With regard to the merge: Automated reasoning is a superfield of automated theorem proving, but both are easily large enough for individual articles. --Stephan Schulz 16:12, 14 August 2006 (UTC)Reply

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)

this seems to me to be a different theorem prover albeit with a similar name.

there doesn't seem to be any doubt that the correct spelling is "vampire" if you do a google search on "vampire theorem prover manchester"

81.77.83.84 19:18, 29 October 2007 (UTC)Reply

Yes, that's a different system. --Stephan Schulz 19:51, 29 October 2007 (UTC)Reply

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)Reply

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)Reply

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)Reply

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)Reply

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)Reply

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)Reply

I agree and removed the section. Any non-standard logic should be added otherwise. Vincent Aravantinos (talk) 18:30, 20 October 2011 (UTC)Reply

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

• they are interactive, not completely automated, so they don't belong here.
• ITPs should listed in their own article.

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)Reply

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)Reply

I think the authors of Jape are Bornat and Sufrin, not Neto. See the links. Rmkeller (talk) 00:12, 28 February 2011 (UTC)Reply

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)Reply

Benjamin Werner might also be added. — Preceding unsigned comment added by 93.97.194.200 (talk) 15:21, 10 June 2011 (UTC)Reply

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)Reply

Good point. I have some overview knowledge, but mostly only primary sources. However, I have a (unread so far) copy of Davis, Martin (2001), "The Early History of Automated Deduction", in Robinson, Alan; Voronkov, Andrei (eds.), [[Handbook of Automated Reasoning]], vol. 1, Elsevier {{citation}}: URL–wikilink conflict (help)). I'll see if I can cobble something together. --Stephan Schulz (talk) 00:36, 2 September 2012 (UTC)Reply

There also is Bibel, Wolfgang (2007). "Early History and Perspectives of Automated Deduction" (PDF). KI 2007. LNAI (4667). Springer: 2–18. Retrieved 2 September 2012.. --Stephan Schulz (talk) 21:00, 2 September 2012 (UTC)Reply

And another interesting source: MacKenzie, Donald (1995). "The automation of proof: A historical and sociological exploration". IEEE Annals of the History of Computing. 17 (3): 7–29.. --Stephan Schulz (talk) 23:47, 26 September 2012 (UTC)Reply

And another: Loveland, Donald W. (1983). "Automated Theorem Proving - A Quarter-Century Review". In Woodrow W. Bledsoe, Donald W. Loveland (ed.). Automated Theorem Proving: After 25 Years. American Mathematical Society. pp. 1–46. Retrieved 4 May 2013. --Stephan Schulz (talk) 12:44, 4 May 2013 (UTC)Reply

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)Reply

"DPLL" is only a special algorithms for the propositional satisfiability problem (SAT), and a more appropriate link, under "Popular techniques", should be to https://en.wikipedia.org/wiki/Boolean_satisfiability_problem Oliver Kullmann (talk) 17:11, 5 June 2016 (UTC)Reply

Under "See also" it seems sensible to add a link to https://en.wikipedia.org/wiki/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)Reply

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)Reply

I agree. Would delete the section. And, if necessary, incorporate the works of the scientists. --ZaaraTE (talk) 17:20, 10 September 2019 (UTC)Reply

I also agree. Saung Tadashi (talk) 21:17, 10 September 2019 (UTC)Reply

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)Reply