Initial import of new "otter" package:

Otter is a theorem-proving program

8 files changed, 279 insertions, 0 deletions

diff --git a/math/otter/Makefile b/math/otter/Makefile
new file mode 100644
index 00000000000..309fa0d7d2b
--- /dev/null
+++ b/math/otter/Makefile
@@ -0,0 +1,36 @@
+# $NetBSD: Makefile,v 1.1.1.1 2000/11/25 18:19:19 jtb Exp $
+
+DISTNAME=	otter-3.0.6
+CATEGORIES=	math
+MASTER_SITES=	ftp://info.mcs.anl.gov/pub/Otter/
+
+MAINTAINER=	jtb@netbsd.org
+HOMEPAGE=	http://www.mcs.anl.gov/AR/otter/
+
+WRKSRC=		${WRKDIR}/${PKGNAME}/source
+
+ALL_TARGET=	otter
+
+do-install:
+	${INSTALL_PROGRAM} ${WRKSRC}/otter ${PREFIX}/bin
+	${INSTALL_DATA_DIR} ${PREFIX}/share/examples/otter
+	${INSTALL_DATA_DIR} ${PREFIX}/share/doc/otter
+	@(cd ${WRKDIR}/${PKGNAME};					\
+	for r in Announce Changelog Copying README*;			\
+	do								\
+	${INSTALL_DATA} $$r ${PREFIX}/share/doc/otter;			\
+	done;								\
+	for d in auto fringe ivy kalman misc program split wos;		\
+	do								\
+	${INSTALL_DATA_DIR} ${PREFIX}/share/examples/otter/$$d;		\
+	${INSTALL_DATA} examples/$$d/* ${PREFIX}/share/examples/otter/$$d;\
+	done;								\
+	for p in Run_all objects summary;				\
+	do								\
+	${INSTALL_SCRIPT} examples/$$p ${PREFIX}/share/examples/otter/$$p;\
+	done;								\
+	${INSTALL_DATA} examples/README ${PREFIX}/share/examples/otter;	\
+	${INSTALL_DATA} ${WRKDIR}/${PKGNAME}/document/* 		\
+	${PREFIX}/share/doc/otter)
+
+.include "../../mk/bsd.pkg.mk"
diff --git a/math/otter/files/md5 b/math/otter/files/md5
new file mode 100644
index 00000000000..af7f9ed0c2c
--- /dev/null
+++ b/math/otter/files/md5
@@ -0,0 +1,3 @@
+$NetBSD: md5,v 1.1.1.1 2000/11/25 18:19:21 jtb Exp $
+
+MD5 (otter-3.0.6.tar.gz) = b6e9c2f13d6de2409c883582fa91daeb
diff --git a/math/otter/files/patch-sum b/math/otter/files/patch-sum
new file mode 100644
index 00000000000..abbb9bc9ad2
--- /dev/null
+++ b/math/otter/files/patch-sum
@@ -0,0 +1,4 @@
+$NetBSD: patch-sum,v 1.1.1.1 2000/11/25 18:19:21 jtb Exp $
+
+MD5 (patch-aa) = 4adefe43039c34802d48503a9242e52d
+MD5 (patch-ab) = 4a4f6729b8bc12a0618a7478afea164f
diff --git a/math/otter/patches/patch-aa b/math/otter/patches/patch-aa
new file mode 100644
index 00000000000..5d7e249eabc
--- /dev/null
+++ b/math/otter/patches/patch-aa
@@ -0,0 +1,13 @@
+$NetBSD: patch-aa,v 1.1.1.1 2000/11/25 18:19:21 jtb Exp $
+
+--- Makefile.orig	Mon Nov 13 23:57:18 2000
++++ Makefile
+@@ -80,7 +80,7 @@
+ # Specify the C compiler.  I recommend gcc (GNU C Compiler) if you have it.
+ # In many Linux environments, cc is just a symlink to gcc.
+ 
+-CC = cc
++#CC = cc
+ 
+ #############################################################################
+ #
diff --git a/math/otter/patches/patch-ab b/math/otter/patches/patch-ab
new file mode 100644
index 00000000000..6403b442272
--- /dev/null
+++ b/math/otter/patches/patch-ab
@@ -0,0 +1,19 @@
+$NetBSD: patch-ab,v 1.1.1.1 2000/11/25 18:19:21 jtb Exp $
+
+--- ../examples/Run_all.orig	Tue Oct 10 12:00:04 2000
++++ ../examples/Run_all
+@@ -1,4 +1,4 @@
+-#
++#!/bin/csh
+ #
+ #  Run a set of otter jobs ($1/*.in) and compare the
+ #  results ($1/*.out) to $1/*.ppro180.
+@@ -18,7 +18,7 @@
+ if ($#argv >= 2) then
+    set OTTER=$2
+ else
+-   set OTTER=../../source/otter
++   set OTTER=otter
+ endif
+ 
+ if ($#argv >= 3) then
diff --git a/math/otter/pkg/COMMENT b/math/otter/pkg/COMMENT
new file mode 100644
index 00000000000..b62c48542e6
--- /dev/null
+++ b/math/otter/pkg/COMMENT
@@ -0,0 +1 @@
+Otter is a theorem-proving program
diff --git a/math/otter/pkg/DESCR b/math/otter/pkg/DESCR
new file mode 100644
index 00000000000..04f69641f7f
--- /dev/null
+++ b/math/otter/pkg/DESCR
@@ -0,0 +1,10 @@
+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.
diff --git a/math/otter/pkg/PLIST b/math/otter/pkg/PLIST
new file mode 100644
index 00000000000..cc1f18ae0cb
--- /dev/null
+++ b/math/otter/pkg/PLIST
@@ -0,0 +1,193 @@
+@comment $NetBSD: PLIST,v 1.1.1.1 2000/11/25 18:19:21 jtb Exp $
+bin/otter
+share/doc/otter/Announce
+share/doc/otter/Changelog
+share/doc/otter/Copying
+share/doc/otter/New_304.txt
+share/doc/otter/New_305.txt
+share/doc/otter/README.302
+share/doc/otter/README.303
+share/doc/otter/README.304
+share/doc/otter/README.305
+share/doc/otter/README.306
+share/doc/otter/manual.dvi
+share/doc/otter/manual.ps
+share/doc/otter/manual.tex
+share/doc/otter/manual.txt
+share/doc/otter/split.txt
+share/examples/otter/README
+share/examples/otter/Run_all
+share/examples/otter/auto/cn19.PII400
+share/examples/otter/auto/cn19.in
+share/examples/otter/auto/comm.PII400
+share/examples/otter/auto/comm.in
+share/examples/otter/auto/ec_yq.PII400
+share/examples/otter/auto/ec_yq.in
+share/examples/otter/auto/group.PII400
+share/examples/otter/auto/group.in
+share/examples/otter/auto/lifsch.PII400
+share/examples/otter/auto/lifsch.in
+share/examples/otter/auto/mv25.PII400
+share/examples/otter/auto/mv25.in
+share/examples/otter/auto/pigeon.PII400
+share/examples/otter/auto/pigeon.in
+share/examples/otter/auto/ring_x2.PII400
+share/examples/otter/auto/ring_x2.in
+share/examples/otter/auto/robbins.PII400
+share/examples/otter/auto/robbins.in
+share/examples/otter/auto/salt.PII400
+share/examples/otter/auto/salt.in
+share/examples/otter/auto/sam.PII400
+share/examples/otter/auto/sam.in
+share/examples/otter/auto/steam.PII400
+share/examples/otter/auto/steam.in
+share/examples/otter/auto/tba_gg.PII400
+share/examples/otter/auto/tba_gg.in
+share/examples/otter/auto/w_sk.PII400
+share/examples/otter/auto/w_sk.in
+share/examples/otter/auto/wang1.PII400
+share/examples/otter/auto/wang1.in
+share/examples/otter/auto/x2_quant.PII400
+share/examples/otter/auto/x2_quant.in
+share/examples/otter/auto/z11.PII400
+share/examples/otter/auto/z11.in
+share/examples/otter/fringe/bring.PII400
+share/examples/otter/fringe/bring.in
+share/examples/otter/fringe/ec_yql.PII400
+share/examples/otter/fringe/ec_yql.in
+share/examples/otter/fringe/gl4.PII400
+share/examples/otter/fringe/gl4.in
+share/examples/otter/fringe/gl8.PII400
+share/examples/otter/fringe/gl8.in
+share/examples/otter/fringe/if.PII400
+share/examples/otter/fringe/if.in
+share/examples/otter/fringe/lexical1.PII400
+share/examples/otter/fringe/lexical1.in
+share/examples/otter/fringe/lexical2.PII400
+share/examples/otter/fringe/lexical2.in
+share/examples/otter/fringe/lexical3.PII400
+share/examples/otter/fringe/lexical3.in
+share/examples/otter/fringe/luka5h.PII400
+share/examples/otter/fringe/luka5h.in
+share/examples/otter/fringe/mfl_13.PII400
+share/examples/otter/fringe/mfl_13.in
+share/examples/otter/fringe/rob_ocd.PII400
+share/examples/otter/fringe/rob_ocd.in
+share/examples/otter/fringe/x3tricks.PII400
+share/examples/otter/fringe/x3tricks.in
+share/examples/otter/ivy/cd-cn19.PII400
+share/examples/otter/ivy/cd-cn19.in
+share/examples/otter/ivy/comb-sk-w.PII400
+share/examples/otter/ivy/comb-sk-w.in
+share/examples/otter/ivy/group-comm.PII400
+share/examples/otter/ivy/group-comm.in
+share/examples/otter/ivy/group-x2-refute.PII400
+share/examples/otter/ivy/group-x2-refute.in
+share/examples/otter/ivy/group-x2.PII400
+share/examples/otter/ivy/group-x2.in
+share/examples/otter/ivy/lifsch.PII400
+share/examples/otter/ivy/lifsch.in
+share/examples/otter/ivy/p-and-not-p.PII400
+share/examples/otter/ivy/p-and-not-p.in
+share/examples/otter/ivy/steam.PII400
+share/examples/otter/ivy/steam.in
+share/examples/otter/ivy/t1.PII400
+share/examples/otter/ivy/t1.in
+share/examples/otter/kalman/ex_1.PII400
+share/examples/otter/kalman/ex_1.in
+share/examples/otter/kalman/ex_2.PII400
+share/examples/otter/kalman/ex_2.in
+share/examples/otter/kalman/ex_3.PII400
+share/examples/otter/kalman/ex_3.in
+share/examples/otter/kalman/ex_4.PII400
+share/examples/otter/kalman/ex_4.in
+share/examples/otter/kalman/i1.PII400
+share/examples/otter/kalman/i1.in
+share/examples/otter/kalman/i2.PII400
+share/examples/otter/kalman/i2.in
+share/examples/otter/kalman/i3.PII400
+share/examples/otter/kalman/i3.in
+share/examples/otter/kalman/i4.PII400
+share/examples/otter/kalman/i4.in
+share/examples/otter/misc/andrews.PII400
+share/examples/otter/misc/andrews.in
+share/examples/otter/misc/cn.PII400
+share/examples/otter/misc/cn.in
+share/examples/otter/misc/dem_alu.PII400
+share/examples/otter/misc/dem_alu.in
+share/examples/otter/misc/ec.PII400
+share/examples/otter/misc/ec.in
+share/examples/otter/misc/kb_bench.PII400
+share/examples/otter/misc/kb_bench.in
+share/examples/otter/misc/mv.PII400
+share/examples/otter/misc/mv.in
+share/examples/otter/misc/sax1.PII400
+share/examples/otter/misc/sax1.in
+share/examples/otter/misc/sax2.PII400
+share/examples/otter/misc/sax2.in
+share/examples/otter/misc/stage1.PII400
+share/examples/otter/misc/stage1.in
+share/examples/otter/misc/stage2.PII400
+share/examples/otter/misc/stage2.in
+share/examples/otter/misc/str_bws.PII400
+share/examples/otter/misc/str_bws.in
+share/examples/otter/objects
+share/examples/otter/program/eval.PII400
+share/examples/otter/program/eval.in
+share/examples/otter/program/jugs.PII400
+share/examples/otter/program/jugs.in
+share/examples/otter/program/mission.PII400
+share/examples/otter/program/mission.in
+share/examples/otter/program/queens.PII400
+share/examples/otter/program/queens.in
+share/examples/otter/program/two_inv.PII400
+share/examples/otter/program/two_inv.in
+share/examples/otter/split/GEO010-2.PII400
+share/examples/otter/split/GEO010-2.in
+share/examples/otter/split/GEO036-2.PII400
+share/examples/otter/split/GEO036-2.in
+share/examples/otter/split/GRP025-1.PII400
+share/examples/otter/split/GRP025-1.in
+share/examples/otter/split/README
+share/examples/otter/split/group2.PII400
+share/examples/otter/split/group2.in
+share/examples/otter/split/noncomm-group.PII400
+share/examples/otter/split/noncomm-group.in
+share/examples/otter/split/pair.PII400
+share/examples/otter/split/pair.in
+share/examples/otter/split/pigeon5.PII400
+share/examples/otter/split/pigeon5.in
+share/examples/otter/split/power.PII400
+share/examples/otter/split/power.in
+share/examples/otter/split/wang3.PII400
+share/examples/otter/split/wang3.in
+share/examples/otter/split/zebra2.PII400
+share/examples/otter/split/zebra2.in
+share/examples/otter/split/zebra4.PII400
+share/examples/otter/split/zebra4.in
+share/examples/otter/summary
+share/examples/otter/wos/README
+share/examples/otter/wos/cursory.PII400
+share/examples/otter/wos/cursory.in
+share/examples/otter/wos/grp_exp3.PII400
+share/examples/otter/wos/grp_exp3.in
+share/examples/otter/wos/grp_exp4.PII400
+share/examples/otter/wos/grp_exp4.in
+share/examples/otter/wos/manyval.PII400
+share/examples/otter/wos/manyval.in
+share/examples/otter/wos/rigorous.PII400
+share/examples/otter/wos/rigorous.in
+share/examples/otter/wos/rob_occ.PII400
+share/examples/otter/wos/rob_occ.in
+share/examples/otter/wos/twoval.PII400
+share/examples/otter/wos/twoval.in
+@dirrm share/examples/otter/wos
+@dirrm share/examples/otter/split
+@dirrm share/examples/otter/program
+@dirrm share/examples/otter/misc
+@dirrm share/examples/otter/kalman
+@dirrm share/examples/otter/ivy
+@dirrm share/examples/otter/fringe
+@dirrm share/examples/otter/auto
+@dirrm share/examples/otter
+@dirrm share/doc/otter