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.
128.186.121.77 (talk) 16:17, 4 October 2019 (UTC)
- All formulae from the goals section will be automatically negated in the preprocessing step. The prover then tries to refute the conjunction of all the formulae, i.e., show that they cannot be satisfied. This will prove the original statement CONJUNCTION(all formulae listed as assumptions) IMPLIES DISJUNCTION(formulas listed as goals). If there is only one goal (the usual case), then the refutation shows that the conjunction of all assumptions implies the goal. Therefore -mortal(socrates), which indeed should be interpreted as socrates is not mortal ("Assume Socrates were immortal"), is correct as displayed on the page. 128.131.42.210 (talk) 18:24, 3 December 2024 (UTC)