doc-src/Logics/logics.toc
 author wenzelm Fri, 16 Jul 1999 22:24:42 +0200 changeset 7024 44bd3c094fd6 parent 465 d4bf81734dfe permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 359 b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  1 \contentsline {chapter}{\numberline {1}Basic Concepts}{1}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  2 \contentsline {section}{\numberline {1.1}Syntax definitions}{2}  104 d8205bb279a7 Initial revision lcp parents: diff changeset  3 \contentsline {section}{\numberline {1.2}Proof procedures}{3}  359 b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  4 \contentsline {chapter}{\numberline {2}First-Order Logic}{4}  104 d8205bb279a7 Initial revision lcp parents: diff changeset  5 \contentsline {section}{\numberline {2.1}Syntax and rules of inference}{4}  d8205bb279a7 Initial revision lcp parents: diff changeset  6 \contentsline {section}{\numberline {2.2}Generic packages}{8}  d8205bb279a7 Initial revision lcp parents: diff changeset  7 \contentsline {section}{\numberline {2.3}Intuitionistic proof procedures}{8}  d8205bb279a7 Initial revision lcp parents: diff changeset  8 \contentsline {section}{\numberline {2.4}Classical proof procedures}{10}  d8205bb279a7 Initial revision lcp parents: diff changeset  9 \contentsline {section}{\numberline {2.5}An intuitionistic example}{11}  d8205bb279a7 Initial revision lcp parents: diff changeset  10 \contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12}  d8205bb279a7 Initial revision lcp parents: diff changeset  11 \contentsline {section}{\numberline {2.7}A classical example}{14}  359 b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  12 \contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{15}  465 d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  13 \contentsline {subsection}{\numberline {2.8.1}Deriving the introduction rule}{16}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  14 \contentsline {subsection}{\numberline {2.8.2}Deriving the elimination rule}{17}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  15 \contentsline {subsection}{\numberline {2.8.3}Using the derived rules}{17}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  16 \contentsline {subsection}{\numberline {2.8.4}Derived rules versus definitions}{19}  359 b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  17 \contentsline {chapter}{\numberline {3}Zermelo-Fraenkel Set Theory}{22}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  18 \contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{22}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  19 \contentsline {section}{\numberline {3.2}The syntax of set theory}{23}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  20 \contentsline {section}{\numberline {3.3}Binding operators}{25}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  21 \contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{27}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  22 \contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{30}  465 d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  23 \contentsline {subsection}{\numberline {3.5.1}Fundamental lemmas}{30}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  24 \contentsline {subsection}{\numberline {3.5.2}Unordered pairs and finite sets}{32}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  25 \contentsline {subsection}{\numberline {3.5.3}Subset and lattice properties}{32}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  26 \contentsline {subsection}{\numberline {3.5.4}Ordered pairs}{36}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  27 \contentsline {subsection}{\numberline {3.5.5}Relations}{36}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  28 \contentsline {subsection}{\numberline {3.5.6}Functions}{37}  359 b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  29 \contentsline {section}{\numberline {3.6}Further developments}{38}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  30 \contentsline {section}{\numberline {3.7}Simplification rules}{47}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  31 \contentsline {section}{\numberline {3.8}The examples directory}{47}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  32 \contentsline {section}{\numberline {3.9}A proof about powersets}{48}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  33 \contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{51}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  34 \contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{52}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  35 \contentsline {chapter}{\numberline {4}Higher-Order Logic}{55}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  36 \contentsline {section}{\numberline {4.1}Syntax}{55}  465 d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  37 \contentsline {subsection}{\numberline {4.1.1}Types}{57}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  38 \contentsline {subsection}{\numberline {4.1.2}Binders}{58}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  39 \contentsline {subsection}{\numberline {4.1.3}The {\ptt let} and {\ptt case} constructions}{58}  359 b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  40 \contentsline {section}{\numberline {4.2}Rules of inference}{58}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  41 \contentsline {section}{\numberline {4.3}A formulation of set theory}{60}  465 d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  42 \contentsline {subsection}{\numberline {4.3.1}Syntax of set theory}{65}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  43 \contentsline {subsection}{\numberline {4.3.2}Axioms and rules of set theory}{69}  359 b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  44 \contentsline {section}{\numberline {4.4}Generic packages and classical reasoning}{71}  b5a2e9503a7a final Springer version lcp parents: 136 diff changeset  45 \contentsline {section}{\numberline {4.5}Types}{73}  465 d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  46 \contentsline {subsection}{\numberline {4.5.1}Product and sum types}{73}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  47 \contentsline {subsection}{\numberline {4.5.2}The type of natural numbers, {\ptt nat}}{73}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  48 \contentsline {subsection}{\numberline {4.5.3}The type constructor for lists, {\ptt list}}{76}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  49 \contentsline {subsection}{\numberline {4.5.4}The type constructor for lazy lists, {\ptt llist}}{76}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  50 \contentsline {section}{\numberline {4.6}Datatype declarations}{79}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  51 \contentsline {subsection}{\numberline {4.6.1}Foundations}{79}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  52 \contentsline {subsection}{\numberline {4.6.2}Defining datatypes}{80}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  53 \contentsline {subsection}{\numberline {4.6.3}Examples}{82}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  54 \contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$}{82}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  55 \contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$ with mixfix syntax}{83}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  56 \contentsline {subsubsection}{Defining functions on datatypes}{83}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  57 \contentsline {subsubsection}{A datatype for weekdays}{84}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  58 \contentsline {section}{\numberline {4.7}The examples directories}{84}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  59 \contentsline {section}{\numberline {4.8}Example: Cantor's Theorem}{85}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  60 \contentsline {chapter}{\numberline {5}First-Order Sequent Calculus}{88}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  61 \contentsline {section}{\numberline {5.1}Unification for lists}{88}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  62 \contentsline {section}{\numberline {5.2}Syntax and rules of inference}{90}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  63 \contentsline {section}{\numberline {5.3}Tactics for the cut rule}{92}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  64 \contentsline {section}{\numberline {5.4}Tactics for sequents}{93}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  65 \contentsline {section}{\numberline {5.5}Packaging sequent rules}{94}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  66 \contentsline {section}{\numberline {5.6}Proof procedures}{94}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  67 \contentsline {subsection}{\numberline {5.6.1}Method A}{95}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  68 \contentsline {subsection}{\numberline {5.6.2}Method B}{95}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  69 \contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{96}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  70 \contentsline {section}{\numberline {5.8}A more complex proof}{97}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  71 \contentsline {chapter}{\numberline {6}Constructive Type Theory}{99}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  72 \contentsline {section}{\numberline {6.1}Syntax}{101}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  73 \contentsline {section}{\numberline {6.2}Rules of inference}{101}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  74 \contentsline {section}{\numberline {6.3}Rule lists}{107}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  75 \contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{107}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  76 \contentsline {section}{\numberline {6.5}Rewriting tactics}{108}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  77 \contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{109}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  78 \contentsline {section}{\numberline {6.7}A theory of arithmetic}{111}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  79 \contentsline {section}{\numberline {6.8}The examples directory}{111}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  80 \contentsline {section}{\numberline {6.9}Example: type inference}{111}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  81 \contentsline {section}{\numberline {6.10}An example of logical reasoning}{113}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  82 \contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{116}  d4bf81734dfe Corrected HOL.tex nipkow parents: 359 diff changeset  83 \contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{117}