Talk:Prover9

Computing: Software / CompSci / Free and open-source software Low‑importance

This article is within the scope of WikiProject Computing, a collaborative effort to improve the coverage of computers, computing, and information technology on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.ComputingWikipedia:WikiProject ComputingTemplate:WikiProject ComputingComputing

Low

This article has been rated as Low-importance on the project's importance scale.

This article is supported by WikiProject Software (assessed as Low-importance).

This article is supported by WikiProject Computer science (assessed as Low-importance).

This article is supported by Free and open-source software (assessed as Low-importance).

Things you can help WikiProject Computer science with:

Here are some tasks awaiting attention:

Article requests :
- Requested articles/Applied arts and sciences/Computer science, computing, and Internet
Cleanup :
- Computer science articles needing attention
- Computer science articles needing expert attention
Copyedit :
- Computing
Expand :
- Computer science
Infobox :
- Computer science articles without infoboxes
Maintain :
- Timeline of computing 2020–present
Photo :
- Find pictures for the biographies of computer scientists (see List of computer scientists)
- Computing articles needing images
Stubs :
- Computer science stubs
Unreferenced :
- WikiProject Computer science/Unreferenced BLPs
Project-related :
- Tag all relevant articles in Category:Computer science and sub-categories with {{WikiProject Computer science}}

Merge of Otter into Prover9

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?

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]

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