An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams

We prove an exponential lower bound on the size of proofs in the proof system operating with ordered binary decision diagrams introduced by Atserias, Kolaitis and Vardi [2]. In fact, the lower bound applies to semantic derivations operating with sets defined by OBDDs. We do not assume any particular...

Full description

Saved in:
Bibliographic Details
Published in:The Journal of symbolic logic 2008-03, Vol.73 (1), p.227-237
Main Author: Krajíček, Jan
Format: Article
Language:English
Subjects:
Boolean functions
Bounded arithmetic
constraint propagation
feasible interpolation
Geometric planes
Grammatical clauses
Interpolation
Logical proofs
Logical theorems
Mathematical monotonicity
OBDD
Proof complexity
Refutation
Semantics
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We prove an exponential lower bound on the size of proofs in the proof system operating with ordered binary decision diagrams introduced by Atserias, Kolaitis and Vardi [2]. In fact, the lower bound applies to semantic derivations operating with sets defined by OBDDs. We do not assume any particular format of proofs or ordering of variables, the hard formulas are in CNF. We utilize (somewhat indirectly) feasible interpolation. We define a proof system combining resolution and the OBDD proof system.
ISSN:0022-4812
1943-5886
DOI:10.2178/jsl/1208358751