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

after

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 exists such 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

of divisibility.

domain (of a function): the set on which a function acts.

element (of a set): member of the set; the notationmeans thatis an element

of

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 product that 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

written

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.

little-oh notation:isif

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

many times.

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 every there 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

forforfor

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-

mains.

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 each there 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 of written

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.