doc-src/Logics/logics.toc
author lcp
Tue May 03 18:38:28 1994 +0200 (1994-05-03)
changeset 359 b5a2e9503a7a
parent 136 a9015b16a0e5
child 465 d4bf81734dfe
permissions -rw-r--r--
final Springer version
lcp@359
     1
\contentsline {chapter}{\numberline {1}Basic Concepts}{1}
lcp@359
     2
\contentsline {section}{\numberline {1.1}Syntax definitions}{2}
lcp@104
     3
\contentsline {section}{\numberline {1.2}Proof procedures}{3}
lcp@359
     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@359
    12
\contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{15}
lcp@359
    13
\contentsline {subsection}{Deriving the introduction rule}{16}
lcp@104
    14
\contentsline {subsection}{Deriving the elimination rule}{17}
lcp@359
    15
\contentsline {subsection}{Using the derived rules}{17}
lcp@359
    16
\contentsline {subsection}{Derived rules versus definitions}{19}
lcp@359
    17
\contentsline {chapter}{\numberline {3}Zermelo-Fraenkel Set Theory}{22}
lcp@359
    18
\contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{22}
lcp@359
    19
\contentsline {section}{\numberline {3.2}The syntax of set theory}{23}
lcp@359
    20
\contentsline {section}{\numberline {3.3}Binding operators}{25}
lcp@359
    21
\contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{27}
lcp@359
    22
\contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{30}
lcp@359
    23
\contentsline {subsection}{Fundamental lemmas}{30}
lcp@359
    24
\contentsline {subsection}{Unordered pairs and finite sets}{32}
lcp@359
    25
\contentsline {subsection}{Subset and lattice properties}{32}
lcp@359
    26
\contentsline {subsection}{Ordered pairs}{36}
lcp@359
    27
\contentsline {subsection}{Relations}{36}
lcp@359
    28
\contentsline {subsection}{Functions}{37}
lcp@359
    29
\contentsline {section}{\numberline {3.6}Further developments}{38}
lcp@359
    30
\contentsline {section}{\numberline {3.7}Simplification rules}{47}
lcp@359
    31
\contentsline {section}{\numberline {3.8}The examples directory}{47}
lcp@359
    32
\contentsline {section}{\numberline {3.9}A proof about powersets}{48}
lcp@359
    33
\contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{51}
lcp@359
    34
\contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{52}
lcp@359
    35
\contentsline {chapter}{\numberline {4}Higher-Order Logic}{55}
lcp@359
    36
\contentsline {section}{\numberline {4.1}Syntax}{55}
lcp@359
    37
\contentsline {subsection}{Types}{57}
lcp@359
    38
\contentsline {subsection}{Binders}{58}
lcp@359
    39
\contentsline {subsection}{The {\ptt let} and {\ptt case} constructions}{58}
lcp@359
    40
\contentsline {section}{\numberline {4.2}Rules of inference}{58}
lcp@359
    41
\contentsline {section}{\numberline {4.3}A formulation of set theory}{60}
lcp@359
    42
\contentsline {subsection}{Syntax of set theory}{65}
lcp@359
    43
\contentsline {subsection}{Axioms and rules of set theory}{69}
lcp@359
    44
\contentsline {section}{\numberline {4.4}Generic packages and classical reasoning}{71}
lcp@359
    45
\contentsline {section}{\numberline {4.5}Types}{73}
lcp@359
    46
\contentsline {subsection}{Product and sum types}{73}
lcp@359
    47
\contentsline {subsection}{The type of natural numbers, {\ptt nat}}{73}
lcp@359
    48
\contentsline {subsection}{The type constructor for lists, {\ptt list}}{76}
lcp@359
    49
\contentsline {subsection}{The type constructor for lazy lists, {\ptt llist}}{76}
lcp@359
    50
\contentsline {section}{\numberline {4.6}The examples directories}{79}
lcp@359
    51
\contentsline {section}{\numberline {4.7}Example: Cantor's Theorem}{80}
lcp@359
    52
\contentsline {chapter}{\numberline {5}First-Order Sequent Calculus}{82}
lcp@359
    53
\contentsline {section}{\numberline {5.1}Unification for lists}{82}
lcp@359
    54
\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{84}
lcp@359
    55
\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{86}
lcp@359
    56
\contentsline {section}{\numberline {5.4}Tactics for sequents}{87}
lcp@359
    57
\contentsline {section}{\numberline {5.5}Packaging sequent rules}{88}
lcp@359
    58
\contentsline {section}{\numberline {5.6}Proof procedures}{88}
lcp@359
    59
\contentsline {subsection}{Method A}{89}
lcp@359
    60
\contentsline {subsection}{Method B}{89}
lcp@359
    61
\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{90}
lcp@359
    62
\contentsline {section}{\numberline {5.8}A more complex proof}{91}
lcp@359
    63
\contentsline {chapter}{\numberline {6}Constructive Type Theory}{93}
lcp@359
    64
\contentsline {section}{\numberline {6.1}Syntax}{95}
lcp@359
    65
\contentsline {section}{\numberline {6.2}Rules of inference}{95}
lcp@359
    66
\contentsline {section}{\numberline {6.3}Rule lists}{101}
lcp@359
    67
\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{101}
lcp@359
    68
\contentsline {section}{\numberline {6.5}Rewriting tactics}{102}
lcp@359
    69
\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{103}
lcp@359
    70
\contentsline {section}{\numberline {6.7}A theory of arithmetic}{105}
lcp@359
    71
\contentsline {section}{\numberline {6.8}The examples directory}{105}
lcp@359
    72
\contentsline {section}{\numberline {6.9}Example: type inference}{105}
lcp@359
    73
\contentsline {section}{\numberline {6.10}An example of logical reasoning}{107}
lcp@359
    74
\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{110}
lcp@359
    75
\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{111}