Conjectura
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Conjunctive query

ConjunctiveQueryabbrev

A conjunctive query is the select–project–join fragment: a set of atoms that must all be matched by one assignment of variables to values. Query containment and evaluation for this fragment are the two problems most of database theory is about, and both are NP-complete.

abbrev ConjunctiveQuery (Var Attr Val : Type*) :=
  Set (RelationInstance Attr Val × (Attr → Var))

import Conjectura.Defs.ComputerScience.Databases.ConjunctiveQuery · maintainer — open · raw source

Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors

Full credits