Questions tagged [proof-search]

Proof search problems in formal systems

Filter by
Sorted by
Tagged with
4 votes
1 answer

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/...
MaiaVictor's user avatar
  • 3,137
10 votes
1 answer

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 ...
MassimoLauria's user avatar
37 votes
2 answers

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 ...
Joseph O'Rourke's user avatar