Package: wnpp Severity: wishlist Owner: Peter Collingbourne <[EMAIL PROTECTED]>
* Package name : otter Version : 3.3f Upstream Author : William McCune <[EMAIL PROTECTED]> * URL : http://www.cs.unm.edu/~mccune/otter/ * License : public domain Programming Lang: C Description : resolution-style theorem prover OTTER is an automated theorem prover for equational logic developed at Argonne National Laboratory. . 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. MACE is a program that searches for finite models of first-order and equational statements developed at Argonne National Laboratory. . This package includes ANLDP, which calls the propositional decision procedure at the core of MACE directly. . MACE serves as a complementary companion to OTTER, which searches for refutations of the same class of statement. In particular, if you have a first-order conjecture, OTTER will search for a proof, and MACE will search for a counterexample from the same input file. Formed is a formula editor for first-order logic formulas that lets you simplify quantified formulas by quantifier transformation among other things. -- System Information: Debian Release: testing/unstable APT prefers testing APT policy: (500, 'testing') Architecture: i386 (i686) Shell: /bin/sh linked to /bin/bash Kernel: Linux 2.6.17-2-686 Locale: LANG=en_GB, LC_CTYPE=en_GB (charmap=ISO-8859-1) -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]
