Subject: pkg/11392: package submission for math/otter
To: None <>
From: Jason Beegan <>
List: netbsd-bugs
Date: 11/01/2000 19:17:07
>Number:         11392
>Category:       pkg
>Synopsis:       package submission for math/otter
>Confidential:   no
>Severity:       non-critical
>Priority:       low
>Responsible:    pkg-manager
>State:          open
>Class:          change-request
>Submitter-Id:   net
>Arrival-Date:   Wed Nov 01 19:06:35 PST 2000
>Originator:     Jason Beegan
>Release:        1.5_ALPHA NetBSD

System: NetBSD 1.5_ALPHA NetBSD 1.5_ALPHA (Kurwenal) #0: Thu Oct 5 19:05:34 PDT 2000 i386

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

Otter is a theorem proving program


Otter (Organized Techniques for Theorem-proving and Effective
Research) 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, and
Knuth-Bendix completion.  Otter is coded in C, is free, and is
portable to many different kinds of computer.