Logic and Foundations
- 103
- ACL2 Version 2.7
- A programming language in which you can model computer systems and a tool to help prove properties of those models. Available under GPL and runs on various platforms. Includes related download links.
- 104
- Church
- Program understands the different types of lambda expressions, can extract lists of variables (both free and bound) and subterms, and can simplify complicated expressions. Uses Python.
- 105
- DC Proof Online
- New proof-writing software to teach the fundamentals of logic and proof. Enables users/students to write error-free proofs by selecting rules of inference, axioms, etc. from convenient drop-down menus. Includes tutorial and exercises.
- 106
- LOOM
- A language and environment for constructing intelligent applications. It is a research project in the Artificial Intelligence research group at the University of Southern California's Information Sciences Institute. The goal of the project is to develop and field advanced tools for knowledge representation and reasoning in Artificial Intelligence.
- 107
- MUltlog
- Takes as input the specification of a finitely-valued first-order logic and produces a sequent calculus, a natural deduction system, and clause formation rules for this logic.
- 109
- PVS
- The PVS Specification and Verification System. Available for Sparc machines with Solaris 2 and Intel x86 Machines with Linux compatible with Redhat 5 or later. Required is Emacs (version 19 or later), recommended LaTeX and Tcl/Tk. Download by FTP.
- 110
- Proof General
- Comprehensive Gnu-Emacs and XEmacs interface for several theorem provers including Coq, Isabelle, Lego, and Phox.
- 111
- WinKE
- An interactive proof assistant based on analytic tableaux, and designed for the teaching of deductive reasoning. Ordering information is available at this site, as are academic papers on the design of the software.
- 112
- Dual Identity Combinators
- Article by Katalin Bimbó presented at the 20th World Congress of Philosophy. Investigates the addition of identity combinators, in the formulae-as-types sense, to combinatory logic.
- 113
- Lambda
- An online introduction to the lambda calculus by Lloyd Allison, complete with a web form that will evaluate lambda expressions.
- 114
- Perl Contains the Lambda-Calculus
- Explains why this computer program is well suited to apply to functional application.
- 115
- Isabelle
- Homepage of the theorem prover environment developed by Larry Paulson at Cambridge University and Tobias Kipkow at TU Munich.
- 116
- NuPrl Proof Development System
- A powerful tactic-based proof assistant, developed over the last 15 years at Cornell University. Features include: very expressive logical language based on Martin-Lof type theory, extensive library of formal mathematics and automata theory, possibility of an extraction a certified program from the constructive proof of its formal specification, graphical proof editor. NuPrl was successfully used in verifying components of the Ensemble group communications system.
- 117
- The HOL Theorem Proving System
- The system documented originated at the Laboratory for Applied Logic of Brigham Young University and features higher-order, classical, natural deduction with tactics.
- 118
- The LEGO Proof Assistant
- A powerful tool for interactive proof development in the natural deduction style. It supports refinement proof as a basic operation. The system design emphasizes removing the more tedious aspects of interactive proofs.