Talk:Automated theorem proving

From Wikipedia, the free encyclopedia

WikiProject Mathematics
Mathematics Portal
This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.
Mathematics rating: Start Class Low Priority  Field: Foundations, logic, and set theory

Contents

[edit] inductive 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)

[edit] merge?

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

[edit] important people list

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

[edit] 12 September 2005 edits by 83.250.196.61

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


[edit] Question...

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)

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)

[edit] vampire / vampyre

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)
Yes, that's a different system. --Stephan Schulz 19:51, 29 October 2007 (UTC)

[edit] Schmidhuber missing

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)