Appendix B
Glossary
Forgot what a countermodel is, or how a term differs from a formula? Here’s a quick reference to the main concepts from the book. The definitions follow our use of the terms; where a choice of logic matters, we’ve said which one we mean.
You can search the terms and their definitions below. For symbols, see the Appendix A · notation table. In the chapters, marked terms show a short definition on hover or keyboard focus; clicking opens the corresponding entry here in a new tab.
Abstract syntax tree (AST)
A tree representing the structure of an expression while omitting grammatical details such as brackets.
Abstraction
Leaving out features of a reasoning scenario that do not matter for the question we are studying.
Action
An operation an agent can perform in the world. An action atom states that a particular action occurs at a particular time.
Adder
A circuit that computes addition on numbers in binary representation.
Affirming a disjunct
The invalid pattern from inclusive A ∨ B and A to ¬B; both disjuncts may be true.
Affirming the consequent
The classically invalid pattern from A → B and B to A.
Agenda
A collection of items awaiting processing by a reasoning procedure.
Algorithm
A precise, step-by-step procedure that takes an input and produces an output in finitely many steps.
Algorithm correctness
An algorithm produces the specified result on its intended inputs; total correctness also requires termination.
Algorithmic undecidability
The absence of an algorithm that terminates with the correct yes-or-no answer on every allowed input to a problem.
Alpha-renaming
Changing a bound variable and its bound occurrences to a fresh variable without changing meaning.
Alphabet
A set of symbols from which strings of a formal language are formed.
Ambiguity
An expression is ambiguous if it has more than one possible reading.
Ambiguous grammar
A grammar that generates at least one expression with more than one grammatical structure.
Antecedent
The if-part A of a conditional A → B.
Arity
The number of argument places of a function or predicate symbol.
Assignment prescription
A list [x₁ ↦ d₁, …, xₙ ↦ dₙ] specifying values for distinct variables. When these include every free variable of a formula, they suffice to determine its satisfaction.
Assignment variant
The assignment v[x ↦ d] sends x to d and agrees with v on every other variable.
Atomic diagram
The set of all atomic and negated atomic sentences true in a model after adding a name for every domain object.
Automated theorem prover
Software that searches for formal proofs of specified claims from given assumptions.
Auxiliary symbol
A symbol used to mark the grammatical structure of an expression, such as a bracket in propositional logic.
Axiom
A formula accepted as a starting point in a proof system or theory.
Backus–Naur Form (BNF)
Notation for grammar rules, using alternatives to specify how expressions can be built.
Backward chaining
Starting with a goal and searching for rules whose premises would establish it.
Base case
A case handled directly by a recursive definition or procedure, without another recursive call.
Belief revision
Changing the propositions we accept when we receive new information, including information that conflicts with earlier beliefs.
Biconditional
A connective written ↔ and read “if and only if”; in classical logic it is true when its two parts have the same truth-value.
Binary representation
Positional notation with digits 0 and 1, in which position n, counted from the right starting at 0, has place value 2 to the power n.
Bit
A binary digit: either 0 or 1.
Bivalence
The assumption that each formula has exactly one of the two Boolean truth-values, true or false.
Boolean evaluation
The extension of a Boolean valuation to all formulas of a propositional language: it keeps the assigned values of variables and interprets ¬, ∧ and ∨ using NOT, AND and OR, respectively.
Boolean function
A function that takes a fixed number of Boolean values, 0 and 1, as inputs and returns one Boolean value.
Boolean identity
An equation between Boolean expressions that holds for every assignment of Boolean values to its variables.
Boolean model
A Boolean valuation of the propositional variables of a language, used to represent a possible reasoning situation. It is a model of a formula when that formula has value 1 under the valuation.
Boolean satisfiability problem
The problem of deciding whether a given propositional formula or finite set of propositional formulas is satisfiable.
Boolean valuation
A function assigning precisely one Boolean value to every propositional variable of a language.
Boolean value
One of the two values 0 and 1. In logic, they represent false and true, respectively. The Boolean value v(A) of a formula A under a valuation v is determined by the values of its variables and the Boolean functions interpreting its connectives.
Bound variable
An occurrence of a variable governed by the nearest enclosing quantifier for that variable.
Bounded SAT planning
Encoding an initial state, a goal, and permitted transitions over a fixed finite horizon as a propositional formula whose satisfying assignments describe plans.
Breadth-first search
A search that explores every possibility at one depth before moving to the next depth.
Canonical normal form
For a fixed ordered variable list, the canonical DNF lists the full terms describing true rows; the canonical CNF lists the full clauses excluding false rows. Components follow binary row order and literals follow variable order.
Cardinality
The number of elements of a set.
Classical logic
The logical framework used in our Boolean and FOL chapters, with bivalent semantics and classical inference principles.
Clause
A disjunctive clause is a disjunction of literals. A conjunctive clause is a conjunction of literals. A single literal counts as either. In resolution, an unqualified clause means a disjunctive clause.
Combinatorial explosion
Rapid growth in the number of combinations to consider as the number of choices increases.
Complement
The complement W ∖ S contains the objects in a specified universe W that do not belong to S.
Complementary literals
A pair consisting of a propositional variable and its negation.
Completeness
A proof system is complete if every semantic consequence can be derived in it.
Conclusion
The statement being inferred from the premises of an inference.
Conclusion indicator
A word or phrase, such as “therefore”, that signals the conclusion of an inference.
Conditional
An if-then statement. In classical logic, A→B is false exactly when A is true and B is false.
Conditional probability
The probability of one claim given another. Formally, Pr(A given B)=Pr(A∧B)/Pr(B), provided Pr(B)>0.
Conjunction
An and-formula. Classical A∧B is true exactly when both conjuncts are true.
Conjunctive clause
A conjunction of literals, also called a term. A single literal counts as a conjunctive clause.
Conjunctive normal form
A conjunction of disjunctions of literals, abbreviated CNF.
Consequent
The then-part B of a conditional A → B.
Consistency
A theory is consistent if it does not prove both a statement and its negation.
Constant
A name in a formal language; in an FOL model it denotes an object in the domain.
Constructor
An operation for building a term of a type from specified inputs.
Contradiction
A formula that is false in every model of the logic under discussion.
Counterexample
A case that shows a claim is false. For an inference, it is a case where the premises are true but the conclusion is false.
Counterfactual conditional
A conditional describing what would be the case under a supposition that may differ from the actual situation.
Read about Counterfactual conditional in Logical conditionals
Countermodel
A model in which all the premises of an inference are true and its conclusion is not true.
Curry–Howard correspondence
The correspondence between propositions and types, and between proofs and terms of those types.
Currying
Representing a function of several arguments as nested functions, each taking one argument.
De Morgan laws
The identities NOT (X OR Y) = (NOT X) AND (NOT Y) and NOT (X AND Y) = (NOT X) OR (NOT Y).
Decidable
A problem is decidable if an algorithm terminates on every allowed input with the correct yes-or-no answer.
Decision procedure
An algorithm that terminates on every allowed input with the correct yes-or-no answer.
Deductive closure
The set of all logical consequences of a set of formulas.
Deductive validity
The impossibility of the premises being true and the conclusion false in the reasoning situations under consideration.
Defeasible inference
An inference whose support can be overturned by additional evidence.
Definite clause
A disjunctive clause containing exactly one positive literal.
Denotation
The value of an expression under an interpretation; a term denotes an object, with variable values supplied by an assignment.
Denying the antecedent
The classically invalid pattern from A → B and ¬A to ¬B.
Dependent function
A function whose output type can depend on its input.
Depth-first search
A search that follows one branch as far as possible before returning to try an alternative.
Derivability
The existence of a formal proof of a conclusion from given assumptions, written with ⊢.
Designated value
A truth value counted as acceptable in defining a consequence relation; in K3, only 1 is designated.
Discharge
Ending a temporary assumption's role as an open assumption by applying a rule that permits it, such as conditional introduction.
Disjunction
An or-formula. Classical A∨B is true exactly when at least one disjunct is true, including when both are.
Disjunctive normal form
A disjunction of conjunctions of literals, abbreviated DNF.
Disjunctive syllogism
The inference from A ∨ B and ¬A to B, valid classically.
Domain
The nonempty set of objects over which an FOL model interprets names, predicates, functions, and quantifiers.
Domain relational calculus
A language for relational queries in which variables stand for domain objects and formulas specify satisfying assignments.
Effective axiomatization
Specifying the axioms of a theory so that an algorithm can list them all, though the list may be infinite.
Eigenvariable
A fresh name or variable used for an arbitrary object in a quantifier proof, subject to the rule's freshness conditions.
Elimination rule
An inference rule using a formula with the relevant main connective to derive a conclusion.
Empty clause
A disjunction with no literals, written ⊥. Its value is 0 under every Boolean valuation.
Empty string
The string containing no symbols, often written ε.
Entailment
Another name for semantic consequence, written with ⊨.
Enumerative induction
Generalizing from observed instances to a universal claim about a population. The universal claim entails its instances, giving weak logical support; the degree of support and the probability of the conclusion depend on the probability function.
Equisatisfiable
Two formulas are equisatisfiable iff they are either both satisfiable or both unsatisfiable.
Event
A set of outcomes in a probability space. In our logical treatment, propositions are events.
Exclusive or
The Boolean truth-function XOR, which returns 1 exactly when its two inputs differ.
Existential quantifier
The symbol ∃, used to say that at least one object in the domain satisfies a condition.
Existential witness
An object that satisfies the quantified scope of an existential claim.
Expansion
Adding a formula and all its consequences together with the old beliefs: KB+A=Cn(KB∪{A}).
Expert system
A system for reasoning or decision making in a particular area, typically combining a knowledge base of expert rules and facts with an inference engine.
Explainable AI
Research into making the behavior and results of AI systems understandable.
Explosion
The inference principle that any conclusion follows from a contradiction.
Extension
The objects, or tuples of objects, to which a predicate applies in a model.
Extension of an open formula
The set of ordered tuples of domain objects that satisfy a formula when assigned to its free variables in a specified order.
Extensional definition of a set
Specifying a set by listing its elements.
Read about Extensional definition of a set in Formal languages
Fact
In a propositional rule base, an atom given as known information.
Factoring
Unifying same-sign literals within a clause and retaining one copy, with the substitution applied to the whole clause.
Fair search
A search strategy that does not postpone any eligible inference forever.
Fallacy
An invalid pattern of reasoning that may appear correct.
Finite model
A model with a finite domain.
First-order atomic formula
A predicate applied to the appropriate number of terms, or an identity between two terms.
First-order clause
A finite disjunction of first-order literals, with all free variables universally quantified; the empty disjunction is ⊥.
First-order CNF
A conjunction of first-order clauses, each with its free variables understood as universally quantified.
First-order consequence
A formula C is a first-order consequence of premises Γ if every first-order model and variable assignment satisfying all formulas in Γ also satisfies C.
First-order literal
An atomic first-order formula or its negation.
First-order logic
A logic with names, predicates, function symbols, and quantifiers over objects.
First-order model
A nonempty domain with a denotation for each constant, a total function for each function symbol, and a relation for each predicate symbol.
First-order resolution
An inference from freshly renamed clauses with opposite-sign literals whose atoms unify, deleting those literals and applying their most general unifier to the remaining literals.
First-order satisfiability
A set of first-order sentences is satisfiable if some first-order model makes all of them true.
First-order signature
The constants, function symbols, and predicate symbols of a language, with a fixed arity for each function and predicate symbol.
Fluent
A feature of a world whose truth may change over time; a propositional planning encoding uses a separate atom for its value at each time point.
FOL SAT problem
The problem of determining whether a given finite set of first-order sentences has a model.
Formal language
A set of finite strings of symbols from an alphabet.
Formalization
Representing an expression or inference in a formal language.
Formula
An expression formed according to the syntax of a logical language.
Forward chaining
Starting with known facts and repeatedly applying rules to derive new facts.
Frame condition
A formula specifying when a fluent retains its value from one time point to the next.
Frame problem
The problem of representing what remains unchanged when an action occurs without explicitly describing every unaffected feature.
Free for
A term is free for a variable in a formula when substituting it for that variable captures none of the term’s variables.
Free variable
An occurrence of a variable not governed by a quantifier for that variable.
Full adder
A circuit that adds two bits and an incoming carry, returning a sum bit and an outgoing carry.
Function symbol
A symbol of fixed arity that forms an object-denoting term when applied to that many terms.
Fuzzy predicate
A predicate whose extension assigns degrees in [0,1] rather than just membership or nonmembership.
Goal clause
A disjunctive clause with no positive literal, expressing that its underlying atoms cannot all be true. The empty clause is included.
Grammar
Rules for generating the expressions of a formal language.
Ground formula
A formula containing no variables.
Ground term
A term containing no variables.
Half adder
A circuit that adds two bits, returning a sum bit and a carry bit. The sum is XOR of the inputs and the carry is AND of the inputs.
Halting problem
The problem of determining whether a given program will eventually stop on a given input.
Hardware verification
Checking whether a hardware implementation meets its specification.
Horn clause
A disjunctive clause containing at most one positive literal.
Horn formula
A conjunction of Horn clauses.
Horn SAT
The problem of deciding whether a finite conjunction of Horn clauses is satisfiable.
Idealization
Representing a situation in a simplified form that need not reproduce all its real features.
Idempotence
For a binary operation, the property that applying it to two copies of the same input returns that input.
Identity
Sameness of objects: a=b is true when the two terms denote the same object.
iff
An abbreviation of “if and only if”, asserting both directions of a condition.
Indefeasible consequence
A consequence that cannot be defeated by adding premises while the semantics remains fixed.
Inductive definition
A definition by initial cases and rules for generating further cases, with nothing else included.
Inductive strength
How strongly the premises support a conclusion without guaranteeing it, given the relevant background information.
Inductive support
Support that premises give a conclusion without guaranteeing it. In probability models, evidence positively supports a conclusion when learning the evidence raises its probability.
Inductive validity
In our weak logical sense, conditioning on the premises never lowers the probability of the conclusion, for any distribution giving the premises positive probability.
Inductive validity (in context)
In the sense used in chapter 1, the premises supporting the conclusion strongly enough to justify accepting it, without making it certain.
Inference
A piece of reasoning from premises to a conclusion.
Inference engine
The part of a reasoning system that applies rules to information in a knowledge base to derive further conclusions.
Inference indicator
A word or phrase, such as “therefore” or “since”, that signals an inference and helps identify its premises or conclusion.
Inference line
A horizontal line separating the premises above it from the conclusion below it.
Inference schema
A pattern of premises and conclusion with placeholders for expressions of specified grammatical categories.
Infinite model
A model with an infinite domain.
Infix notation
Notation in which a binary operator is written between its two arguments. Brackets or precedence conventions specify grouping.
Interpretation
An assignment of meanings to the nonlogical vocabulary of a formal language over a domain.
Intersection
The set of elements belonging to every one of the sets being intersected.
Introduction rule
An inference rule deriving a formula with the relevant connective as its main connective.
Intuitionistic logic
A logic whose natural deduction rules omit classical proof by contradiction; double-negation elimination is not generally available.
Iterated quantifiers
Quantifiers occurring within the scopes of other quantifiers.
Kernel
The component of a proof assistant that checks proofs according to its basic rules.
Kleene star
For an alphabet Σ, the set Σ* of all finite strings over Σ, including the empty string.
Knowledge base
A set of statements represented in a formal language, which an agent can ASK for consequences and TELL new information.
Knowledge engineering
Choosing a representation and encoding the information needed for a reasoning task.
Knowledge graph
A graph representing objects as nodes and relations among them through labeled links.
Knowledge Representation and Reasoning (KRR)
The study of how to represent information in a form that allows a system to draw conclusions and answer questions.
Read about Knowledge Representation and Reasoning (KRR) in Logic and AI
Least model
A model whose true atoms are contained among the true atoms of every model of the same formulas.
Lemma
A proved result used in another proof.
Likelihood ratio
The probability of the evidence if a conclusion is true, divided by its probability if the conclusion is false. Ratios above 1 favor the conclusion; ratios below 1 count against it.
Literal
An atomic formula or the negation of an atomic formula.
Log-likelihood ratio
The logarithm of the ratio of the likelihood of the evidence under a hypothesis to its likelihood under the alternative. Positive values favor the first hypothesis.
Logic
The discipline that aims to define and understand valid inference.
Logical consequence
A conclusion is a logical consequence of premises if every model making the premises true also makes the conclusion true.
Logical equivalence
Two formulas are logically equivalent if they have the same truth-value in every model of the logic.
Logical form
The structure of an expression or inference that matters for logical validity, abstracting from its particular subject matter.
Logical inductive support
Support that holds across all probability functions on a fixed model space for which conditioning on the premises is defined, using a specified criterion of support.
Logical invalidity
An inference being invalid on account of its logical form: some interpretation makes the premises true and the conclusion false.
Logical law
A general principle of valid inference in a logical system.
Logical operator
A symbol used to form compound expressions, such as negation or conjunction.
Logical proof. Alt: derivation
A chaining of inference rules applied to logical formulas, with assumptions tracked through the derivation.
Logical space
The collection of models considered by a semantics.
Logical system
A mathematical model of valid inference, typically comprising syntax, semantics, and proof theory.
Logical validity
Validity that depends on logical form, rather than the particular subject matter of the inference.
Material inductive support
Inductive support relative to a particular probability function and a chosen measure of support.
Material invalidity
An inference admitting a case where the premises are true and the conclusion false, even when the relevant meanings and background facts are respected.
Material validity
Correctness that depends on domain-specific meanings, facts, or assumptions; in inductive reasoning, support relative to a particular probability measure.
Mathematical theorem
A mathematical fact whose truth is established by a gapless, rigorous mathematical proof or argument.
Meaning postulate
A statement included among the background assumptions to capture a relationship between the meanings of expressions.
Metavariable
A variable in the language used to talk about another language; for example, A standing for any formula of propositional logic.
Model
A mathematical representation of a possible reasoning situation; a model of premises makes those premises true.
Model checking
Determining whether a formula is true in a specified model.
Modus ponens
The inference from A → B and A to B.
Modus tollens
The inference from A → B and ¬B to ¬A, valid classically.
Monotonicity of consequence
The property that adding premises to a valid inference preserves its validity, with interpretations and the model space held fixed.
Most general unifier
A unifier from which every other unifier is obtained by further substitution.
Multiple discharge
Discharging several occurrences of an assumption with the same label in one rule application.
Natural deduction
A proof system with introduction and elimination rules, including rules for reasoning with and discharging temporary assumptions.
Negation
A not-formula. Classical ¬A is true exactly when A is false.
Negation normal form
A propositional formula built from literals using only conjunction and disjunction.
Negative literal
The negation of an atomic formula. Negative describes its syntactic form, not its truth-value.
Normal form
A prescribed syntactic shape for expressions.
Numeral
A written expression representing a number; for example, 120 represents the number one hundred and twenty.
Occurs check
The unification check that rejects replacing a variable by a term containing that same variable properly.
Open assumption
An assumption on which a derivation still depends.
Open formula
A formula with at least one free variable occurrence.
Operator precedence
A convention specifying which operators bind more tightly when brackets are omitted.
Ordered tuple
A finite sequence of objects, with order and repetitions retained.
Parity
Whether a whole number is even or odd. The parity of a list of bits is 0 when it contains an even number of 1s and 1 otherwise.
Parsing
Reconstructing the grammatical structure of a string according to a grammar.
Plan
For a fixed horizon, a model of a planning knowledge base together with its initial and goal conditions, assigning values to state and action atoms at each time point.
Planning horizon
The chosen number of action steps in a bounded planning problem. A SAT encoding tests for a plan within that bound.
Pop
To remove and return the top item of a nonempty stack.
Positive literal
An unnegated atomic formula. Positive describes its syntactic form, not its truth-value.
Postfix (reverse Polish) notation
Notation in which each operator is written after its arguments. Fixed operator arities determine how the expression is grouped.
Read about Postfix (reverse Polish) notation in Formal languages
Predicate
A symbol expressing a property of objects or a relation among them.
Prefix (Polish) notation
Notation in which each operator is written before its arguments. Fixed operator arities determine how the expression is grouped.
Premise
A statement from which an inference starts.
Premise indicator
A word or phrase, such as “given that”, that signals a premise of an inference.
Probability
A measure of the chance of an event, given by adding the masses of its outcomes in our finite models.
Probability function
A measure assigning events probabilities between 0 and 1. In a finite space, outcome masses sum to 1 and event probabilities sum the masses of their outcomes.
Probability-raising support
Support measured by the conditional probability of the conclusion given the premises minus its unconditional probability. A positive difference favors the conclusion; a negative difference counts against it.
Proof assistant
Software for constructing formal proofs and checking that their steps obey the rules of the proof system.
Proof calculus
A system of rules for constructing logical proofs.
Proof checking
Checking that a supplied formal proof obeys the rules and establishes its stated conclusion from its stated assumptions.
Proof search
Searching for a formal derivation of a conclusion from assumptions.
Proof term
A typed term representing a formal proof, whose type expresses the proposition proved.
Proof theory
The study of formal proofs and the rules by which they are constructed; as a component of a logical system, it models stepwise inference.
Proposition
In this semantic approach, the set of models in which a formula is true.
Propositional variable
A basic symbol representing a proposition in a propositional language.
Pseudocode
A precise description of an algorithm written for readers, using programming-like notation without requiring a complete executable program.
Push
To add an item to the top of a stack.
Quantification
The expression of how many individuals satisfy a condition. Universal and existential quantification concern all individuals and at least one individual, respectively.
Quantifier scope
The formula that is the immediate child of a quantifier in a syntax tree.
Querying a database
Asking a database for information by specifying what to retrieve and which conditions it must meet.
Queue
A list processed in first-in, first-out order: new items enter at the end and the first item is removed next.
Recursion
Defining or carrying out a procedure through further calls to itself, directly or through other procedures.
Recursive case
A case handled by applying the same definition or procedure to smaller parts and combining their results.
Refutation
A derivation of a contradiction from a set of formulas, establishing that the set is unsatisfiable.
Refutation completeness
The property that every unsatisfiable input has a derivation of a contradiction in the given proof system.
Relational algebra
A language that forms relational queries using operations on tables.
Relational database
A database that stores relations as tables.
Relational query
A request for the assignments to a formula’s free variables that satisfy it in a database model.
Resolution
An inference rule that removes one complementary pair of literals from two clauses and forms the disjunction of the remaining literals.
Resolution pivot
The variable whose positive and negative literals are removed in one resolution step.
Resolvent
The disjunction of the literals remaining after one complementary pair is removed from two parent clauses, with repetitions removed.
Rewrite rule
A rule specifying how to replace an expression or a matching part of an expression.
Rooted tree
A structure of nodes joined by edges, with a designated root and exactly one path from the root to each other node.
Sample space
The set of possible outcomes of an experiment, written Ω.
SAT solving
Using an algorithm to decide whether a propositional formula or finite set of propositional formulas is satisfiable.
Satisfaction
The relation between a model, a variable assignment, and a formula that is true under that assignment in the model.
Satisfiability
A propositional formula is satisfiable iff some Boolean valuation makes it true. A set of formulas is jointly satisfiable iff one Boolean valuation makes all its formulas true.
Saturation under resolution
A clause list is saturated under resolution iff every resolvent is tautological or already present, ignoring the order and repetition of literals.
Semantics
The component of a logical system that specifies interpretations and truth conditions.
Semidecidability
The availability of a procedure that eventually confirms every positive instance, but may not terminate on a negative instance.
Sentence
A formula with no free variables.
Set
A collection of objects, called its members or elements. Sets are equal when they have exactly the same members.
Set abstraction
Specifying a set by a condition its members satisfy, within an intended domain.
Set diagram
A diagram representing sets by regions and membership by placement inside those regions.
Set difference
The difference S ∖ T contains the members of S that do not belong to T.
Set membership
An object belongs to a set if it is one of its elements, written ∈.
Shunting-yard algorithm
An algorithm that converts infix expressions to postfix notation, using a stack to hold operators until precedence and grouping allow them to be written to the output.
Skolem constant
A fresh constant used as an existential witness with no universally quantified variables in scope.
Skolem function
A fresh function symbol used to choose an existential witness as a function of the universally quantified variables in scope.
Skolemization
Replacing existentially quantified variables with fresh witness functions or constants, preserving satisfiability in an expanded language.
Sound argument
A deductively valid argument with true premises, and therefore a true conclusion. Distinct from soundness of a proof system.
Soundness
A proof system is sound if everything derivable from assumptions is a semantic consequence of those assumptions.
Stack
A collection in which items are added and removed at one end, the top. The last item added is the first removed.
Standardizing apart
Renaming variables in separate clause uses so that those uses have disjoint variable sets.
String
A finite sequence of symbols, where order and repetitions matter.
Subset
S is a subset of T when every member of S belongs to T. Equality is allowed.
Substitution
Replacing free occurrences of a variable by a term, while avoiding variable capture.
Syntax
The component of a logical system that specifies which expressions are well formed.
System 1 thinking
Fast, automatic, intuitive and associative thinking, usually requiring little conscious effort.
System 2 thinking
Slow, deliberate and conscious thinking, such as working through a calculation or checking an argument.
Tactic
An instruction for constructing a proof in a proof assistant, often by reducing a goal to simpler goals.
Tautological clause
A disjunctive clause containing a literal and its negation. It is true under every valuation and imposes no constraint on a satisfying valuation.
Tautology
A formula true in every valuation of the propositional logic under discussion.
Term
An expression for an object, built in FOL from variables, constants, and function symbols.
Termination
The property that a procedure finishes after finitely many steps on its intended inputs.
Time complexity
The running time of an algorithm as a function of its input size.
Total function
A function that assigns exactly one output to every input in its domain.
Truth in a model
A sentence is true in a model if it is satisfied under every variable assignment in that model.
Truth-functional completeness
A collection of truth-functions is truth-functionally complete if every Boolean truth-function of positive finite arity can be expressed using those functions.
Truth-table
A table listing the values of one or more propositional formulas under every assignment to their variables.
Truth-value
A value assigned to a formula by a semantics, such as 0 or 1 in classical logic.
Tseytin transformation
A linear-size CNF encoding that gives subformulas fresh variables, constrains their values, and asserts the original formula through its name.
Type
A classification of terms that determines which constructions and operations are permitted on them.
Type checking
Checking whether a term has a specified type according to the rules of the type system.
Typed term
An expression assigned a type by the rules of a type system; t : A states that t has type A.
Undecidable
A decision problem is undecidable when no algorithm terminates on every input and correctly answers every instance.
Undecidable statement (in a theory)
A statement that can neither be proved nor refuted in the theory under discussion.
Read about Undecidable statement (in a theory) in Logic and AI
Unification
Finding a substitution that makes two expressions syntactically identical.
Unifier
A substitution that makes two expressions syntactically identical.
Union
The union S ∪ T contains every object belonging to S or T, including objects belonging to both.
Unique readability
A property of a grammar: every expression it generates has exactly one grammatical structure.
Unit clause
A disjunctive clause consisting of a single literal. Satisfying it requires that literal to be true.
Universal closure
The sentence obtained by universally quantifying all free variables of a formula.
Universal quantifier
The symbol ∀, used to say that every object in the domain satisfies a condition.
Unsatisfiable
A propositional formula is unsatisfiable iff no Boolean valuation makes it true. A set of formulas is unsatisfiable iff no Boolean valuation makes all of them true.
Vacuous discharge
Discharge of an assumption that was not used in the derivation.
Vacuous quantifier
A quantifier whose scope contains no free occurrence of the variable it quantifies.
Validity
In the broad sense used in chapter 1, the premises supporting the conclusion in the way required by the kind of inference under discussion.
Variable assignment
A mapping from variables to objects in the domain of a model.
Verification
Checking that a proposed result meets a stated specification; for an argument, checking a proof or a countermodel in the chosen formal setting.