formed | formula editor for first-order logic formulae | Mehr ... |
mace2 | program that searches for finite models of first-order statements | Mehr ... |
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. |
otter | resolution-style theorem prover | Mehr ... |
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.
|