Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: ROOT Sprache: PVS

Original von: Isabelle^©

chapter FOLP

session FOLP = Pure +
  description "
    Author:     Martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

    Modifed version of FOL that contains proof terms.

    Presence of unknown proof term means that matching does not behave as expected.
  "
  theories
    IFOLP (global)
    FOLP (global)

session "FOLP-ex" in ex = FOLP +
  description "
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge

    Examples for First-Order Logic.
  "
  theories
    Intro
    Nat
    Foundation
    If
    Intuitionistic
    Classical
    Propositional_Int
    Quantifiers_Int
    Propositional_Cla
    Quantifiers_Cla

¤ Dauer der Verarbeitung: 0.1 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.