Add to ORKGThe questions "What is a proof?" and "When are two proofs the same?" are fundamental for proof theory. But for the most prominent logic, Boolean (or classical) propositional logic, we still have no satisfactory answers. This is embarrassing not only for proof theory itself, but also for computer science, where classical propositional logic plays a major role in automated reasoning and logic programming. Also the design and verification of hardware is based on classical Boolean logic. Every area in which proof search is employed can benefit from a better understanding of the concept of proof in classical logic, and the famous NP-versus-coNP problem can be reduced to the question whether there is a short (i.e., polynomial size) proof for ever...
