Conjunctive query containment is NP-complete
Lax420092.ContainmentNPComplete · concepts/Lax420092/ContainmentNPComplete.lean · lax-420092
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Boolean conjunctive query containment is NP-complete in the sense of the NP core: it reduces to evaluation by the Chandra–Merlin theorem, evaluating the right query in the canonical database of the left one, and evaluation reduces to it, a database being a variable-free query. This is the containment half of Chandra and Merlin (1977).
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax904597.Problems |
| 2 | import Lax904597.Interpretations |
| 3 | import Lax904597.Classes |
| 4 | import Lax799700.Problems |
| 5 | import Lax420092.QueryDatabases |
| 6 | import Lax420092.Evaluation |
| 7 | import Lax420092.QueryPairs |
| 8 | import Lax420092.PackagedInstances |
| 9 | |
| 10 | /-! |
| 11 | --- |
| 12 | title: Conjunctive query containment is NP-complete |
| 13 | type: theorem |
| 14 | --- |
| 15 | Boolean conjunctive query containment is NP-complete in the sense of the NP |
| 16 | core: it reduces to evaluation by the Chandra–Merlin theorem, evaluating the |
| 17 | right query in the canonical database of the left one, and evaluation |
| 18 | reduces to it, a database being a variable-free query. This is the |
| 19 | containment half of Chandra and Merlin (1977). |
| 20 | -/ |
| 21 | |
| 22 | namespace Lax420092.ContainmentNPComplete |
| 23 | |
| 24 | open FirstOrder FirstOrder.Language |
| 25 | open Lax904597.Problems Lax904597.Interpretations Lax904597.Classes Lax799700.Problems |
| 26 | open Lax420092.QueryDatabases Lax420092.Evaluation Lax420092.QueryPairs Lax420092.PackagedInstances |
| 27 | |
| 28 | /-- CQContainment is NP-complete. -/ |
| 29 | axiom cqContainment_NP_complete : NP.Complete CQContainment |
| 30 | |
| 31 | end Lax420092.ContainmentNPComplete |
| 32 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments