Jump to content

Talk:Propositional proof system

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

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

Gentzen without Cut in Picture

[edit]

According to the Cut Elimination Theorem (e.g. https://wiki.riteme.site/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)[reply]