Questions tagged [proof-search]
Proof search problems in formal systems
4 questions
7
votes
0
answers
122
views
Are there any programming languages based on the method of analytic tableaux, aside from Fitting's Proflog?
The method of analytic tableaux [0] describes a process by which logical formulae, particularly of first order logic, can be determined to be valid or invalid. From the Wikipedia entry:
A tableau ...
- 109
4
votes
1
answer
165
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/...
- 3,217
10
votes
1
answer
268
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 ...
- 1,841
37
votes
2
answers
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 ...
- 3,773