Go Home
AI Repository Logo in GIF format


Logic and Reasoning

This site is no longer being maintained.  Sorry.

[OUTLINE - TUTORIAL - TOOLS - RESOURCES - SUBMIT]

Freeware
Tools
  • FINDER
    • 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: lwb@iam.unibe.ch
  • LP
    • 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.
  • MaGIC
  • OTTER
    • 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 programming system.
    • 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

Commercial
Tools
  • Logic for Fun
    • Description:  Provides puzzles and other problems to be formalized in a first order language. Answers are checked by running them through a solver which generates their models. 
    • Target audience:  Logic undergraduates at any level. Also useful for critical reasoning, computer science, AI. No download required: entirely web-based. 
    • Price: This is almost freeware.  Normally $5.00 (US) for 1000 runs. See site for details.
    • Platforms:  Internet Browser.
    • Source: http://csl.anu.edu.au/~jks/puzzlesite/.
    • Reference: http://csl.anu.edu.au/~jks/lff_info.html.
    • Contact: John.Slaney@anu.edu.au

Submit

 Submit a Logic and Reasoning tool.

© 1996-2003. All rights reserved.
Last updated on Tuesday, April 13, 2004 04:08:08 PM.
Suggestion Box.

visitors since April 8, 1999 (counter provided by LinkExchange)