Verifying that P is not equal to NP using a theorem prover
2013 (English)Report (Other academic)
The problem of computing whether any formula in propositional logic is satisfiable is not in P . Therefore, P is not equal to NP . In the first- order theory B, axiomatizing Turing’s theory of computing, three versions of the proofs are presented. First, an informal (conceptual) proof about formal proofs. Second, a more formal proof in Hilbert’s proof theory. Third, a formal proof in Hilbert’s proof theory, using a theorem prover.
Place, publisher, year, edition, pages
Uppsala: Department of Informatics and Media , 2013. , 36 p.
Research report / Uppsala University, Department of Information Science, ISSN 1403-7572 ; 2013:2
P is not equal to NP, theorem prover
Information Systems, Social aspects
Research subject Computer Systems Sciences
IdentifiersURN: urn:nbn:se:uu:diva-207452OAI: oai:DiVA.org:uu-207452DiVA: diva2:648241