A Survey of Automatability
summary
Defines automatability as finding a proof within time bounded by the shortest proof length and contrasts algorithms and lower bounds. Gives the trivial 2^s brute force and a width-based n^w search using size–width (w = O(√n log S)) to get subexponential time exp(O(√n log S)). Presents a tree-like recursion achieving n^{log s} and degree-based n^d bounds for algebraic systems. Shows crypto (one-way permutations) rules out weak automatability for strong systems, and Atserias–Müller proves P≠NP implies polynomial inapproximability of proof size; many gaps remain.
AI-written summary · about
chapters (9)
- 0:00Automatability in proof search
- 10:44Proof systems landscape
- 17:30Resolution automation bounds
- 27:03Tree-like resolution automation
- 33:10Algebraic automatability degrees
- 38:49Cryptographic lower bounds
- 48:48P vs NP resolution hardness
- 57:21Future automatability directions
- 1:02:27Q&A
related talks
58mA New Perspective on Commutativity in Verification
22mExecution Time Program Verification With Tight Bounds
05mWhy Performance in Programming Is Always a Problem
40mUtilizing Structure in Combinatorial Solving and Reasoning
52mNumbers, Logic, and Decidability for Cyber-Physical Systems
01h 05mVerifying Infinitely Many Programs at Once
21mMechanised Hypersafety Proofs about Structured Data
27mUnrealizability Logic