534 articles
Computably enumerable set
A computably enumerable set, also called a recursively enumerable set, is a set whose members can be listed by an algorithm, including non-computable sets like the halting problem.
Computation
Computation is the execution of an algorithm that transforms an input into an output by fixed rules, the foundation of computer science and, on some accounts, a physical process.
Computation tree logic
Computation tree logic (CTL) is a branching-time temporal logic used in formal verification, checked by model checking in linear time, and expressively incomparable with LTL.
Computer-assisted proof
A computer-assisted proof is a mathematical proof in which a computer performs calculations or exhaustive case checks impractical to verify by hand, as in the 1976 four-color theorem proof.
Condensation algorithm
The Condensation algorithm, or Conditional Density Propagation, is a particle-filtering method for visual tracking in clutter, introduced by Michael Isard and Andrew Blake at Oxford in 1996.
Conditional proof
Conditional proof is a proof technique for deriving a conditional statement: one temporarily assumes A, derives B, and concludes A → B with the assumption discharged.
Conjecture
A conjecture is a mathematical statement proposed as true on the basis of observation or partial evidence but lacking a rigorous proof; a proof makes it a theorem.
Conjunctive normal form
Conjunctive normal form (CNF), also called clausal normal form, is a standard way of writing a propositional logic formula as a conjunction (AND) of clauses, each a disjunction of literals.
Conjunctive query
A conjunctive query is a database query expressed as a conjunction of relational atoms with existentially quantified variables, defined by Chandra and Merlin in 1977; evaluation is NP-complete.
Consistency
Consistency, also called logical consistency, is the syntactic property that no contradiction can be proven from a set of formulas; Gödel's completeness theorem shows every consistent first-order set is satisfiable.
Constructive modal logic
Constructive modal logic is modal logic built on an intuitionistic propositional base, adding necessity and possibility operators; its basic system is Constructive K, introduced in 2001.
Constructive proof
A constructive proof establishes that a mathematical object exists by giving an explicit construction of it, rejecting proof by contradiction and the law of excluded middle in general.
Constructive set theory
Constructive set theory is a family of axiomatic set theories, the best known being CZF, that provide foundations for mathematics based on intuitionistic logic without the law of excluded middle.
Constructivism (philosophy of mathematics)
Constructivism, also called constructive mathematics, is the philosophy of mathematics holding that existence requires a construction or proof, a view founded by L.E.J. Brouwer in 1907 that rejects the law of excluded middle.
Contraposition
Contraposition is the logical equivalence between a conditional and its contrapositive, where the contrapositive of P → Q is ¬Q → ¬P; the two are equivalent in classical logic.
Coq (proof assistant)
Coq, an interactive theorem prover developed at INRIA in France since 1984, underlies the verified CompCert C compiler and was renamed the Rocq Prover in 2025.
Countable set
A countable set is a set whose elements can be matched one-to-one with some or all of the natural numbers, a concept introduced by Georg Cantor.
Counterpart theory
Counterpart theory is David Lewis's 1968 semantic framework for modality: an individual exists in only one possible world, and its modal properties are evaluated through counterparts.
Covariance and contravariance (computer science)
Covariance and contravariance are properties of type constructors such as generic interfaces and arrays that describe how subtyping of their type arguments translates into subtyping of the constructed types.
Craig interpolation
Craig interpolation is a theorem of mathematical logic, proved by William Craig in 1957, stating that whenever one formula implies another, an intermediate formula in their shared vocabulary connects the two.
Curry–Howard correspondence
The Curry–Howard correspondence, also known as the propositions-as-types principle, identifies propositions with types and proofs with programs, so writing a program is constructing a proof.
Curry's paradox
Curry's paradox, or Löb's paradox, is a self-reference paradox from Haskell Curry's 1942 work that proves an arbitrary conclusion using only implication, without negation, unlike the liar paradox.
Cut elimination
Cut elimination is a proof theory theorem, proved by Gerhard Gentzen in 1935, stating that any sequent-calculus derivation using the cut rule can be transformed into a cut-free derivation.
Datalog
Datalog is a declarative logic-based query and rule language that allows recursive queries over relational data, developed in the early 1980s and now used in program analysis, security, and graph databases.
Davis–Putnam algorithm
The Davis–Putnam algorithm, introduced by Martin Davis and Hilary Putnam in 1960, is a complete decision procedure for propositional satisfiability that eliminates one variable at a time by resolution.
Decidability (logic)
Decidability in logic is the property of a formal system, theory, or class of questions for which an algorithm answers every instance with a yes or a no.
Decidability of first-order theories
Decidability of first-order theories asks which first-order theories have an algorithm deciding whether any sentence follows from them; Presburger arithmetic is decidable, first-order validity is not.
Deduction theorem
The deduction theorem is a metatheorem of logic stating that if ψ is derivable from Γ plus assumption φ, then φ → ψ is derivable from Γ alone.
Deep inference
Deep inference is a proof-theoretic methodology in which inference rules apply at any depth inside logical expressions, not just at the root of a formula.
Definable set
A definable set is a subset of a structure's universe picked out exactly by a first-order formula, and is a basic object of study in model theory.