Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: README Sprache: Lisp

Original von: Isabelle^©

                 Provers: generic theorem proving tools

This directory contains ML sources of generic theorem proving tools.
Typically, they can be applied to various logics, provided rules of a
certain form are derivable.

  blast.ML              generic tableau prover with proof reconstruction
  clasimp.ML  combination of classical reasoner and simplifier
  classical.ML          theorem prover for classical logics
  hypsubst.ML           tactic to substitute in the hypotheses
  quantifier1.ML simplification procedures for "1 point rules"
  splitter.ML           performs case splits for simplifier
  typedsimp.ML          basic simplifier for explicitly typed logics

directory Arith:
  assoc_fold.ML  fold numerals in nested products
  cancel_numerals.ML cancel common coefficients in balanced expressions
  cancel_sums.ML cancel common summands
  combine_numerals.ML combine coefficients in expressions
  fast_lin_arith.ML generic linear arithmetic package

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