Rex Page - Essential Logic for Computer Science

List of Figures

Equations of numeric algebra.

Why (1) (1) = 1.

Boolean axioms (basic equations).

Proof of theorem { truth table}.

Proof of theorem { complement}.

Proof of theorem { truth table}.

Proof of theorem { truth table}.

Proof of theorem { null}.

Proof of theorem { absorption}.

Rules of grammar for Boolean formulas.

Axioms of Boolean algebra.

Some Boolean theorems.

Digital circuits = logic formulas.

Nand is all you need.

Rules of inference for natural deduction.

Theorem {Socrates was mortal}: citing modus ponens.

{ commutes}: citing three inference rules involving .

{self-implication}: citing {identity} and { introduction} inference rules.

{ commutes}: citing { elimination}.

Proving the implication chain rule.

{modus tollens}: citing a theorem to justify an inference.

{ forward}: citing reductio ad absurdum.

{disjunctive syllogism}: citing {contradiction}.

A four-step strategy for reasoning with quantifiers.

Equations of quantifier reasoning.

Proof of equation { }.

Example: migrating quantifiers.

A game of Nim.

Shorthand for nested cons: list.

Nonempty list predicate: consp.

Numbered list notation.

List constructor and deconstructors: cons, first, rest.

Length of list: .

Formula selector: .

DoubleCheck test of append.

List concatenation: append.

Mathematical induction: a rule of inference.

The three Cs: a guide to inductive definitions.

Defining concatenation: append.

Defining list suffix extractor: nthcdr.

Inductive case: S(n) S(n + 1).

Defining list prefix extractor: prefix.

Inductive case: n. P(n) P(n + 1).

Proof Pad session with proof bar.

Importing theorems to facilitate proof: append-suffix theorem.

Theorem with constraint: append-prefix.

Fibonacci numbers.

Fibonacci numbers: quick delivery.

Fast Fibonacci delivers Fibonacci numbers.

Theorem {halting problem}: a proof by contradiction.

Definitions of operators and loop.

Proof of theorem {H}.

Theorem {halting problem}: a proof by contradiction.

{Horner 10}: proof of base case.

{Horner 10}: proof of inductive case.

Proof by induction of theorem {dgts-ok}.

Mathematical induction (strong induction version).

Definitions of operators bits and numb.

Adding decimal numerals.

Adding binary numerals.

Half-adder circuit and ACL2 model.

Full-adder circuit and ACL2 model.

Full-adder theorem.

Two-bit adder and ACL2 model.

Ripple-carry adder and ACL2 model.

Adding w-bit binary numerals.

Theorem {adder-ok}: proof by mathematical induction.

Twos-complement numerals for three-bit words.

Twos-complement negation trick.

Bignum addition operator.

Grade-school multiplication: digit by digit.

Bignum multiplication operator.

Theorem {mux-length}: inductive case when both operands are nonempty.

Theorems and lemmas about merge-sort.

Basic one-step operators.

Computation steps in formulas with basic operators.

Computation steps in demultiplex.

Double induction: a rule of inference.

Recurrence inequalities for merge-sort computation steps.

Bound on steps in merge-sort computation.

Formal definition of isort.

In = average number of steps to compute (isortxx1x2xn.

Search tree diagram and corresponding formula.

Search tree operators and predicates.

Balance shortens trees.

Balance predicate.

Insert new key, preserving order but not balance.

Balanced trees of height n + 2.

Balanced trees of height n + 2, subtrees expanded.

Insertion, unbalanced outcome, and rebalancing.

Rotation operators and .

Inside cases.

Using the wrong rotation can make it worse.

Double rotation rebalances inside cases.

Formal definition of the clockwise rotation operator.

Formal definition of the insertion operator.

Revised operators to avoid height computation.

Operator to find state capitals.

Letterbox array and capital search operator.

Hash table storage and retrieval.

Prototype hashing operators (slow: using lists, not arrays).

Tables for Facebook-style status updates.

Storing friends lists in Cassandra.

Storing status updates in Cassandra.

Iterative MapReduce operation.

A picture encoded as a matrix of pixels.

Straight line vs. a line made up of random segments.

Operator to draw a ragged line using random numbers.

List of Table

Ten-bucket hash table for state capitals.

List of Boxes

Models of Computation

Operators, Operands, Functions, Parameters, Arguments

Hold on to Your Seat

Truth Tables

Truth Tables and Feasibility

Abstraction

Boolean Equivalence ()

Implication Gate Is Universal

Struggling? Join the Club

Variables Stand for Formulas

Quantifier with Empty Universe

Equal by Definition:

Other Quantifiers

Proof Pad and ACL2

Natural Numbers

Modular Arithmetic

Local Names for Values: *

Floor and Ceiling Operators, Floor and Ceiling Brackets

Square Bracket Notation for Lists: Paper-and-Pencil Only

Equal by Definition:

Suppressing Computation with Single-Quote