action: a literal or a print command in a production system.
aleph-null: the cardinality,of the setof natural numbers.
AND: the logical operator for conjunction, also written.
antecedent: in a conditional proposition(“ifthen”) the proposition(“if-clause”) that precedes the arrow.
antichain: a subset of a poset in which no two elements are comparable.
antisymmetric: the property of a binary relationthat ifandthen
argument form: a sequence of statement forms each called a premise of the argument followed by a statement form called a conclusion of the argument.
assertion (or program assertion): a program comment specifying some conditions on the values of the computational variables; these conditions are supposed to hold whenever program flow reaches the location of the assertion.
asymmetric: the property of a binary relationthat ifthen
asymptotic: A functionis asymptotic to a functionwritten if
for sufficiently large x and
atom (or atomic formula): simplest formula of predicate logic.
atomic formula: See atom.
atomic proposition: a proposition that cannot be analysed into smaller parts and logical operations.
automated reasoning: the process of proving theorems using a computer program that can draw conclusions that follow logically from a set of given facts.
axiom: a statement that is assumed to be true; a postulate.
axiom of choice: the assertion that given any nonempty collectionof pairwise disjoint sets, there is a set that consists of exactly one element from each of the sets in
axiom (or semantic axiom): a rule for a programming language construct prescribing the change of values of computational variables when an instruction of that construct type is executed.
basis step: a proof of the basis premise (first case) in a proof by mathematical induction.
big-oh notation:iswrittenif there are constantsandsuch thatfor all
bijection (or bijective function): a function that is one-to-one and onto.
bijective function: See bijection.
binary relation from a setto a setany subset of
binary relation on a seta binary relation fromtoi.e., a subset of
body of a clausein a logic program: the literals B1 , . . . , Bm
cardinal number (or cardinality) of a set: for a finite set, the number of elements; for an infinite set, the order of infinity. The cardinal number ofis written
cardinality: See cardinal number.
Cartesian product (of setsand): the setof ordered pairswith
and(more generally, the iterated Cartesian productis the set of ordered-tupleswithfor each).
ceiling (of): the smallest integer that is greater than or equal towritten
chain: a subset of a poset in which every pair of elements are comparable.
characteristic function (of a set): the function fromtowhose value at
is 1 ifand 0 if
clause (in a logic program): closed formula of the form
closed formula: for a function valuean algebraic expression in
closure (of a relationwith respect to a property): the relationif it exists, that has propertyand containssuch thatis a subset of every relation that has propertyand contains
codomain (of a function): the set in which the function values occur.
comparable: Two elements in a poset are comparable if they are related by the partial order relation.
complement (of a relation): given a relationthe relationwhereif and only if
complement (of a set): given a setin a “universal” domainthe setof objects inthat are not in
complement operator: a functionused for complementing fuzzy sets.
complete: property of a set of axioms that it is possible to prove all true statements.
complex number: a number of the formwhereandare real numbers, anthe set of all complex numbers is denoted
composite key: given an-ary relationona product of domains
such that for each-tuplethere is at most one-tuple inthat matchesin coordinates
composition (of relations): fora relation fromtoanda relation fromto the relationfromtosuch thatif and only if there existssuch thatand
composition (of functions): the functionwhose value atis
compound proposition: a proposition built up from atomic propositions and logical connectives.
computer-assisted proof : a proof that relies on checking the validity of a large number of cases using a special purpose computer program.
conclusion (of an argument form): the last statement of an argument form.
conclusion (of a proof): the last proposition of a proof; the objective of the proof is
demonstrating that the conclusion follows from the premises.
condition: the disjunctionof atomic formulas.
conditional statement: the compound proposition(“ifthen”) that is true except whenis true andis false.
conjunction: the compound proposition(“and”) that is true only when
andare both true.
conjunctive normal form: for a proposition in the variablesan equivalent proposition that is the conjunction of disjunctions, with each disjunction of the forwhereis eitheror
consequent: in a conditional proposition(“ifthen”) the proposition(“then-clause”) that follows the arrow.
consistent: property of a set of axioms that no contradiction can be deduced from the axioms.
construct (or program construct): the general form of a programming instruction such as an assignment, a conditional, or a while-loop.
continuum hypothesis: the assertion that the cardinal number of the real numbers is the smallest cardinal number greater than the cardinal number of the natural numbers.
contradiction: a self-contradictory proposition, one that is always false.
contradiction (in an indirect proof): the negation of a premise.
contrapositive (of the conditional proposition): the conditional proposition
converse (of the conditional proposition): the conditional proposition
converse relation: another name for the inverse relation.
corollary: a theorem that is derived as an easy consequence of another theorem.
correct conclusion: the conclusion of a valid proof, when all the premises are true.
countable set: a set that is finite or denumerable.
counterexample: a case that makes a statement false.
definite clause: clause with at most one atom in its head.
denumerable set: a set that can be placed in one-to-one correspondence with the natural numbers.
diagonalization proof : any proof that involves something analogous to the diagonal of a list of sequences.
difference: a binary relationsuch thatif and only ifis true andis false.
difference (of sets): the setof objects inthat are not in
direct proof : a proof ofthat assumesand shows thatmust follow.
disjoint (pair of sets): two sets with no members in common.
disjunction: the statement(“or”) that is true when at least one of the two
propositions p and q is true; also called inclusive or.
disjunctive normal form: for a proposition in the variablesan equivalent proposition that is the disjunction of conjunctions, with each conjunction of the formwhereis eitheror
disproof : a proof that a statement is false.
divisibility lattice: the lattice consisting of the positive integers under the relation
domain (of a function): the set on which a function acts.
element (of a set): member of the set; the notationmeans thatis an element
elementary projection function: the functionsuch that
empty set: the set with no elements, writtenor
epimorphism: an onto function.
equality (of sets): property that two sets have the same elements.
equivalence class: given an equivalence relation on a setandthe subset of consisting of all elements related to a.
equivalence relation: a binary relation that is reflexive, symmetric, and transitive.
equivalent propositions: two compound propositions (on the same simple variables) with the same truth table.
existential quantifier: the quantifierread “there is an”.
existentially quantified predicate: a statementthat there exists a value
ofsuch thatis true.
exponential function: any function of the form a positive constant,
fact set: set of ground atomic formulas.
factorial (function): the functionwhose value on the argumentis the productthat is,
finite: property of a set that it is either empty or else can be put in a one-to-one correspondence with a setfor some positive integer
first-order logic: See predicate calculus.
floor (of): the greatest integer less than or equal towritten
formula: a logical expression constructed from atoms with conjunctions, disjunctions, and negations, possibly with some logical quantifiers.
full conjunctive normal form: conjunctive normal form where each disjunction is a disjunction of all variables or their negations.
full disjunctive normal form: disjunctive normal form where each conjunction is a conjunction of all variables or their negations.
fully parenthesized proposition: any proposition that can be obtained using the following recursive definition: each variable is fully parenthesized, if P and Q are fully parenthesized, so areand
functiona rule that assigns to every objectin the domain setexactly one objectin the codomain set
functionally complete set: a set of logical connectives from which all other connectives can be derived by composition.
fuzzy logic: a system of logic in which each statement has a truth value in the interval
fuzzy set: a set in which each element is associated with a number in the intervalthat measures its degree of membership.
generalized continuum hypothesis: the assertion that for every infinite setthere is no cardinal number greater thanand less than
goal: a clause with an empty head.
graph (of a function): given a functionthe set
greatest lower bound (of a subset of a poset): an element of the poset that is a lower bound of the subset and is greater than or equal to every other lower bound of the subset.
ground formula: a formula without any variables.
halting function: the function that maps computer programs to the setwith value 1 if the program always halts, regardless of input, and 0 otherwise.
Hasse diagram: a directed graph that represents a poset.
head (of a clause): the literalsbefore
identity function (on a set): given a setthe function fromto itself whose value atis
image set (of a function): the set of function values as x ranges over all objects of the domain.
implication: formally, the relationthat a propositionis true whenever propositionis true; informally, a synonym for the conditional statement
incomparable: two elements in a poset that are not related by the partial order relation.
induced partition (on a set under an equivalence relation): the set of equivalence classes under the relation.
independent: property of a set of axioms that none of the axioms can be deduced from the other axioms.
indirect proof : a proof ofthat assumesis true and proves thatis true.
induction: See mathematical induction.
induction hypothesis: in a mathematical induction proof, the statementin the induction step.
induction step: in a mathematical induction proof, a proof of the induction premise “ifis true, thenis true”.
inductive proof : See mathematical induction.
infinite (set): a set that is not finite.
injection (or injective function): a one-to-one function.
instance (of a formula): formula obtained using a substitution.
instantiation: substitution of concrete values for the free variables of a statement or sequence of statements; an instance of a production rule.
integer: a whole number, possibly zero or negative; i.e., one of the elements in the set
intersection: the setof objects common to both setsand
intersection relation: for binary relationsandonthe relationwhere
if and only ifand
interval (in a poset): givenin a poset, a subset of the poset consisting of all elementssuch that
inverse function: for a one-to-one, onto functionthe functionwhose value atis the uniquesuch that
inverse image (underof a subset): the subset
inverse relation: for a binary relationfromtothe relationfromto
whereif and only if
invertible (function): a one-to-one and onto function; a function that has an inverse.
irrational number: a real number that is not rational.
irreflexive: property of a binary relationonthatfor all
lattice: a poset in which every pair of elements has both a least upper bound and a greatest lower bound.
least upper bound (of a subset of a poset): an element of the poset that is an upper bound of the subset and is less than or equal to every other upper bound of the subset.
lemma: a theorem that is an intermediate step in the proof of a more important theorem.
linearly ordered: the property of a poset that every pair of elements are comparable, also called totally ordered.
literal: an atom or its negation.
logarithmic function: a function(a positive constant,) defined by the ruelif and only if
logic program: a finite sequence of definite clauses.
logically equivalent propositions: compound propositions that involve the same variables and have the same truth table.
logically implies: A compound propositionlogically implies a compound propositionif is true wheneveris true.
loop invariant: an expression that specifies the circumstance under which the loop body will be executed again.
lower bound (for a subset of a poset): an element of the poset that is less than or equal to every element of the subset.
mathematical induction: a method of proving that every item of a sequence of propositions such asis true by showing: (1) is true, and (2) for allis true.
maximal element: in a poset an element that has no element greater than it.
maximum element: in a poset an element greater than or equal to every element.
membership function (in fuzzy logic): a function from elements of a set to
membership table (for a set expression): a table used to calculate whether an object lies in the set described by the expression, based on its membership in the sets mentioned by the expression.
minimal element: in a poset an element that has no element smaller than it.
minimum element: in a poset an element less than or equal to every element.
monomorphism: a one-to-one function.
multi-valued logic: a logic system with a set of more than two truth values.
multiset: an extension of the set concept, in which each element may occur arbitrarily
mutually disjoint (family of sets): (See pairwise disjoint.)
-ary predicate: a statement involving n variables.
-ary relation: any subset of
naive set theory: set theory where any collection of objects can be considered to be a valid set, with paradoxes ignored.
NAND: the logical connective “not and”.
natural number: a nonnegative integer (or “counting” number); i.e., an element of
Note: Sometimes 0 is not regarded as a natural number.
negation: the statement (“not”) that is true if and only ifis not true.
NOP: pronounced “no-op”, a program instruction that does nothing to alter the values of computational variables or the order of execution.
NOR: the logical connective “not or”.
NOT: the logical connective meaning “not”, used in place of ¬.
null set: the set with no elements, writtenor
omega notation:if there are constantsandsuch thatfor all
one-to-one (function): a functionthat assigns distinct elements of the
codomain to distinct elements of the domain; thus, ifthen
onto (function): a functionwhose image equals its codomain; i.e., for everythere is ansuch that
OR: the logical operator for disjunction, also written
pairwise disjoint: property of a family of sets that each two distinct sets in the family have empty intersection; also called mutually disjoint.
paradox: a statement that contradicts itself.
partial function: a functionthat assigns a well-defined object into some (but not necessarily all) the elements of its domain
partial order: a binary relation that is reflexive, antisymmetric, and transitive.
partially ordered set: a set with a partial order relation defined on it.
partition (of a set): given a set S, a pairwise disjoint familyof nonempty subsets ofwhose union is
Peano definition: a recursive description of the natural numbers that uses the concept of successor.
Polish prefix notation: the style of writing compound propositions in prefix notationwhere sometime the usual operand symbols are replaced as followsfor for
poset: a partially ordered set.
postcondition: an assertion that appears immediately after the executable portion of a program fragment or of a subprogram.
postfix notation: the style of writing compound logical propositions where operators
are written to the right of the operands.
power (of a relation): for a relation R on A, the relation Rn on A where R0 = I,
R1 = R and Rn = Rn−1 ◦ R for all n > 1.
power set: given a set A, the set P(A) of all subsets of A.
precondition: an assertion that appears immediately before the executable portion of
a program fragment or of a subprogram.
predicate: a statement involving one or more variables that range over various do-
predicate calculus: the symbolic study of quantified predicate statements.
prefix notation: the style of writing compound logical propositions where operators are written to the left of the operands.
premise: a proposition taken as the foundation of a proof, from which the conclusion is to be derived.
prenex normal form: the form of a well-formed formula in which every quantifier occurs at the beginning and the scope is whatever follows the quantifiers.
preorder: a binary relation that is reflexive and transitive.
primary key: for an-ary relation ona coordinate domainsuch that for eachthere is at most one-tuple in the relation whose jth coordinate is
production rule: a formula of the formwhere eachis a condition and eachis an action.
production system: a set of production rules and a fact set.
program construct: See construct.
program fragment: any sequence of program code, from a single instruction to an entire program.
program semantics (or semantics): the meaning of an instruction or of a program fragment; i.e., the effect of its execution on the computational variables.
projection function: a function defined on a set of-tuples that selects the elements in certain coordinate positions.
proof (of a conclusion from a set of premises): a sequence of statements (called steps)
terminating in the conclusion, such that each step is either a premise or follows from previous steps by a valid argument.
proof by contradiction: a proof that assumes the negation of the statement to be proved and shows that this leads to a contradiction.
proof done by hand: a proof done by a human without the use of a computer.
proper subset: given a seta subsetofsuch thatcontains at least one element not in
proposition: a declarative sentence or statement that is unambiguously either true or false.
propositional calculus: the symbolic study of propositions.
range (of a function): the image set of a function; sometimes used as synonym for codomain.
rational number: the set of rational numbers is denoted
real number: the set of all real numbers is denoted
recursive definition (of a function with domain): a set of initial values and a rule for computingin terms of valuesfor
recursive definition (of a set): a form of specification of membership ofin which some basis elements are named individually, and in which a computable rule is given to construct each other element in a finite number of steps.
refinement of a partition: given a partitionon a seta partitionon the same set S such that everyis a subset of some
reflexive: the property of a binary relationthat
relation (from setto set): a binary relation fromto
relation (on a set): a binary relation fromto
restriction (of a function): givenand a subsetthe functionwith domaiand codomainwhose rule is the same as that of
reverse Polish notation: postfix notation.
rule of inference: a valid argument form.
scope (of a quantifier): the predicate to which the quantifier applies.
semantic axiom: See axiom.
semantics: See program semantics.
sentence: a well-formed formula with no free variables.
sequence (in a set): a list of objects from a setwith repetitions allowed; that is, a function(an infinite sequence, often written) or a function(a finite sequence, often written).
set: a well-defined collection of objects.
singleton: a set with one element.
specification: in program correctness, a precondition and a postcondition.
statement form: a declarative sentence containing some variables and logical symbols
which becomes a proposition if concrete values are substituted for all free variables.
string: a finite sequence in a setusually written so that consecutive entries are juxtaposed (i.e., written with no punctuation or extra space between them).
strongly correct code: code whose execution terminates in a computational state satisfying the postcondition, whenever the precondition holds before execution.
subset of a setany setof objects that are also elements ofwritten
substitution: a set of pairs of variables and terms.
surjection (or surjective function): an onto function.
symmetric: the property of a binary relationthat ifthen
symmetric difference (of relations): for relationsandonthe relationwhereif and only if exactly one of the following is true:
symmetric difference (of sets): for setsandthe setcontaining each object that is an element ofor an element ofbut not an element of both.
system of distinct representatives: given sets(some of which may be equal), a setof n distinct elements withfor
tautology: a compound proposition whose form makes it always true, regardless of the truth values of its atomic parts.
term (in a domain): either a fixed element of a domainor an-valued variable.
theorem: a statement derived as the conclusion of a valid proof from axioms and definitions.
theta notation:writtenif there are positive constantsandsuch thatfor all
totally ordered: the property of a poset that every pair of elements are comparable; also called linearly ordered.
transitive: the property of a binary relationthat ifandthen
transitive closure: for a relationonthe smallest transitive relation containing
transitive reduction (of a relation): a relation with the same transitive closure as the original relation and with a minimum number of ordered pairs.
truth table: for a compound proposition, a table that gives the truth value of the proposition for each possible combination of truth values of the atomic variables in the proposition.
two-valued logic: a logic system where each statement has exactly one of the two values: true or false.
union: the setof objects in one or both of the setsand
union relation: forandbinary relations onthe relationwhere
if and only ifor
universal domain: the collection of all possible objects in the context of the immediate discussion.
universal quantifier: the quantifierread “for all” or “for every”.
universally quantified predicate: a statementthatis true for everyin its universe of discourse.
universe of discourse: the range of possible values of a variable, within the context of the immediate discussion.
upper bound (for a subset of a poset): an element of the poset that is greater than or equal to every element of the subset.
valid argument form: an argument form such that in any instantiation where all the premises are true, the conclusion is also true.
Venn diagram: a figure composed of possibly overlapping circles or ellipses, used to picture membership in various combinations of the sets.
verification (of a program): a formal argument for the correctness of a program with respect to its specifications.
weakly correct code: code whose execution results in a computational state satisfying the postcondition, whenever the precondition holds before execution and the execution terminates.
well-formed formula (wff ): a proposition or predicate with quantifiers that bind one or more of its variables.
well-ordered: property of a set that every nonempty subset has a minimum element.
well-ordering principle: the axiom that every nonempty subset of integers, each
greater than a fixed integer, contains a smallest element.
XOR: the logical connective “not or”.
Zermelo-Fraenkel axioms: a set of axioms for set theory.
zero-order logic: propositional calculus.