doc-src/Logics/logics.toc
 changeset 136 a9015b16a0e5 parent 104 d8205bb279a7 child 359 b5a2e9503a7a
     1.1 --- a/doc-src/Logics/logics.toc	Mon Nov 22 11:27:04 1993 +0100
1.2 +++ b/doc-src/Logics/logics.toc	Mon Nov 22 11:28:25 1993 +0100
1.3 @@ -16,85 +16,85 @@
1.4  \contentsline {subsection}{Derived rules versus definitions}{20}
1.5  \contentsline {chapter}{\numberline {3}Zermelo-Fraenkel set theory}{23}
1.6  \contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{23}
1.7 -\contentsline {section}{\numberline {3.2}The syntax of set theory}{25}
1.8 -\contentsline {section}{\numberline {3.3}Binding operators}{25}
1.9 +\contentsline {section}{\numberline {3.2}The syntax of set theory}{24}
1.10 +\contentsline {section}{\numberline {3.3}Binding operators}{26}
1.11  \contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{28}
1.12  \contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{33}
1.13 -\contentsline {subsection}{Fundamental lemmas}{33}
1.14 -\contentsline {subsection}{Unordered pairs and finite sets}{36}
1.15 -\contentsline {subsection}{Subset and lattice properties}{36}
1.16 +\contentsline {subsection}{Fundamental lemmas}{34}
1.17 +\contentsline {subsection}{Unordered pairs and finite sets}{34}
1.18 +\contentsline {subsection}{Subset and lattice properties}{37}
1.19  \contentsline {subsection}{Ordered pairs}{37}
1.20  \contentsline {subsection}{Relations}{37}
1.21 -\contentsline {subsection}{Functions}{40}
1.22 -\contentsline {section}{\numberline {3.6}Further developments}{40}
1.23 -\contentsline {section}{\numberline {3.7}Simplification rules}{47}
1.24 -\contentsline {section}{\numberline {3.8}The examples directory}{48}
1.25 -\contentsline {section}{\numberline {3.9}A proof about powersets}{49}
1.26 -\contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{51}
1.27 -\contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{52}
1.28 -\contentsline {chapter}{\numberline {4}Higher-order logic}{55}
1.29 -\contentsline {section}{\numberline {4.1}Syntax}{55}
1.30 -\contentsline {subsection}{Types}{55}
1.31 -\contentsline {subsection}{Binders}{58}
1.32 -\contentsline {section}{\numberline {4.2}Rules of inference}{58}
1.33 -\contentsline {section}{\numberline {4.3}Generic packages}{62}
1.34 -\contentsline {section}{\numberline {4.4}A formulation of set theory}{63}
1.35 -\contentsline {subsection}{Syntax of set theory}{63}
1.36 -\contentsline {subsection}{Axioms and rules of set theory}{69}
1.37 -\contentsline {subsection}{Derived rules for sets}{69}
1.38 -\contentsline {section}{\numberline {4.5}Types}{69}
1.39 -\contentsline {subsection}{Product and sum types}{74}
1.40 -\contentsline {subsection}{The type of natural numbers, $nat$}{74}
1.41 -\contentsline {subsection}{The type constructor for lists, $\alpha \pcomma list$}{74}
1.42 -\contentsline {subsection}{The type constructor for lazy lists, $\alpha \pcomma llist$}{78}
1.43 -\contentsline {section}{\numberline {4.6}Classical proof procedures}{78}
1.44 -\contentsline {section}{\numberline {4.7}The examples directory}{78}
1.45 -\contentsline {section}{\numberline {4.8}Example: deriving the conjunction rules}{79}
1.46 -\contentsline {subsection}{The introduction rule}{79}
1.47 -\contentsline {subsection}{The elimination rule}{80}
1.48 -\contentsline {section}{\numberline {4.9}Example: Cantor's Theorem}{81}
1.49 -\contentsline {chapter}{\numberline {5}First-order sequent calculus}{83}
1.50 -\contentsline {section}{\numberline {5.1}Unification for lists}{83}
1.51 -\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{84}
1.52 -\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{84}
1.53 -\contentsline {section}{\numberline {5.4}Tactics for sequents}{88}
1.54 -\contentsline {section}{\numberline {5.5}Packaging sequent rules}{89}
1.55 -\contentsline {section}{\numberline {5.6}Proof procedures}{89}
1.56 -\contentsline {subsection}{Method A}{90}
1.57 -\contentsline {subsection}{Method B}{90}
1.58 -\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{91}
1.59 -\contentsline {section}{\numberline {5.8}A more complex proof}{92}
1.60 -\contentsline {chapter}{\numberline {6}Constructive Type Theory}{95}
1.61 -\contentsline {section}{\numberline {6.1}Syntax}{96}
1.62 -\contentsline {section}{\numberline {6.2}Rules of inference}{96}
1.63 -\contentsline {section}{\numberline {6.3}Rule lists}{101}
1.64 -\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{104}
1.65 -\contentsline {section}{\numberline {6.5}Rewriting tactics}{105}
1.66 -\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{105}
1.67 -\contentsline {section}{\numberline {6.7}A theory of arithmetic}{106}
1.68 -\contentsline {section}{\numberline {6.8}The examples directory}{106}
1.69 -\contentsline {section}{\numberline {6.9}Example: type inference}{108}
1.70 -\contentsline {section}{\numberline {6.10}An example of logical reasoning}{109}
1.71 -\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{112}
1.72 -\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{113}
1.73 -\contentsline {chapter}{\numberline {7}Defining Logics}{118}
1.74 -\contentsline {section}{\numberline {7.1}Precedence grammars}{118}
1.75 -\contentsline {section}{\numberline {7.2}Basic syntax}{119}
1.76 -\contentsline {subsection}{Logical types and default syntax}{120}
1.77 -\contentsline {subsection}{Lexical matters *}{121}
1.78 -\contentsline {subsection}{Inspecting syntax *}{121}
1.79 -\contentsline {section}{\numberline {7.3}Abstract syntax trees}{123}
1.80 -\contentsline {subsection}{Parse trees to asts}{125}
1.81 -\contentsline {subsection}{Asts to terms *}{126}
1.82 -\contentsline {subsection}{Printing of terms *}{126}
1.83 -\contentsline {section}{\numberline {7.4}Mixfix declarations}{128}
1.84 -\contentsline {subsection}{Infixes}{130}
1.85 -\contentsline {subsection}{Binders}{130}
1.86 -\contentsline {section}{\numberline {7.5}Syntactic translations (macros)}{131}
1.87 -\contentsline {subsection}{Specifying macros}{132}
1.88 -\contentsline {subsection}{Applying rules}{133}
1.89 -\contentsline {subsection}{Rewriting strategy}{135}
1.90 -\contentsline {subsection}{More examples}{135}
1.91 -\contentsline {section}{\numberline {7.6}Translation functions *}{138}
1.92 -\contentsline {subsection}{A simple example *}{139}
1.93 -\contentsline {section}{\numberline {7.7}Example: some minimal logics}{140}
1.94 +\contentsline {subsection}{Functions}{38}
1.95 +\contentsline {section}{\numberline {3.6}Further developments}{41}
1.96 +\contentsline {section}{\numberline {3.7}Simplification rules}{49}
1.97 +\contentsline {section}{\numberline {3.8}The examples directory}{49}
1.98 +\contentsline {section}{\numberline {3.9}A proof about powersets}{52}
1.99 +\contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{54}
1.100 +\contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{55}
1.101 +\contentsline {chapter}{\numberline {4}Higher-order logic}{58}
1.102 +\contentsline {section}{\numberline {4.1}Syntax}{58}
1.103 +\contentsline {subsection}{Types}{58}
1.104 +\contentsline {subsection}{Binders}{61}
1.105 +\contentsline {section}{\numberline {4.2}Rules of inference}{61}
1.106 +\contentsline {section}{\numberline {4.3}Generic packages}{65}
1.107 +\contentsline {section}{\numberline {4.4}A formulation of set theory}{66}
1.108 +\contentsline {subsection}{Syntax of set theory}{66}
1.109 +\contentsline {subsection}{Axioms and rules of set theory}{72}
1.110 +\contentsline {subsection}{Derived rules for sets}{72}
1.111 +\contentsline {section}{\numberline {4.5}Types}{72}
1.112 +\contentsline {subsection}{Product and sum types}{77}
1.113 +\contentsline {subsection}{The type of natural numbers, $nat$}{77}
1.114 +\contentsline {subsection}{The type constructor for lists, $\alpha \pcomma list$}{77}
1.115 +\contentsline {subsection}{The type constructor for lazy lists, $\alpha \pcomma llist$}{81}
1.116 +\contentsline {section}{\numberline {4.6}Classical proof procedures}{81}
1.117 +\contentsline {section}{\numberline {4.7}The examples directories}{81}
1.118 +\contentsline {section}{\numberline {4.8}Example: deriving the conjunction rules}{82}
1.119 +\contentsline {subsection}{The introduction rule}{82}
1.120 +\contentsline {subsection}{The elimination rule}{83}
1.121 +\contentsline {section}{\numberline {4.9}Example: Cantor's Theorem}{84}
1.122 +\contentsline {chapter}{\numberline {5}First-order sequent calculus}{87}
1.123 +\contentsline {section}{\numberline {5.1}Unification for lists}{87}
1.124 +\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{88}
1.125 +\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{88}
1.126 +\contentsline {section}{\numberline {5.4}Tactics for sequents}{93}
1.127 +\contentsline {section}{\numberline {5.5}Packaging sequent rules}{93}
1.128 +\contentsline {section}{\numberline {5.6}Proof procedures}{94}
1.129 +\contentsline {subsection}{Method A}{95}
1.130 +\contentsline {subsection}{Method B}{95}
1.131 +\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{95}
1.132 +\contentsline {section}{\numberline {5.8}A more complex proof}{97}
1.133 +\contentsline {chapter}{\numberline {6}Constructive Type Theory}{99}
1.134 +\contentsline {section}{\numberline {6.1}Syntax}{100}
1.135 +\contentsline {section}{\numberline {6.2}Rules of inference}{100}
1.136 +\contentsline {section}{\numberline {6.3}Rule lists}{105}
1.137 +\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{108}
1.138 +\contentsline {section}{\numberline {6.5}Rewriting tactics}{109}
1.139 +\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{109}
1.140 +\contentsline {section}{\numberline {6.7}A theory of arithmetic}{110}
1.141 +\contentsline {section}{\numberline {6.8}The examples directory}{110}
1.142 +\contentsline {section}{\numberline {6.9}Example: type inference}{112}
1.143 +\contentsline {section}{\numberline {6.10}An example of logical reasoning}{113}
1.144 +\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{116}
1.145 +\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{117}
1.146 +\contentsline {chapter}{\numberline {7}Defining Logics}{121}
1.147 +\contentsline {section}{\numberline {7.1}Precedence grammars}{121}
1.148 +\contentsline {section}{\numberline {7.2}Basic syntax}{122}
1.149 +\contentsline {subsection}{Logical types and default syntax}{123}
1.150 +\contentsline {subsection}{Lexical matters *}{124}
1.151 +\contentsline {subsection}{Inspecting syntax *}{124}
1.152 +\contentsline {section}{\numberline {7.3}Abstract syntax trees}{126}
1.153 +\contentsline {subsection}{Parse trees to asts}{128}
1.154 +\contentsline {subsection}{Asts to terms *}{129}
1.155 +\contentsline {subsection}{Printing of terms *}{129}
1.156 +\contentsline {section}{\numberline {7.4}Mixfix declarations}{130}
1.157 +\contentsline {subsection}{Infixes}{133}
1.158 +\contentsline {subsection}{Binders}{133}
1.159 +\contentsline {section}{\numberline {7.5}Syntactic translations (macros)}{134}
1.160 +\contentsline {subsection}{Specifying macros}{135}
1.161 +\contentsline {subsection}{Applying rules}{136}
1.162 +\contentsline {subsection}{Rewriting strategy}{138}
1.163 +\contentsline {subsection}{More examples}{138}
1.164 +\contentsline {section}{\numberline {7.6}Translation functions *}{141}
1.165 +\contentsline {subsection}{A simple example *}{142}
1.166 +\contentsline {section}{\numberline {7.7}Example: some minimal logics}{143}