NP Satisfiability for Arrays as Powers
summary
Claim: the existential satisfiability problem for product (power) structures with an equicardinality predicate is in NP. Proof uses a semantic, model-theoretic reduction that guesses a DNF disjunct, issues a polynomial number of queries to the component theory, and replicates component solutions to meet cardinality requirements. Result extends combinatory array logic to handle cardinality constraints via QF‑BAPA, stays component‑theory agnostic, and preserves existential satisfiability in NP.
AI-written summary · about
chapters (6)
related talks
26mMechanical Proofs in an Array-Combinator Language
01h 08mType Arithmetic and the Yoneda Lemma
55mNon-commutative Computation
01h 04mExplicit SoS Lower Bounds from (Small-Set) High Dimensional Expanders
14mAdequacy for Algebraic Effects Revisited
21mBlack-box Constructive Proofs are Unavoidable
30mRelatively Complete Verification of Probabilistic Programs
14mOn Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs