44 articles
Proof-theoretic semantics
Proof-theoretic semantics is an alternative to model-theoretic semantics that explains the meaning of logical constants in terms of the inference rules governing their behavior in proofs.
Propositional proof system
A propositional proof system is any polynomial-time computable function whose range is exactly the propositional tautologies, the abstract definition by Cook and Reckhow in 1979 that founded proof complexity.
Reflection principles
A reflection principle is a formal schema asserting that a theory is sound, meaning every sentence it proves is true; it extends theories beyond what they can prove about themselves.
Relevance logic
Relevance logic, also known as relevant logic, is a family of non-classical logics developed to avoid the paradoxes of material and strict implication by requiring content connection.
Reverse mathematics
Reverse mathematics, also known as reverse math, is a program in mathematical logic founded by Harvey Friedman in 1974 that determines which axioms are necessary to prove theorems of ordinary mathematics.
Rule of inference
A rule of inference, also called an inference rule, is a syntactic schema in logic that licenses a proof step from premises to a conclusion.
Separation logic
Separation logic is an extension of Hoare logic for verifying programs that manipulate heap-allocated pointer structures, using a separating conjunction for disjoint memory; it won the 2016 Gödel Prize.
Sequent
A sequent is an expression Γ ⇒ Δ in a formal logic, read as yielding the right side from the left, introduced by Gerhard Gentzen in his 1934/35 dissertation.
Sequent calculus
The sequent calculus, or Gentzen calculus, is a formal proof system for logic introduced by Gerhard Gentzen in 1934, a central tool of structural proof theory.
Soundness
Soundness (logical soundness) is the property of a proof system that proves only what is semantically valid: derivable conclusions hold in every model of the premises.
Structural induction
Structural induction is a proof technique that establishes a property for all elements of an inductively defined data type, such as lists, trees, or formulae.
Substructural logic
Substructural logic is a family of non-classical logics lacking one or more structural rules of classical logic, including relevant logics, the Lambek calculus, and linear logic.
Takeuti's conjecture
Takeuti's conjecture, also called Takeuti's fundamental conjecture, is the claim that Gentzen's cut-elimination theorem extends from first-order logic to simple type theory, formulated by Gaisi Takeuti in 1953.
Unification (computer science)
Unification in computer science is the algorithmic problem of finding a substitution making two logical expressions identical, introduced by Robinson in 1965 for resolution theorem proving.