Update of /cvsroot/fink/dists/10.3/unstable/main/finkinfo/sci
In directory sc8-pr-cvs5.sourceforge.net:/tmp/cvs-serv773
Added Files:
otter.info
Log Message:
Looks OK--add for maintainer
--- NEW FILE: otter.info ---
Package: otter
Version: 3.3f
Description: Tools for first-order models and theorems
Revision: 1
Maintainer: Jesse Alama <[EMAIL PROTECTED]>
Homepage: http://www-unix.mcs.anl.gov/AR/otter/
Source: http://www-unix.mcs.anl.gov/AR/otter/dist33/%n-%v.tar.gz
Source-MD5: 795711b307cc1316e08d3d4f46c998c9
DocFiles: README.first README README.Ivy Legal documents/otter33.pdf
documents/mace2.pdf documents/anldp.pdf
License: Public Domain
CompileScript: <<
make all
<<
InstallScript: <<
mkdir -p %i/bin
install -m 755 bin/otter %i/bin
install -m 755 bin/mace2 %i/bin
install -m 755 bin/anldp %i/bin
<<
DescDetail: <<
This package contains OTTER, MACE, and ANLDP, three programs developed
at Argonne National Labs for first-order theorem proving and model
generation.
OTTER is a resolution-style theorem-proving program for first-order
logic with equality. OTTER includes the inference rules binary
resolution, hyperresolution, UR-resolution, and binary
paramodulation. Some of its other abilities and features are
conversion from first-order formulas to clauses, forward and back
subsumption, factoring, weighting, answer literals, term ordering,
forward and back demodulation, evaluable functions and predicates,
Knuth-Bendix completion, and the hints strategy.
MACE is a program that searches for finite models of first-order
statements. The statement to be modeled is first translated to
clauses, then to relational clauses; finally for the given domain
size, the ground instances are constructed. A
Davis-Putnam-Loveland-Logeman procedure decides the propositional
problem, and any models found are translated to first-order
models. MACE is a useful complement to the theorem prover OTTER, with
OTTER searching for proofs and MACE looking for countermodels.
ANLDP is a model generation program based on the Davis-Putnam method
for solving the propositional satisfiability problem.
<<
-------------------------------------------------------------------------
Take Surveys. Earn Cash. Influence the Future of IT
Join SourceForge.net's Techsay panel and you'll get the chance to share your
opinions on IT & business topics through brief surveys -- and earn cash
http://www.techsay.com/default.php?page=join.php&p=sourceforge&CID=DEVDEV
_______________________________________________
Fink-commits mailing list
Fink-commits@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/fink-commits
