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 ***
lcp@104
     1
\contentsline {chapter}{\numberline {1}Introduction}{1}
lcp@104
     2
\contentsline {section}{\numberline {1.1}Syntax definitions}{1}
lcp@104
     3
\contentsline {section}{\numberline {1.2}Proof procedures}{3}
lcp@104
     4
\contentsline {chapter}{\numberline {2}First-order logic}{4}
lcp@104
     5
\contentsline {section}{\numberline {2.1}Syntax and rules of inference}{4}
lcp@104
     6
\contentsline {section}{\numberline {2.2}Generic packages}{8}
lcp@104
     7
\contentsline {section}{\numberline {2.3}Intuitionistic proof procedures}{8}
lcp@104
     8
\contentsline {section}{\numberline {2.4}Classical proof procedures}{10}
lcp@104
     9
\contentsline {section}{\numberline {2.5}An intuitionistic example}{11}
lcp@104
    10
\contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12}
lcp@104
    11
\contentsline {section}{\numberline {2.7}A classical example}{14}
lcp@104
    12
\contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{16}
lcp@104
    13
\contentsline {subsection}{Deriving the introduction rule}{17}
lcp@104
    14
\contentsline {subsection}{Deriving the elimination rule}{17}
lcp@104
    15
\contentsline {subsection}{Using the derived rules}{18}
lcp@104
    16
\contentsline {subsection}{Derived rules versus definitions}{20}
lcp@104
    17
\contentsline {chapter}{\numberline {3}Zermelo-Fraenkel set theory}{23}
lcp@104
    18
\contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{23}
wenzelm@136
    19
\contentsline {section}{\numberline {3.2}The syntax of set theory}{24}
wenzelm@136
    20
\contentsline {section}{\numberline {3.3}Binding operators}{26}
lcp@104
    21
\contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{28}
lcp@104
    22
\contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{33}
wenzelm@136
    23
\contentsline {subsection}{Fundamental lemmas}{34}
wenzelm@136
    24
\contentsline {subsection}{Unordered pairs and finite sets}{34}
wenzelm@136
    25
\contentsline {subsection}{Subset and lattice properties}{37}
lcp@104
    26
\contentsline {subsection}{Ordered pairs}{37}
lcp@104
    27
\contentsline {subsection}{Relations}{37}
wenzelm@136
    28
\contentsline {subsection}{Functions}{38}
wenzelm@136
    29
\contentsline {section}{\numberline {3.6}Further developments}{41}
wenzelm@136
    30
\contentsline {section}{\numberline {3.7}Simplification rules}{49}
wenzelm@136
    31
\contentsline {section}{\numberline {3.8}The examples directory}{49}
wenzelm@136
    32
\contentsline {section}{\numberline {3.9}A proof about powersets}{52}
wenzelm@136
    33
\contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{54}
wenzelm@136
    34
\contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{55}
wenzelm@136
    35
\contentsline {chapter}{\numberline {4}Higher-order logic}{58}
wenzelm@136
    36
\contentsline {section}{\numberline {4.1}Syntax}{58}
wenzelm@136
    37
\contentsline {subsection}{Types}{58}
wenzelm@136
    38
\contentsline {subsection}{Binders}{61}
wenzelm@136
    39
\contentsline {section}{\numberline {4.2}Rules of inference}{61}
wenzelm@136
    40
\contentsline {section}{\numberline {4.3}Generic packages}{65}
wenzelm@136
    41
\contentsline {section}{\numberline {4.4}A formulation of set theory}{66}
wenzelm@136
    42
\contentsline {subsection}{Syntax of set theory}{66}
wenzelm@136
    43
\contentsline {subsection}{Axioms and rules of set theory}{72}
wenzelm@136
    44
\contentsline {subsection}{Derived rules for sets}{72}
wenzelm@136
    45
\contentsline {section}{\numberline {4.5}Types}{72}
wenzelm@136
    46
\contentsline {subsection}{Product and sum types}{77}
wenzelm@136
    47
\contentsline {subsection}{The type of natural numbers, $nat$}{77}
wenzelm@136
    48
\contentsline {subsection}{The type constructor for lists, $\alpha \pcomma list$}{77}
wenzelm@136
    49
\contentsline {subsection}{The type constructor for lazy lists, $\alpha \pcomma llist$}{81}
wenzelm@136
    50
\contentsline {section}{\numberline {4.6}Classical proof procedures}{81}
wenzelm@136
    51
\contentsline {section}{\numberline {4.7}The examples directories}{81}
wenzelm@136
    52
\contentsline {section}{\numberline {4.8}Example: deriving the conjunction rules}{82}
wenzelm@136
    53
\contentsline {subsection}{The introduction rule}{82}
wenzelm@136
    54
\contentsline {subsection}{The elimination rule}{83}
wenzelm@136
    55
\contentsline {section}{\numberline {4.9}Example: Cantor's Theorem}{84}
wenzelm@136
    56
\contentsline {chapter}{\numberline {5}First-order sequent calculus}{87}
wenzelm@136
    57
\contentsline {section}{\numberline {5.1}Unification for lists}{87}
wenzelm@136
    58
\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{88}
wenzelm@136
    59
\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{88}
wenzelm@136
    60
\contentsline {section}{\numberline {5.4}Tactics for sequents}{93}
wenzelm@136
    61
\contentsline {section}{\numberline {5.5}Packaging sequent rules}{93}
wenzelm@136
    62
\contentsline {section}{\numberline {5.6}Proof procedures}{94}
wenzelm@136
    63
\contentsline {subsection}{Method A}{95}
wenzelm@136
    64
\contentsline {subsection}{Method B}{95}
wenzelm@136
    65
\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{95}
wenzelm@136
    66
\contentsline {section}{\numberline {5.8}A more complex proof}{97}
wenzelm@136
    67
\contentsline {chapter}{\numberline {6}Constructive Type Theory}{99}
wenzelm@136
    68
\contentsline {section}{\numberline {6.1}Syntax}{100}
wenzelm@136
    69
\contentsline {section}{\numberline {6.2}Rules of inference}{100}
wenzelm@136
    70
\contentsline {section}{\numberline {6.3}Rule lists}{105}
wenzelm@136
    71
\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{108}
wenzelm@136
    72
\contentsline {section}{\numberline {6.5}Rewriting tactics}{109}
wenzelm@136
    73
\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{109}
wenzelm@136
    74
\contentsline {section}{\numberline {6.7}A theory of arithmetic}{110}
wenzelm@136
    75
\contentsline {section}{\numberline {6.8}The examples directory}{110}
wenzelm@136
    76
\contentsline {section}{\numberline {6.9}Example: type inference}{112}
wenzelm@136
    77
\contentsline {section}{\numberline {6.10}An example of logical reasoning}{113}
wenzelm@136
    78
\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{116}
wenzelm@136
    79
\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{117}
wenzelm@136
    80
\contentsline {chapter}{\numberline {7}Defining Logics}{121}
wenzelm@136
    81
\contentsline {section}{\numberline {7.1}Precedence grammars}{121}
wenzelm@136
    82
\contentsline {section}{\numberline {7.2}Basic syntax}{122}
wenzelm@136
    83
\contentsline {subsection}{Logical types and default syntax}{123}
wenzelm@136
    84
\contentsline {subsection}{Lexical matters *}{124}
wenzelm@136
    85
\contentsline {subsection}{Inspecting syntax *}{124}
wenzelm@136
    86
\contentsline {section}{\numberline {7.3}Abstract syntax trees}{126}
wenzelm@136
    87
\contentsline {subsection}{Parse trees to asts}{128}
wenzelm@136
    88
\contentsline {subsection}{Asts to terms *}{129}
wenzelm@136
    89
\contentsline {subsection}{Printing of terms *}{129}
wenzelm@136
    90
\contentsline {section}{\numberline {7.4}Mixfix declarations}{130}
wenzelm@136
    91
\contentsline {subsection}{Infixes}{133}
wenzelm@136
    92
\contentsline {subsection}{Binders}{133}
wenzelm@136
    93
\contentsline {section}{\numberline {7.5}Syntactic translations (macros)}{134}
wenzelm@136
    94
\contentsline {subsection}{Specifying macros}{135}
wenzelm@136
    95
\contentsline {subsection}{Applying rules}{136}
wenzelm@136
    96
\contentsline {subsection}{Rewriting strategy}{138}
wenzelm@136
    97
\contentsline {subsection}{More examples}{138}
wenzelm@136
    98
\contentsline {section}{\numberline {7.6}Translation functions *}{141}
wenzelm@136
    99
\contentsline {subsection}{A simple example *}{142}
wenzelm@136
   100
\contentsline {section}{\numberline {7.7}Example: some minimal logics}{143}