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