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