Jump to content

Talk:Prover9

Page contents not supported in other languages.
From Wikipedia, the free encyclopedia

Merge of Otter into Prover9

[edit]

I'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)[reply]

  • 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)[reply]

Is the Socrates example incorrect?

[edit]

Is 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)[reply]