>Number:         11402
>Category:       pkg
>Synopsis:       package submission for math/gandalf
>Confidential:   no
>Severity:       non-critical
>Priority:       low
>Responsible:    pkg-manager
>State:          open
>Class:          change-request
>Submitter-Id:   net
>Arrival-Date:   Wed Nov 01 19:07:01 PST 2000
>Closed-Date:
>Last-Modified:
>Originator:     Jason Beegan
>Release:        1.5_ALPHA NetBSD
>Organization:

>Environment:
	
System: NetBSD tarnhelm.verklaerung.net 1.5_ALPHA NetBSD 1.5_ALPHA (Kurwenal) #0: Thu Oct 5 19:05:34 PDT 2000 root@tarnhelm.verklaerung.net:/usr/src/sys/arch/i386/compile/Kurwenal i386


>Description:
I would like to submit a package to the pkgsrc collection.
You will find it at

	http://indigo.ie/~jasontd/pkgsrc-math-gandalf.tar.gz


COMMENT:
Gandalf is a theorem prover for classical first order logic

DESCR:

Gandalf is a resolution theorem prover for first order classical logic
with equality.

Gandalf won the yearly ATP competition CASC in 1997.

Gandalf has a powerful automatic mode and, differently from most of
the other existing provers, it is well optimised for handling problems
where big amounts of long clauses are derived.

Gandalf implements a large number of various search strategies.  The
usage of these strategies can be either controlled by the human user
or by the powerful automatic mode of Gandalf. The automatic mode first
selects a set of different strategies which are likely to be useful
for a given problem and then tries all these strategies one after
another. Gandalf is also well optimised for handling problems where
big amounts of long clauses are derived.

Gandalf is not interactive - it reads in a file containing the
problem, outputs information about the progress of proof search and
eventually outputs a detailed proof.

Gandalf is written in Scheme and compiled to C by the Scheme-to-C
compiler Hobbit developed by the author of Gandalf.

>How-To-Repeat:
>Fix:
>Release-Note:
>Audit-Trail:
>Unformatted: