doc-src/Logics/logics.toc
changeset 465 d4bf81734dfe
parent 359 b5a2e9503a7a
     1.1 --- a/doc-src/Logics/logics.toc	Tue Jul 12 09:28:00 1994 +0200
     1.2 +++ b/doc-src/Logics/logics.toc	Tue Jul 12 12:49:15 1994 +0200
     1.3 @@ -10,22 +10,22 @@
     1.4  \contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12}
     1.5  \contentsline {section}{\numberline {2.7}A classical example}{14}
     1.6  \contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{15}
     1.7 -\contentsline {subsection}{Deriving the introduction rule}{16}
     1.8 -\contentsline {subsection}{Deriving the elimination rule}{17}
     1.9 -\contentsline {subsection}{Using the derived rules}{17}
    1.10 -\contentsline {subsection}{Derived rules versus definitions}{19}
    1.11 +\contentsline {subsection}{\numberline {2.8.1}Deriving the introduction rule}{16}
    1.12 +\contentsline {subsection}{\numberline {2.8.2}Deriving the elimination rule}{17}
    1.13 +\contentsline {subsection}{\numberline {2.8.3}Using the derived rules}{17}
    1.14 +\contentsline {subsection}{\numberline {2.8.4}Derived rules versus definitions}{19}
    1.15  \contentsline {chapter}{\numberline {3}Zermelo-Fraenkel Set Theory}{22}
    1.16  \contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{22}
    1.17  \contentsline {section}{\numberline {3.2}The syntax of set theory}{23}
    1.18  \contentsline {section}{\numberline {3.3}Binding operators}{25}
    1.19  \contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{27}
    1.20  \contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{30}
    1.21 -\contentsline {subsection}{Fundamental lemmas}{30}
    1.22 -\contentsline {subsection}{Unordered pairs and finite sets}{32}
    1.23 -\contentsline {subsection}{Subset and lattice properties}{32}
    1.24 -\contentsline {subsection}{Ordered pairs}{36}
    1.25 -\contentsline {subsection}{Relations}{36}
    1.26 -\contentsline {subsection}{Functions}{37}
    1.27 +\contentsline {subsection}{\numberline {3.5.1}Fundamental lemmas}{30}
    1.28 +\contentsline {subsection}{\numberline {3.5.2}Unordered pairs and finite sets}{32}
    1.29 +\contentsline {subsection}{\numberline {3.5.3}Subset and lattice properties}{32}
    1.30 +\contentsline {subsection}{\numberline {3.5.4}Ordered pairs}{36}
    1.31 +\contentsline {subsection}{\numberline {3.5.5}Relations}{36}
    1.32 +\contentsline {subsection}{\numberline {3.5.6}Functions}{37}
    1.33  \contentsline {section}{\numberline {3.6}Further developments}{38}
    1.34  \contentsline {section}{\numberline {3.7}Simplification rules}{47}
    1.35  \contentsline {section}{\numberline {3.8}The examples directory}{47}
    1.36 @@ -34,42 +34,50 @@
    1.37  \contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{52}
    1.38  \contentsline {chapter}{\numberline {4}Higher-Order Logic}{55}
    1.39  \contentsline {section}{\numberline {4.1}Syntax}{55}
    1.40 -\contentsline {subsection}{Types}{57}
    1.41 -\contentsline {subsection}{Binders}{58}
    1.42 -\contentsline {subsection}{The {\ptt let} and {\ptt case} constructions}{58}
    1.43 +\contentsline {subsection}{\numberline {4.1.1}Types}{57}
    1.44 +\contentsline {subsection}{\numberline {4.1.2}Binders}{58}
    1.45 +\contentsline {subsection}{\numberline {4.1.3}The {\ptt let} and {\ptt case} constructions}{58}
    1.46  \contentsline {section}{\numberline {4.2}Rules of inference}{58}
    1.47  \contentsline {section}{\numberline {4.3}A formulation of set theory}{60}
    1.48 -\contentsline {subsection}{Syntax of set theory}{65}
    1.49 -\contentsline {subsection}{Axioms and rules of set theory}{69}
    1.50 +\contentsline {subsection}{\numberline {4.3.1}Syntax of set theory}{65}
    1.51 +\contentsline {subsection}{\numberline {4.3.2}Axioms and rules of set theory}{69}
    1.52  \contentsline {section}{\numberline {4.4}Generic packages and classical reasoning}{71}
    1.53  \contentsline {section}{\numberline {4.5}Types}{73}
    1.54 -\contentsline {subsection}{Product and sum types}{73}
    1.55 -\contentsline {subsection}{The type of natural numbers, {\ptt nat}}{73}
    1.56 -\contentsline {subsection}{The type constructor for lists, {\ptt list}}{76}
    1.57 -\contentsline {subsection}{The type constructor for lazy lists, {\ptt llist}}{76}
    1.58 -\contentsline {section}{\numberline {4.6}The examples directories}{79}
    1.59 -\contentsline {section}{\numberline {4.7}Example: Cantor's Theorem}{80}
    1.60 -\contentsline {chapter}{\numberline {5}First-Order Sequent Calculus}{82}
    1.61 -\contentsline {section}{\numberline {5.1}Unification for lists}{82}
    1.62 -\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{84}
    1.63 -\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{86}
    1.64 -\contentsline {section}{\numberline {5.4}Tactics for sequents}{87}
    1.65 -\contentsline {section}{\numberline {5.5}Packaging sequent rules}{88}
    1.66 -\contentsline {section}{\numberline {5.6}Proof procedures}{88}
    1.67 -\contentsline {subsection}{Method A}{89}
    1.68 -\contentsline {subsection}{Method B}{89}
    1.69 -\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{90}
    1.70 -\contentsline {section}{\numberline {5.8}A more complex proof}{91}
    1.71 -\contentsline {chapter}{\numberline {6}Constructive Type Theory}{93}
    1.72 -\contentsline {section}{\numberline {6.1}Syntax}{95}
    1.73 -\contentsline {section}{\numberline {6.2}Rules of inference}{95}
    1.74 -\contentsline {section}{\numberline {6.3}Rule lists}{101}
    1.75 -\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{101}
    1.76 -\contentsline {section}{\numberline {6.5}Rewriting tactics}{102}
    1.77 -\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{103}
    1.78 -\contentsline {section}{\numberline {6.7}A theory of arithmetic}{105}
    1.79 -\contentsline {section}{\numberline {6.8}The examples directory}{105}
    1.80 -\contentsline {section}{\numberline {6.9}Example: type inference}{105}
    1.81 -\contentsline {section}{\numberline {6.10}An example of logical reasoning}{107}
    1.82 -\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{110}
    1.83 -\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{111}
    1.84 +\contentsline {subsection}{\numberline {4.5.1}Product and sum types}{73}
    1.85 +\contentsline {subsection}{\numberline {4.5.2}The type of natural numbers, {\ptt nat}}{73}
    1.86 +\contentsline {subsection}{\numberline {4.5.3}The type constructor for lists, {\ptt list}}{76}
    1.87 +\contentsline {subsection}{\numberline {4.5.4}The type constructor for lazy lists, {\ptt llist}}{76}
    1.88 +\contentsline {section}{\numberline {4.6}Datatype declarations}{79}
    1.89 +\contentsline {subsection}{\numberline {4.6.1}Foundations}{79}
    1.90 +\contentsline {subsection}{\numberline {4.6.2}Defining datatypes}{80}
    1.91 +\contentsline {subsection}{\numberline {4.6.3}Examples}{82}
    1.92 +\contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$}{82}
    1.93 +\contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$ with mixfix syntax}{83}
    1.94 +\contentsline {subsubsection}{Defining functions on datatypes}{83}
    1.95 +\contentsline {subsubsection}{A datatype for weekdays}{84}
    1.96 +\contentsline {section}{\numberline {4.7}The examples directories}{84}
    1.97 +\contentsline {section}{\numberline {4.8}Example: Cantor's Theorem}{85}
    1.98 +\contentsline {chapter}{\numberline {5}First-Order Sequent Calculus}{88}
    1.99 +\contentsline {section}{\numberline {5.1}Unification for lists}{88}
   1.100 +\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{90}
   1.101 +\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{92}
   1.102 +\contentsline {section}{\numberline {5.4}Tactics for sequents}{93}
   1.103 +\contentsline {section}{\numberline {5.5}Packaging sequent rules}{94}
   1.104 +\contentsline {section}{\numberline {5.6}Proof procedures}{94}
   1.105 +\contentsline {subsection}{\numberline {5.6.1}Method A}{95}
   1.106 +\contentsline {subsection}{\numberline {5.6.2}Method B}{95}
   1.107 +\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{96}
   1.108 +\contentsline {section}{\numberline {5.8}A more complex proof}{97}
   1.109 +\contentsline {chapter}{\numberline {6}Constructive Type Theory}{99}
   1.110 +\contentsline {section}{\numberline {6.1}Syntax}{101}
   1.111 +\contentsline {section}{\numberline {6.2}Rules of inference}{101}
   1.112 +\contentsline {section}{\numberline {6.3}Rule lists}{107}
   1.113 +\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{107}
   1.114 +\contentsline {section}{\numberline {6.5}Rewriting tactics}{108}
   1.115 +\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{109}
   1.116 +\contentsline {section}{\numberline {6.7}A theory of arithmetic}{111}
   1.117 +\contentsline {section}{\numberline {6.8}The examples directory}{111}
   1.118 +\contentsline {section}{\numberline {6.9}Example: type inference}{111}
   1.119 +\contentsline {section}{\numberline {6.10}An example of logical reasoning}{113}
   1.120 +\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{116}
   1.121 +\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{117}