Talk:Prover9
 | This article is rated Start-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | ||||||||||||||||||||||||||
| |||||||||||||||||||||||||||
.svg){kind=logo}
Merge of Otter into Prover9
editI'm sorry to be so late, but I only now noted the merge. As far as I am concerned, this is a very bad idea. Otter is/was the first of the theorem provers in the modern refutation/saturation style combining rewriting and resolution with an efficient implementation based on term indexing. It is a milestone of the field. The redirect feels a bit like redirecting Douglas DC-3 to McDonnell_Douglas_DC-10#Development, or to redirect World War I to World_War_II#Background. Yes, Prover9 is both a better theorem prover and a more modern system. But it does not come close the the influence Otter had on the field...--Stephan Schulz (talk) 22:11, 5 June 2017 (UTC)
- This seems to be a controversial merge. It also does not seem to have proper attributions per WP:FMERGE/WP:SMERGE. I am therefore going to back it out as I am not prepared add content/references to the articles as they stand. There may be a case for re-proposing a possibly controversial merge under discussion (which might be in the other direction, or it may be elsewhere). Thankyou.Djm-leighpark (talk) 07:51, 11 November 2018 (UTC)
Is the Socrates example incorrect?
editIs not the conclusion (-mortal(socrates)) wrong for the Socrates example?
While I am not conversant with Prover9, to be consistent with the other bits, this seems to read "Socrates is not mortal", but that's exactly the opposite of the correct conclusion.