doc-src/Logics/logics.toc
 author lcp Wed Nov 10 05:00:57 1993 +0100 (1993-11-10) changeset 104 d8205bb279a7 child 136 a9015b16a0e5 permissions -rw-r--r--
Initial revision
 lcp@104 1 \contentsline {chapter}{\numberline {1}Introduction}{1} lcp@104 2 \contentsline {section}{\numberline {1.1}Syntax definitions}{1} lcp@104 3 \contentsline {section}{\numberline {1.2}Proof procedures}{3} lcp@104 4 \contentsline {chapter}{\numberline {2}First-order logic}{4} lcp@104 5 \contentsline {section}{\numberline {2.1}Syntax and rules of inference}{4} lcp@104 6 \contentsline {section}{\numberline {2.2}Generic packages}{8} lcp@104 7 \contentsline {section}{\numberline {2.3}Intuitionistic proof procedures}{8} lcp@104 8 \contentsline {section}{\numberline {2.4}Classical proof procedures}{10} lcp@104 9 \contentsline {section}{\numberline {2.5}An intuitionistic example}{11} lcp@104 10 \contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12} lcp@104 11 \contentsline {section}{\numberline {2.7}A classical example}{14} lcp@104 12 \contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{16} lcp@104 13 \contentsline {subsection}{Deriving the introduction rule}{17} lcp@104 14 \contentsline {subsection}{Deriving the elimination rule}{17} lcp@104 15 \contentsline {subsection}{Using the derived rules}{18} lcp@104 16 \contentsline {subsection}{Derived rules versus definitions}{20} lcp@104 17 \contentsline {chapter}{\numberline {3}Zermelo-Fraenkel set theory}{23} lcp@104 18 \contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{23} lcp@104 19 \contentsline {section}{\numberline {3.2}The syntax of set theory}{25} lcp@104 20 \contentsline {section}{\numberline {3.3}Binding operators}{25} lcp@104 21 \contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{28} lcp@104 22 \contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{33} lcp@104 23 \contentsline {subsection}{Fundamental lemmas}{33} lcp@104 24 \contentsline {subsection}{Unordered pairs and finite sets}{36} lcp@104 25 \contentsline {subsection}{Subset and lattice properties}{36} lcp@104 26 \contentsline {subsection}{Ordered pairs}{37} lcp@104 27 \contentsline {subsection}{Relations}{37} lcp@104 28 \contentsline {subsection}{Functions}{40} lcp@104 29 \contentsline {section}{\numberline {3.6}Further developments}{40} lcp@104 30 \contentsline {section}{\numberline {3.7}Simplification rules}{47} lcp@104 31 \contentsline {section}{\numberline {3.8}The examples directory}{48} lcp@104 32 \contentsline {section}{\numberline {3.9}A proof about powersets}{49} lcp@104 33 \contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{51} lcp@104 34 \contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{52} lcp@104 35 \contentsline {chapter}{\numberline {4}Higher-order logic}{55} lcp@104 36 \contentsline {section}{\numberline {4.1}Syntax}{55} lcp@104 37 \contentsline {subsection}{Types}{55} lcp@104 38 \contentsline {subsection}{Binders}{58} lcp@104 39 \contentsline {section}{\numberline {4.2}Rules of inference}{58} lcp@104 40 \contentsline {section}{\numberline {4.3}Generic packages}{62} lcp@104 41 \contentsline {section}{\numberline {4.4}A formulation of set theory}{63} lcp@104 42 \contentsline {subsection}{Syntax of set theory}{63} lcp@104 43 \contentsline {subsection}{Axioms and rules of set theory}{69} lcp@104 44 \contentsline {subsection}{Derived rules for sets}{69} lcp@104 45 \contentsline {section}{\numberline {4.5}Types}{69} lcp@104 46 \contentsline {subsection}{Product and sum types}{74} lcp@104 47 \contentsline {subsection}{The type of natural numbers, $nat$}{74} lcp@104 48 \contentsline {subsection}{The type constructor for lists, $\alpha \pcomma list$}{74} lcp@104 49 \contentsline {subsection}{The type constructor for lazy lists, $\alpha \pcomma llist$}{78} lcp@104 50 \contentsline {section}{\numberline {4.6}Classical proof procedures}{78} lcp@104 51 \contentsline {section}{\numberline {4.7}The examples directory}{78} lcp@104 52 \contentsline {section}{\numberline {4.8}Example: deriving the conjunction rules}{79} lcp@104 53 \contentsline {subsection}{The introduction rule}{79} lcp@104 54 \contentsline {subsection}{The elimination rule}{80} lcp@104 55 \contentsline {section}{\numberline {4.9}Example: Cantor's Theorem}{81} lcp@104 56 \contentsline {chapter}{\numberline {5}First-order sequent calculus}{83} lcp@104 57 \contentsline {section}{\numberline {5.1}Unification for lists}{83} lcp@104 58 \contentsline {section}{\numberline {5.2}Syntax and rules of inference}{84} lcp@104 59 \contentsline {section}{\numberline {5.3}Tactics for the cut rule}{84} lcp@104 60 \contentsline {section}{\numberline {5.4}Tactics for sequents}{88} lcp@104 61 \contentsline {section}{\numberline {5.5}Packaging sequent rules}{89} lcp@104 62 \contentsline {section}{\numberline {5.6}Proof procedures}{89} lcp@104 63 \contentsline {subsection}{Method A}{90} lcp@104 64 \contentsline {subsection}{Method B}{90} lcp@104 65 \contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{91} lcp@104 66 \contentsline {section}{\numberline {5.8}A more complex proof}{92} lcp@104 67 \contentsline {chapter}{\numberline {6}Constructive Type Theory}{95} lcp@104 68 \contentsline {section}{\numberline {6.1}Syntax}{96} lcp@104 69 \contentsline {section}{\numberline {6.2}Rules of inference}{96} lcp@104 70 \contentsline {section}{\numberline {6.3}Rule lists}{101} lcp@104 71 \contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{104} lcp@104 72 \contentsline {section}{\numberline {6.5}Rewriting tactics}{105} lcp@104 73 \contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{105} lcp@104 74 \contentsline {section}{\numberline {6.7}A theory of arithmetic}{106} lcp@104 75 \contentsline {section}{\numberline {6.8}The examples directory}{106} lcp@104 76 \contentsline {section}{\numberline {6.9}Example: type inference}{108} lcp@104 77 \contentsline {section}{\numberline {6.10}An example of logical reasoning}{109} lcp@104 78 \contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{112} lcp@104 79 \contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{113} lcp@104 80 \contentsline {chapter}{\numberline {7}Defining Logics}{118} lcp@104 81 \contentsline {section}{\numberline {7.1}Precedence grammars}{118} lcp@104 82 \contentsline {section}{\numberline {7.2}Basic syntax}{119} lcp@104 83 \contentsline {subsection}{Logical types and default syntax}{120} lcp@104 84 \contentsline {subsection}{Lexical matters *}{121} lcp@104 85 \contentsline {subsection}{Inspecting syntax *}{121} lcp@104 86 \contentsline {section}{\numberline {7.3}Abstract syntax trees}{123} lcp@104 87 \contentsline {subsection}{Parse trees to asts}{125} lcp@104 88 \contentsline {subsection}{Asts to terms *}{126} lcp@104 89 \contentsline {subsection}{Printing of terms *}{126} lcp@104 90 \contentsline {section}{\numberline {7.4}Mixfix declarations}{128} lcp@104 91 \contentsline {subsection}{Infixes}{130} lcp@104 92 \contentsline {subsection}{Binders}{130} lcp@104 93 \contentsline {section}{\numberline {7.5}Syntactic translations (macros)}{131} lcp@104 94 \contentsline {subsection}{Specifying macros}{132} lcp@104 95 \contentsline {subsection}{Applying rules}{133} lcp@104 96 \contentsline {subsection}{Rewriting strategy}{135} lcp@104 97 \contentsline {subsection}{More examples}{135} lcp@104 98 \contentsline {section}{\numberline {7.6}Translation functions *}{138} lcp@104 99 \contentsline {subsection}{A simple example *}{139} lcp@104 100 \contentsline {section}{\numberline {7.7}Example: some minimal logics}{140}