2026-07-30T16:22:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12470 2024-03-06T10:50:13Z ddc:004 open_access

Feasible Interpolation for Polynomial Calculus and Sums-Of-Squares Hakoniemi, Tuomas Proof Complexity Feasible Interpolation Sums-of-Squares Polynomial Calculus We prove that both Polynomial Calculus and Sums-of-Squares proof systems admit a strong form of feasible interpolation property for sets of polynomial equality constraints. Precisely, given two sets P(x,z) and Q(y,z) of equality constraints, a refutation Π of P(x,z) ∪ Q(y,z), and any assignment a to the variables z, one can find a refutation of P(x,a) or a refutation of Q(y,a) in time polynomial in the length of the bit-string encoding the refutation Π. For Sums-of-Squares we rely on the use of Boolean axioms, but for Polynomial Calculus we do not assume their presence. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Tuomas Hakoniemi 2020 Is Part Of LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2020.63 urn:nbn:de:0030-drops-124707 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.63 eng https://creativecommons.org/licenses/by/3.0/legalcode