Talk:Propositional proof system
 | This article is rated Start-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | ||||||||||
| |||||||||||
Header
The set of propositional tautologies is a coNP-complete. Sets do not have a computational complexity, but algorithms do. I would suggest to remove the whole paragraph because what it says is not explained and what is explained is not true.
- For example, P is the class of sets that can be decided in polynomial time. — Carl (CBM · talk) 21:33, 2 December 2012 (UTC)
Gentzen without Cut in Picture
According to the Cut Elimination Theorem (e.g. https://en.wikipedia.org/wiki/Cut-elimination_theorem) Gentzen with and without cut have the same effect regarding the polynomial proof of tautologies. So I think that Gentzen without cut should be replaced above below Gentzen with Cut. --Alina Morad (talk) 20:51, 5 January 2020 (UTC)