Questions tagged [proof-search]
Proof search problems in formal systems
3
questions
36
votes
2answers
2k views
If P=NP, could we obtain proofs of Goldbach's Conjecture etc.?
This is a naive question, out of my expertise; apologies in advance.
Goldbach's Conjecture and many other unsolved questions in mathematics can be written
as short formulas in predicate calculus.
For ...
10
votes
1answer
241 views
A direct sum theorem for Resolution clause space complexity?
Resolution is a scheme to prove unsatisfiability of CNFs. A proof in resolution is a logical deduction of the empty clause for the initial clauses in of the CNF. In particular any initial clause can ...
4
votes
1answer
135 views
Is there a simple algorithm for proof search on CoC?
Given the usual Calculus of Constructions with an extra primitive, _, that stands for "attempt to fill this location in a way that type-checks", is there any simple/...
