Formal Logic & Computation Systems

← Back to Domain-Specific Families

Abstractions about formal reasoning and computational systems, including logical inference rules, type theory, automata, rewriting systems, and nonmonotonic or temporal logics, spanning proof systems, decision problems and specification frameworks.

24 abstractions in this family — domain-specific abstractions that sit near one another in structural-signature space (k-means over structural-signature embeddings). Each is shown with its short description.

• Abstract state machine — A formal operational model in which each state is an arbitrary mathematical structure and guarded updates define discrete state transitions.
• And-inverter graph — A directed acyclic representation of Boolean logic using two-input AND nodes and optional edge inversions.
• Constructive dilemma — A valid propositional inference from two conditionals and a disjunction of their antecedents to the disjunction of their consequents.
• Default logic — A nonmonotonic formal logic that licenses defeasible conclusions when prerequisites hold and their justifications remain consistent with the evolving belief set.
• Deterministic automaton — An automaton whose current state and next input determine at most one successor state, eliminating branching choice from transition execution.
• Hidden algebra — An algebraic specification framework for stateful and concurrent systems that distinguishes visible data sorts from hidden state sorts and characterizes state by observable behavior.
• Independence of premise — A constructive-logical principle allowing an existential witness to be moved outside an implication when the premise does not contain that witness variable.
• Indeterminate form — A limiting-value pattern whose component limits do not by themselves determine the limit of their arithmetic combination.
• Interactive proof system — A protocol in which a computationally unbounded but untrusted prover exchanges messages with a resource-bounded randomized verifier to establish language membership with completeness and soundness guarantees.
• Metric temporal logic — A temporal logic whose modalities carry quantitative time intervals, allowing formulas to require that events occur within explicit deadlines or durations.
• Model elimination — A goal-directed automated theorem-proving calculus that extends resolution with ancestor links and a chain-based proof state.
• Monotonicity of entailment — A logical property whereby every conclusion entailed by a premise set remains entailed after any additional premises are added.
• Negation introduction — A rule of inference that derives not-P after assuming P and deriving a contradiction within a properly discharged subproof.
• One-sided limit — The limiting value approached by a function when its argument tends to a point only through values on one specified side.
• Ordinal collapsing function — A notation-building function that introduces symbols for very large ordinals and systematically collapses them into canonical notations for large countable ordinals.
• Paraconsistent logic — A logic whose consequence relation does not validate explosion, allowing some contradictions without every proposition becoming derivable.
• Postcondition — A predicate required to hold immediately after a program operation or specified code region completes normally.
• Qualification problem — The knowledge-representation problem that real-world actions have indefinitely many exceptional preconditions, making a complete list of conditions for their intended effects impossible to state in advance.
• Reachability problem — The decision problem asking whether allowed transitions can carry a system from a specified initial state to a target state.
• Rewriting — Rule-governed replacement of a subexpression by another expression within a formal object.
• Symbol (formal) — An abstract atomic item in a formal language whose concrete inscriptions or encodings are token instances rather than the symbol itself.
• Type theory — The family of formal systems that classify expressions by types and govern how typed terms may be formed, transformed and interpreted.
• Typing rule — A formal inference rule specifying how types of component expressions and contextual assumptions justify a type judgment for a larger syntactic construction.
• Well-founded semantics — A unique three-valued semantics for general logic programs that assigns each ground atom true, false or undefined.