Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity

DOI10.1016/0168-0072(84)90029-0zbMath0594.03022OpenAlexW2026916148WikidataQ127957473 ScholiaQ127957473MaRDI QIDQ1076669

Daniele Mundici

Publication date: 1984

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(84)90029-0

zbMATH Keywords

decision procedurecircuit depthproof lengthdeterministic Turing machinelengths of interpolants

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Complexity of computation (including implicit computational complexity) (03D15) Interpolation, preservation, definability (03C40) Relative consistency and interpretations (03F25)

Related Items

Nondeterministic functions and the existence of optimal proof systems, Feasible Interpolation for QBF Resolution Calculi, On propositional definability, Some consequences of cryptographical conjectures for \(S_2^1\) and EF, Foundations of instance level updates in expressive description logics, Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, How to deal with unbelievable assertions, On the computational content of intuitionistic propositional proofs, Proof Complexity of Non-classical Logics

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On uniform circuit complexity
• Model theory.
• Riemann's hypothesis and tests for primality
• Two Familiar Transitive Closure Algorithms Which Admit No Polynomial Time, Sublinear Space Implementations
• Complexity problems in computational theory
• Every Prime Has a Succinct Certificate
• A lower bound for the complexity of Craig's interpolants in sentential logic