- Description: FINDER is a tool for logical problem-solving. It can generate
counter-examples and can be used in combination with other reasoning systems.
- Platforms: UNIX.
- Source: N/A.
- Reference: Additional information is available at arp.anu.edu.au
- Contact: John.Slaney@anu.edu.au
- The Logics Workbench
- Description: The LWB offers the possibility to work in a user-friendly way in classical and non-classical propositional logics, including nonmonotonic approaches. It incorporates functions concerning provability, simplification of formulas, computation of normal forms, embeddings, generation of random formulas, and others. It also includes a programming language for combining existing functions
for general problem solving.
- Platforms: UNIX, Mac, and Internet Browser.
- Source: www.lwb.unibe.ch/.
- Reference: Additional information is available at www.lwb.unibe.ch/.
- Contact: email@example.com
- Description: LP is a theorem prover for multisorted first-order logic. LP
concentrates on helping users find and correct flaws in conjectures, thereby aiding in the
early stages of design.
- Platforms: Available for DEC Alpha AXP running OSF/1, DECstation running Ultrix,
and Sparcstation running SunOS 4.1 or Solaris 5.3
- Source: Retrieve both the run-time library and the appropriate version from larch.lcs.mit.edu.
- Reference: Additional information is available at the LP website.
- Contact: NA.
- Description: Otter is an automated deduction
system designed to prove theorems stated in first-order logic with
equality. Otter's inference rules are based on resolution and
paramodulation, and it includes facilities for term rewriting, term
orderings, Knuth-Bendix completion, weighting, and strategies for
directing and restricting searches for proofs. Otter can also be
used as a symbolic calculator and has an embedded equational
- Platforms: UNIX, Mac, MS Windows.
- Source: www-unix.mcs.anl.gov/AR/otter/.
- Reference: Additional information is available at www-unix.mcs.anl.gov/AR/otter/.
- Contact: Bill McCune,
Argonne National Lab.
- Stat Reasoning-Ace Detective (STATRAD)
- Description: Stat Reasoning-Ace Detective (statrad) is an interactive tool to
help students learn reasoning with uncertainty. It uses graphics, color, and animation and
runs on UNIX. The initial implementation of this tool focuses on Dempster-Shafer theory.
- Platforms: UNIX.
- Source: N/A
- Reference: The README file at the ftp site includes instructions on how to down
load the package to your site. This file also lists the platforms that will be needed at
your site to run statrad.
- Contact: Deborah Ann Vastola