src/FOL/ROOT
author wenzelm
Sat, 22 Mar 2014 18:19:57 +0100
changeset 56254 a2dd9200854d
parent 52488 cd65ee49a8ba
child 56781 f2eb0f22589f
permissions -rw-r--r--
more antiquotations;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
51397
03b586ee5930 support for 'chapter' specifications within session ROOT;
wenzelm
parents: 48738
diff changeset
     1
chapter FOL
03b586ee5930 support for 'chapter' specifications within session ROOT;
wenzelm
parents: 48738
diff changeset
     2
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48487
diff changeset
     3
session FOL = Pure +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     4
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     5
    First-Order Logic with Natural Deduction (constructive and classical
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     6
    versions). For a classical sequent calculus, see Isabelle/LK.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     7
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     8
    Useful references on First-Order Logic:
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     9
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    10
    Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    11
    1991) (The first chapter is an excellent introduction to natural deduction
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    12
    in general.)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    13
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    14
    Antony Galton, Logic for Information Technology (Wiley, 1990)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    15
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    16
    Michael Dummett, Elements of Intuitionism (Oxford, 1977)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    17
  *}
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    18
  theories FOL
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    19
  files "document/root.tex"
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    20
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48487
diff changeset
    21
session "FOL-ex" in ex = FOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    22
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    23
    Examples for First-Order Logic.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    24
  *}
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    25
  theories
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    26
    First_Order_Logic
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    27
    Natural_Numbers
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    28
    Intro
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    29
    Nat
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    30
    Nat_Class
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    31
    Foundation
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    32
    Prolog
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    33
    Intuitionistic
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    34
    Propositional_Int
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    35
    Quantifiers_Int
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    36
    Classical
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    37
    Propositional_Cla
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    38
    Quantifiers_Cla
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    39
    Miniscope
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    40
    If
51558
91f8bed6d0a4 allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents: 51403
diff changeset
    41
  theories [document = false, skip_proofs = false]
91f8bed6d0a4 allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents: 51403
diff changeset
    42
    "Locale_Test/Locale_Test"
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    43
  files "document/root.tex"
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    44