Math Computational Logic in the Best of the Web Directory

Math Computational Logic

  • Alfa

    Proof editor succeeding ALF, an editor for direct manipulation of proof objects in a logical framework based on Per Martin-LC6f's Type Theory. Free download available.

  • Automated Reasoning

    Article from the Stanford Encyclopedia of Philosophy.

  • Coq Proof Assistant

    Formal proof management system, based on a logical framework called Calculus of Inductive Constructions extended by a modular development system for theories. With links to download, documentation and related tools.

  • CtCoq

    Provides a working environment for the Coq theorem prover. Developed at INRIA Sophia Antipolis.

  • Dual Identity Combinators

    Provides an analysis of the effect of the identity combinators in dual systems. Written by Katalin Bimbó.

  • HOL Project

    Automated proof system for higher order logic. Operates as an open source project with a BSD-style license allowing free use in commercial products.

  • Isabelle

    Generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).

  • Kumo

    Web-based proof assistant for first order-hidden logic, using OBJ3 as a reduction engine. Also generates proof documentation for the web and supports distributed cooperative proving.

  • Lambda Calculus

    Guide to lazy and strict versions of the lambda-calculus interpreter.

  • LEGO Proof Assistant

    Interactive proof development system designed and implemented by Randy Pollack in Edinburgh.

  • Proof General

    Generic interface for proof assistants, based on the customizable text editor Emacs. Works with either XEmacs or GNU Emacs.

  • Yarrow

    Proof-assistant for Pure Type Systems (PTSs) with several extensions. With user guide, installation guide, tutorials and articles about Yarrow.

Submit a site to this category