Next:
Introduction
MAU22C00 lecture notes
John Stalker
Introduction
A simplified example
Rules
Languages
Statements
A formal language
Logic
Parse trees
Graphs
Interpretation
Expressiveness
Parsing
Infix, prefix and postfix
A parser for the prefix language
A parser for the postfix language
Parser generators
A simple checker
A simpler checker
Idealised machines
A hierarchy of languages
Satisfiability
Tautologies and consequences
Rules of inference
Formal systems
Sets
A regular language
Conclusion
Languages
A grammar example (bc)
Terminology
Thinking backwards
A subexample
More numerical examples
Ambiguous grammars
Constructing a “parser” from a grammar
Formal definition
Grammars
Hierarchy
Back to the beginning
A final example
Zeroeth order logic
Formal vs informal proof
Formal systems
A language for zeroeth order logic
Interpretation(s)
Truth tables
Informal proofs in zeroeth order logic
Analytic tableaux
Tableau rules
Satisfiability
Another example
Consequences
Tableaux as nondeterministic computations
The Nicod formal system
Soundness of the Nicod system
Completeness of the Nicod system
The Łukasiewicz system
Natural deduction
A formal system for natural deduction
Introducing and discharging hypotheses
Some proofs
Substitution
More proofs
Soundness, consistency and completeness
First order logic
A language for first order logic
Free and bound variables
Interpretations
Informal proofs
Tableaux for first order logic
Example tableaux
Tableaux as nondeterministic computations
Natural deduction for first order logic
Soundness, consistency and completeness of first order logic
Elementary arithmetic
A language for arithmetic
Expressing more complex ideas
Arithmetic subsets
Encoding
Encoding arithmetic in arithmetic
A formal system for arithmetic
Induction
A formal proof
Gödel’s theorem and Tarski’s theorem.
Set theory
A language for set theory
Simple set theory
Axioms (informal version)
Discussion
Axioms (formal version)
Non-sets
Set operations and Boolean operations
Finite sets
Definitions
Elementary properties of finite sets.
Induction for finite sets
Lists
Chains and pairs
Ordered pairs
Lists
Interfaces
Cartesian products
Relations
Basic definitions
Examples
Functions
Order relations, equivalence relations
Notation
Infinite sets
Natural numbers
The set of natural numbers
Cardinality
Diagonalisation
Countable sets
Properties of countable sets
Uncountable sets
Axiom(s) of choice
Computational paths
Dependent choice
The Axiom of Choice
Banach-Tarski
Additional axioms
Foundation
Extensionality, again
Zermelo-Fraenkel
Graph theory
Examples
Different notions of a graph
Definition
Ways to describe graphs
Bipartite graphs, complete graphs
Isomorphism
Subgraphs, degrees
Walks, trails, paths, etc.
Connectedness
Eulerian trails and circuits
Hamiltonian paths and circuits
Spanning trees
Abstract algebra
Binary operations
Semigroups
Identity elements, monoids
Inverse elements and groups
Homomorphisms
Quotients
Integers and rationals
The power function
Notation
Regular languages
Regular grammars
Closure properties
Unions
Concatenation
Kleene star
Reversal
Finite state automata
Non-deterministic finite state automata
Deterministic finite state automata
Closure properties
Intersection
Relative complements
Regular expressions
The basic operations
Examples
From regular expressions to grammars
Regular expressions from automata
Reversal
Extended syntax
Regular languages
Pumping lemma
The statement of the lemma
An example
Finite languages
The proof of the lemma
The Myhill-Nerode theorem
From languages to automata
An example
The converse
The syntactic monoid
Context free languages
Closure properties
Pushdown automata
Parsing by guessing
Deterministic pushdown automata
From pushdown automata to context free grammars
Pumping lemma
Application
Proof