Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ROOT Sprache: BAT

Original von: Isabelle^©

chapter FOL

session FOL = Pure +
  description "
    First-Order Logic with Natural Deduction (constructive and classical
    versions). For a classical sequent calculus, see Isabelle/LK.

    Useful references on First-Order Logic:

    Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
    1991) (The first chapter is an excellent introduction to natural deduction
    in general.)

    Antony Galton, Logic for Information Technology (Wiley, 1990)

    Michael Dummett, Elements of Intuitionism (Oxford, 1977)
  "
  theories
    IFOL (global)
    FOL (global)
  document_files "root.tex"

session "FOL-ex" in ex = FOL +
  description "
    Examples for First-Order Logic.
  "
  directories "Locale_Test"
  theories
    Natural_Numbers
    Intro
    Nat
    Nat_Class
    Foundation
    Prolog
    Intuitionistic
    Propositional_Int
    Quantifiers_Int
    Classical
    Propositional_Cla
    Quantifiers_Cla
    Miniscope
    If
  theories [document = false, skip_proofs = false]
    "Locale_Test/Locale_Test"
  document_files "root.tex"

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.