Mathematical Logic
Comp520e Hui Li
Turing Machine
- Alan Turing
- Turing Machine, Abacus Machine
- A Doubling Turing Machine: Flow Chart, Results
Propositional Logic
- Formula, Tree Form, String Form, Formal Grammar
- Interpretation, Truth Table, Boolean Operators, Sets of Operators, Functional Completeness
- Logically Equivalent, Logical Equivalence Examples
- Satisfiable/Valid (Tautology)/Unsatisfiable/Falsible, Decision Procedures
- Satisfiability of a set of formulas, Logical Consequence, Semantic Tableaux
- Deductive Systems, Hilbert System, Variant Form of the Deductive Systems
- Resolution, Conjunctive Norm Form, Clausal Form, CNF to 3CNF
- Binary Decision Diagram, Efficient Truth Table, Reduced Binary Decision Diagram
First-Order Logic
- Sequence, Tuple, Cartesian Product, Relation, Function
- Generalization, Symbols, Formula, Open and Close, Formal Grammar
- Interpretation, Assignment and Truth Value, Ground, Validity and Satisfiability
- Interpretation for A Set of formulas
- Language of Arithmetic, Interpretation of Arithmetic Language, Syntax of Language
- Logical Equivalence, Logical Consequence, Logical Equivalence Examples
- Semantic Tableaux, Hilbert System
- PCNF, Clauses Form, Skolem's Theorem, Skolem's Algorithm
- Herbrand Models, Ground Resolution, Substitution, Unification
Prolog Programming
- Horn Clause
- SLD Resolution, Search Rules, SLD Tree
- Prolog Software: SWI Prolog
- Prolog Examples: Hanoi, Results; GK.2010.83
网站备案