Concept wiki
Terms used across Axeyum
The 75 articles in this index define the logic, solver, computer algebra, proof-checking, and formal-library terms used on the site. Each article includes an example, a boundary, and links to the lessons that teach it.
75 concepts
Subject
Reasoning foundations
- Claim A statement presented as true or false.
- Constraint A rule that restricts which values or states are allowed.
- Decision problem A problem whose answer is one of a fixed set of outcomes, usually yes or no.
- Evidence Data that another procedure can use to check a result.
- Formalization A precise representation of a statement in a defined language.
- Solver A program that searches for values satisfying a formal problem.
- Soundness The property that accepted results are valid under the stated semantics.
- Trusted computing base
TCBThe code and assumptions that must be correct for a result to be valid.
Subject
Boolean logic
- Assignment A choice of values for a formula's free variables.
- Boolean formula An expression built from Boolean variables and logical connectives.
- Boolean value One of the two values true and false.
- Clause A disjunction of literals.
- Conjunctive normal form
CNFA Boolean formula written as an and of clauses. - Literal A Boolean variable or its negation.
- Logical connective An operation that combines or changes truth values.
- Model An interpretation that makes every asserted constraint true.
- Proposition A statement with a truth value.
- Satisfiable Having at least one assignment that makes all constraints true.
- Unsatisfiable Having no assignment that makes all constraints true.
- Variable A named place whose value is supplied by an assignment or binder.
Subject
SAT solving
- And-inverter graph
AIGA graph representation built from and nodes and complemented edges. - Backtracking Returning to an earlier search state after a conflict.
- Boolean satisfiability
SATThe problem of deciding whether a Boolean formula has a satisfying assignment. - Conflict A clause made false by the current partial assignment.
- Conflict-driven clause learning
CDCLA SAT search method that learns clauses from conflicts. - DRAT proof
DRATA common SAT proof format based on redundant clause additions. - Learned clause A new clause derived from a conflict and added to the SAT problem.
- Proof certificate A checkable record supporting a solver's result.
- SAT search decision A provisional variable assignment chosen when propagation cannot continue.
- Unit propagation Assigning the only remaining value that can keep a clause true.
- Unknown result A report that the solver did not decide the query.
Subject
SMT solving
- Bit-blasting Translating fixed-width operations into Boolean constraints on individual bits.
- Bit-vector A fixed-width sequence of bits with precisely defined operations.
- Logic fragment A named restriction on the terms allowed in a solver query.
- Model replay Evaluating a returned model against the original query.
- QF_BV The quantifier-free SMT-LIB logic for fixed-width bit-vectors.
- Rewriting Replacing a term with another term that preserves its meaning under stated rules.
- Satisfiability modulo theories
SMTSatisfiability with values and operations from stated theories. - SMT-LIB A standard language and benchmark format for SMT solvers.
- Sort The declared kind of value an SMT term may have.
- Theory A set of meanings and laws for a class of values and operations.
- Theory solver A procedure that decides or propagates constraints in one formal theory.
Subject
Computer algebra
- Computer algebra system
CASA program that performs exact operations on symbolic mathematical expressions. - Exact arithmetic Computation that preserves an exact mathematical value instead of rounding it.
- Operation-specific checker A checker written for the evidence returned by one class of computation.
- Simplification Transforming an expression into a chosen simpler form while preserving meaning.
- Symbolic differentiation Computing a derivative by applying exact rules to an expression.
- Symbolic expression An expression that retains variables and mathematical operations.
- Symbolic integration Finding an expression whose derivative matches a given expression.
Subject
Proof checking
- Definitional equality Equality determined by the core computation rules rather than by a separate theorem.
- Dependent type A type that can mention a value.
- Elaborator A program that turns convenient source syntax into explicit terms for a kernel.
- Formal proof A proof expressed in a language whose steps can be checked mechanically.
- Inductive type A type generated by a declared set of constructors.
- Proof kernel The small part of a proof system that checks declarations and proof terms.
- Proof term A term whose type is the proposition it proves.
- Recursor The elimination rule used to define functions or proofs by cases on an inductive value.
- Reduction Computing a term according to the core language's evaluation rules.
- Tactic A procedure that constructs or refines a proof.
- Type theory A formal foundation in which terms have types and propositions can be types.
- Universe A level used to organize types without placing every type inside itself.
- Weak head normal form
WHNFA term reduced enough to expose its outermost form.
Subject
Formal knowledge
- Axiom A proposition accepted without a proof term in the current formal environment.
- Axiom footprint The set of trusted axioms reached by a declaration's dependencies.
- Axiom of choice A principle that selects an element from each set in a family of nonempty sets.
- Classical logic Logic that permits principles such as excluded middle for every proposition.
- Constructive mathematics Mathematics that requires explicit constructions or evidence for existence claims.
- Dependency graph A graph that records which facts or declarations rely on which others.
- Fact ledger Axeyum's typed collection of claims, evidence, assumptions, and dependencies.
- Formal library A maintained collection of definitions, theorems, proofs, and their relationships.
- Law of excluded middle The principle that P or not P holds for every proposition P.
- Propositional extensionality The principle that logically equivalent propositions are equal as propositions.
- Provenance Information about where a statement or artifact came from and how it was produced.
- Quotient soundness A trusted rule that identifies quotient representatives related by the chosen relation.
- Theorem A proposition accepted with a proof under stated assumptions.
No concepts match both filters.