doc-src/Logics/logics.toc
changeset 104 d8205bb279a7
child 136 a9015b16a0e5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Logics/logics.toc	Wed Nov 10 05:00:57 1993 +0100
     1.3 @@ -0,0 +1,100 @@
     1.4 +\contentsline {chapter}{\numberline {1}Introduction}{1}
     1.5 +\contentsline {section}{\numberline {1.1}Syntax definitions}{1}
     1.6 +\contentsline {section}{\numberline {1.2}Proof procedures}{3}
     1.7 +\contentsline {chapter}{\numberline {2}First-order logic}{4}
     1.8 +\contentsline {section}{\numberline {2.1}Syntax and rules of inference}{4}
     1.9 +\contentsline {section}{\numberline {2.2}Generic packages}{8}
    1.10 +\contentsline {section}{\numberline {2.3}Intuitionistic proof procedures}{8}
    1.11 +\contentsline {section}{\numberline {2.4}Classical proof procedures}{10}
    1.12 +\contentsline {section}{\numberline {2.5}An intuitionistic example}{11}
    1.13 +\contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12}
    1.14 +\contentsline {section}{\numberline {2.7}A classical example}{14}
    1.15 +\contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{16}
    1.16 +\contentsline {subsection}{Deriving the introduction rule}{17}
    1.17 +\contentsline {subsection}{Deriving the elimination rule}{17}
    1.18 +\contentsline {subsection}{Using the derived rules}{18}
    1.19 +\contentsline {subsection}{Derived rules versus definitions}{20}
    1.20 +\contentsline {chapter}{\numberline {3}Zermelo-Fraenkel set theory}{23}
    1.21 +\contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{23}
    1.22 +\contentsline {section}{\numberline {3.2}The syntax of set theory}{25}
    1.23 +\contentsline {section}{\numberline {3.3}Binding operators}{25}
    1.24 +\contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{28}
    1.25 +\contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{33}
    1.26 +\contentsline {subsection}{Fundamental lemmas}{33}
    1.27 +\contentsline {subsection}{Unordered pairs and finite sets}{36}
    1.28 +\contentsline {subsection}{Subset and lattice properties}{36}
    1.29 +\contentsline {subsection}{Ordered pairs}{37}
    1.30 +\contentsline {subsection}{Relations}{37}
    1.31 +\contentsline {subsection}{Functions}{40}
    1.32 +\contentsline {section}{\numberline {3.6}Further developments}{40}
    1.33 +\contentsline {section}{\numberline {3.7}Simplification rules}{47}
    1.34 +\contentsline {section}{\numberline {3.8}The examples directory}{48}
    1.35 +\contentsline {section}{\numberline {3.9}A proof about powersets}{49}
    1.36 +\contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{51}
    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}{55}
    1.41 +\contentsline {subsection}{Binders}{58}
    1.42 +\contentsline {section}{\numberline {4.2}Rules of inference}{58}
    1.43 +\contentsline {section}{\numberline {4.3}Generic packages}{62}
    1.44 +\contentsline {section}{\numberline {4.4}A formulation of set theory}{63}
    1.45 +\contentsline {subsection}{Syntax of set theory}{63}
    1.46 +\contentsline {subsection}{Axioms and rules of set theory}{69}
    1.47 +\contentsline {subsection}{Derived rules for sets}{69}
    1.48 +\contentsline {section}{\numberline {4.5}Types}{69}
    1.49 +\contentsline {subsection}{Product and sum types}{74}
    1.50 +\contentsline {subsection}{The type of natural numbers, $nat$}{74}
    1.51 +\contentsline {subsection}{The type constructor for lists, $\alpha \pcomma list$}{74}
    1.52 +\contentsline {subsection}{The type constructor for lazy lists, $\alpha \pcomma llist$}{78}
    1.53 +\contentsline {section}{\numberline {4.6}Classical proof procedures}{78}
    1.54 +\contentsline {section}{\numberline {4.7}The examples directory}{78}
    1.55 +\contentsline {section}{\numberline {4.8}Example: deriving the conjunction rules}{79}
    1.56 +\contentsline {subsection}{The introduction rule}{79}
    1.57 +\contentsline {subsection}{The elimination rule}{80}
    1.58 +\contentsline {section}{\numberline {4.9}Example: Cantor's Theorem}{81}
    1.59 +\contentsline {chapter}{\numberline {5}First-order sequent calculus}{83}
    1.60 +\contentsline {section}{\numberline {5.1}Unification for lists}{83}
    1.61 +\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{84}
    1.62 +\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{84}
    1.63 +\contentsline {section}{\numberline {5.4}Tactics for sequents}{88}
    1.64 +\contentsline {section}{\numberline {5.5}Packaging sequent rules}{89}
    1.65 +\contentsline {section}{\numberline {5.6}Proof procedures}{89}
    1.66 +\contentsline {subsection}{Method A}{90}
    1.67 +\contentsline {subsection}{Method B}{90}
    1.68 +\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{91}
    1.69 +\contentsline {section}{\numberline {5.8}A more complex proof}{92}
    1.70 +\contentsline {chapter}{\numberline {6}Constructive Type Theory}{95}
    1.71 +\contentsline {section}{\numberline {6.1}Syntax}{96}
    1.72 +\contentsline {section}{\numberline {6.2}Rules of inference}{96}
    1.73 +\contentsline {section}{\numberline {6.3}Rule lists}{101}
    1.74 +\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{104}
    1.75 +\contentsline {section}{\numberline {6.5}Rewriting tactics}{105}
    1.76 +\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{105}
    1.77 +\contentsline {section}{\numberline {6.7}A theory of arithmetic}{106}
    1.78 +\contentsline {section}{\numberline {6.8}The examples directory}{106}
    1.79 +\contentsline {section}{\numberline {6.9}Example: type inference}{108}
    1.80 +\contentsline {section}{\numberline {6.10}An example of logical reasoning}{109}
    1.81 +\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{112}
    1.82 +\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{113}
    1.83 +\contentsline {chapter}{\numberline {7}Defining Logics}{118}
    1.84 +\contentsline {section}{\numberline {7.1}Precedence grammars}{118}
    1.85 +\contentsline {section}{\numberline {7.2}Basic syntax}{119}
    1.86 +\contentsline {subsection}{Logical types and default syntax}{120}
    1.87 +\contentsline {subsection}{Lexical matters *}{121}
    1.88 +\contentsline {subsection}{Inspecting syntax *}{121}
    1.89 +\contentsline {section}{\numberline {7.3}Abstract syntax trees}{123}
    1.90 +\contentsline {subsection}{Parse trees to asts}{125}
    1.91 +\contentsline {subsection}{Asts to terms *}{126}
    1.92 +\contentsline {subsection}{Printing of terms *}{126}
    1.93 +\contentsline {section}{\numberline {7.4}Mixfix declarations}{128}
    1.94 +\contentsline {subsection}{Infixes}{130}
    1.95 +\contentsline {subsection}{Binders}{130}
    1.96 +\contentsline {section}{\numberline {7.5}Syntactic translations (macros)}{131}
    1.97 +\contentsline {subsection}{Specifying macros}{132}
    1.98 +\contentsline {subsection}{Applying rules}{133}
    1.99 +\contentsline {subsection}{Rewriting strategy}{135}
   1.100 +\contentsline {subsection}{More examples}{135}
   1.101 +\contentsline {section}{\numberline {7.6}Translation functions *}{138}
   1.102 +\contentsline {subsection}{A simple example *}{139}
   1.103 +\contentsline {section}{\numberline {7.7}Example: some minimal logics}{140}