The Stack Overflow podcast is back! Listen to an interview with our new CEO.

Questions tagged [proof-search]

Proof search problems in formal systems

Filter by
Sorted by
Tagged with
4
votes
1answer
126 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/...
10
votes
1answer
218 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 ...
35
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 ...