doc-src/Logics/logics.toc
 author wenzelm Mon Nov 22 11:28:25 1993 +0100 (1993-11-22) changeset 136 a9015b16a0e5 parent 104 d8205bb279a7 child 359 b5a2e9503a7a permissions -rw-r--r--
*** empty log message ***
     1 \contentsline {chapter}{\numberline {1}Introduction}{1}

     2 \contentsline {section}{\numberline {1.1}Syntax definitions}{1}

     3 \contentsline {section}{\numberline {1.2}Proof procedures}{3}

     4 \contentsline {chapter}{\numberline {2}First-order logic}{4}

     5 \contentsline {section}{\numberline {2.1}Syntax and rules of inference}{4}

     6 \contentsline {section}{\numberline {2.2}Generic packages}{8}

     7 \contentsline {section}{\numberline {2.3}Intuitionistic proof procedures}{8}

     8 \contentsline {section}{\numberline {2.4}Classical proof procedures}{10}

     9 \contentsline {section}{\numberline {2.5}An intuitionistic example}{11}

    10 \contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12}

    11 \contentsline {section}{\numberline {2.7}A classical example}{14}

    12 \contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{16}

    13 \contentsline {subsection}{Deriving the introduction rule}{17}

    14 \contentsline {subsection}{Deriving the elimination rule}{17}

    15 \contentsline {subsection}{Using the derived rules}{18}

    16 \contentsline {subsection}{Derived rules versus definitions}{20}

    17 \contentsline {chapter}{\numberline {3}Zermelo-Fraenkel set theory}{23}

    18 \contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{23}

    19 \contentsline {section}{\numberline {3.2}The syntax of set theory}{24}

    20 \contentsline {section}{\numberline {3.3}Binding operators}{26}

    21 \contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{28}

    22 \contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{33}

    23 \contentsline {subsection}{Fundamental lemmas}{34}

    24 \contentsline {subsection}{Unordered pairs and finite sets}{34}

    25 \contentsline {subsection}{Subset and lattice properties}{37}

    26 \contentsline {subsection}{Ordered pairs}{37}

    27 \contentsline {subsection}{Relations}{37}

    28 \contentsline {subsection}{Functions}{38}

    29 \contentsline {section}{\numberline {3.6}Further developments}{41}

    30 \contentsline {section}{\numberline {3.7}Simplification rules}{49}

    31 \contentsline {section}{\numberline {3.8}The examples directory}{49}

    32 \contentsline {section}{\numberline {3.9}A proof about powersets}{52}

    33 \contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{54}

    34 \contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{55}

    35 \contentsline {chapter}{\numberline {4}Higher-order logic}{58}

    36 \contentsline {section}{\numberline {4.1}Syntax}{58}

    37 \contentsline {subsection}{Types}{58}

    38 \contentsline {subsection}{Binders}{61}

    39 \contentsline {section}{\numberline {4.2}Rules of inference}{61}

    40 \contentsline {section}{\numberline {4.3}Generic packages}{65}

    41 \contentsline {section}{\numberline {4.4}A formulation of set theory}{66}

    42 \contentsline {subsection}{Syntax of set theory}{66}

    43 \contentsline {subsection}{Axioms and rules of set theory}{72}

    44 \contentsline {subsection}{Derived rules for sets}{72}

    45 \contentsline {section}{\numberline {4.5}Types}{72}

    46 \contentsline {subsection}{Product and sum types}{77}

    47 \contentsline {subsection}{The type of natural numbers, $nat$}{77}

    48 \contentsline {subsection}{The type constructor for lists, $\alpha \pcomma list$}{77}

    49 \contentsline {subsection}{The type constructor for lazy lists, $\alpha \pcomma llist$}{81}

    50 \contentsline {section}{\numberline {4.6}Classical proof procedures}{81}

    51 \contentsline {section}{\numberline {4.7}The examples directories}{81}

    52 \contentsline {section}{\numberline {4.8}Example: deriving the conjunction rules}{82}

    53 \contentsline {subsection}{The introduction rule}{82}

    54 \contentsline {subsection}{The elimination rule}{83}

    55 \contentsline {section}{\numberline {4.9}Example: Cantor's Theorem}{84}

    56 \contentsline {chapter}{\numberline {5}First-order sequent calculus}{87}

    57 \contentsline {section}{\numberline {5.1}Unification for lists}{87}

    58 \contentsline {section}{\numberline {5.2}Syntax and rules of inference}{88}

    59 \contentsline {section}{\numberline {5.3}Tactics for the cut rule}{88}

    60 \contentsline {section}{\numberline {5.4}Tactics for sequents}{93}

    61 \contentsline {section}{\numberline {5.5}Packaging sequent rules}{93}

    62 \contentsline {section}{\numberline {5.6}Proof procedures}{94}

    63 \contentsline {subsection}{Method A}{95}

    64 \contentsline {subsection}{Method B}{95}

    65 \contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{95}

    66 \contentsline {section}{\numberline {5.8}A more complex proof}{97}

    67 \contentsline {chapter}{\numberline {6}Constructive Type Theory}{99}

    68 \contentsline {section}{\numberline {6.1}Syntax}{100}

    69 \contentsline {section}{\numberline {6.2}Rules of inference}{100}

    70 \contentsline {section}{\numberline {6.3}Rule lists}{105}

    71 \contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{108}

    72 \contentsline {section}{\numberline {6.5}Rewriting tactics}{109}

    73 \contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{109}

    74 \contentsline {section}{\numberline {6.7}A theory of arithmetic}{110}

    75 \contentsline {section}{\numberline {6.8}The examples directory}{110}

    76 \contentsline {section}{\numberline {6.9}Example: type inference}{112}

    77 \contentsline {section}{\numberline {6.10}An example of logical reasoning}{113}

    78 \contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{116}

    79 \contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{117}

    80 \contentsline {chapter}{\numberline {7}Defining Logics}{121}

    81 \contentsline {section}{\numberline {7.1}Precedence grammars}{121}

    82 \contentsline {section}{\numberline {7.2}Basic syntax}{122}

    83 \contentsline {subsection}{Logical types and default syntax}{123}

    84 \contentsline {subsection}{Lexical matters *}{124}

    85 \contentsline {subsection}{Inspecting syntax *}{124}

    86 \contentsline {section}{\numberline {7.3}Abstract syntax trees}{126}

    87 \contentsline {subsection}{Parse trees to asts}{128}

    88 \contentsline {subsection}{Asts to terms *}{129}

    89 \contentsline {subsection}{Printing of terms *}{129}

    90 \contentsline {section}{\numberline {7.4}Mixfix declarations}{130}

    91 \contentsline {subsection}{Infixes}{133}

    92 \contentsline {subsection}{Binders}{133}

    93 \contentsline {section}{\numberline {7.5}Syntactic translations (macros)}{134}

    94 \contentsline {subsection}{Specifying macros}{135}

    95 \contentsline {subsection}{Applying rules}{136}

    96 \contentsline {subsection}{Rewriting strategy}{138}

    97 \contentsline {subsection}{More examples}{138}

    98 \contentsline {section}{\numberline {7.6}Translation functions *}{141}

    99 \contentsline {subsection}{A simple example *}{142}

   100 \contentsline {section}{\numberline {7.7}Example: some minimal logics}{143}