Artificial Intelligence FAQ: FTP Resources 6/7 [Monthly posting]
ca...@cs.ucla.edu
Posting-Frequency: monthly
Last-Modified: Fri Mar 19 13:37:08 PST 1999 by Ric Crabbe
Version: 2.0
Maintainer: Ric Crabbe <ca...@cs.ucla.edu> and Amit Dubey <adu...@undergrad.math.uwaterloo.ca>
URL: ftp://ftp.cs.ucla.edu/pub/AI/ai_6.faq
Size: 84098 bytes, 1871 lines
;;; ****************************************************************
;;; Answers to Questions about Artificial Intelligence *************
;;; ****************************************************************
;;; Written by Amit Dubey, Ric Crabbe, and Mark Kantrowitz
;;; ai_6.faq
If you think of questions that are appropriate for this FAQ, or would
like to improve an answer, please send email to the maintainers.
Please note that the WWW & FTP Resources section is now split across parts 5
and 6 of the AI FAQ.
Note: Question [5-2] is split across parts 5 and 6.
Part 5b (WWW & FTP Resources):
[5-2b] WWW & FTP Resources: Qualitative Reasoning -- Theorem Proving
--------------------------------------------------------------------
Subject: [5-2b] WWW & FTP Resources: GAs -- Theorem Proving
ICOT:
Japan's Institute for New Generation Computer Technology (ICOT) has
made their software available to the public free of charge. The
collection includes a variety of prolog-based programs in symbol
processing, knowledge representation, reasoning and problem solving,
natural language processing. All programs are available by anonymous
ftp from ftp.icot.or.jp. Note that most of the programs are written
for the PSI machines, and very few have been ported to Unix-based
emulators. For further information, send email to i...@icot.or.jp, or
write to ICOT Free Software Desk, Institute for New Generation
Computer Technology, 21st Floor, Mita Kokusai Bldg., 4-28, Mita
1-chome, Minato-ku, Tokyo 108, Japan, fax +81-3-4456-1618.
Knowledge Representation:
KNOWBEL -- ai.toronto.edu:/pub/kr/ as the files knowbel.tar.Z and
manual.txt.tar.Z
Contact: Bryan M. Kramer, <kra...@ai.toronto.edu>
Telos temporal/sorted logic system.
SB-ONE -- Contact: ko...@inf-wiss.uni-konstanz.de
KL-ONE family. Currently undergoing revision and will be
renamed KN-PART+.
KRIS -- Contact: baa...@dfki.uni-kl.de
KL-ONE family (Symbolics only)
BACK -- Contact: ba...@cs.tu-berlin.de
ftp.cs.tu-berlin.de:/pub/doc/reports/tu-berlin.de/kit/Back52
Files are BACK_V52.intro and Back52.tar.Z
Tar file includes Tutorial/Manual in postscript format
and installation instructions.
KL-ONE family
CLASSIC -- Contact: d...@research.att.com
KL-ONE family
MOTEL -- Contact: hus...@mpi-sb.mpg.de
mpi-sb.mpg.de:/pub/tools/motel.tar.Z [139.19.1.1]
Modal KL-ONE (contains KRIS as a kernel).
Implemented in Prolog.
FOL GETFOL -- Contact: fau...@irst.it
Weyrauch's FOL system
COLAB/RELFUN -- Contact: bo...@informatik.uni-kl.de
Logic Programming
COLAB/FORWARD -- Contact: hink...@dfki.uni-kl.de
Logic Programming
COLAB/CONTAX -- Contact: me...@dfki.uni-kl.de
Constraint System for Weighted Constraints over
Hierarchically Structured Finite Domains.
COLAB/TAXON -- Contact: hans...@dfki.uni-kl.de
Terminological Knowl. Rep. w/Concrete Domains
SNePS (Semantic Network Processing System) is the implementation of a
fully intensional theory of propositional knowledge representation and
reasoning. SNePS includes a module for creating and accessing
propositional semantic networks, path-based inference, node-based
inference based on SWM (a relevance logic with quantification) that
uses natural deduction and can deal with recursive rules, forward,
backward and bi-directional inference, nonstandard logical connectives
and quantifiers, an assumption based TMS for belief revision (SNeBR), a
morphological analyzer and a generalized ATN (GATN) parser for parsing
and generating natural language, SNePSLOG, a predicate-logic-style
interface to SNePS, XGinseng, an X-based graphics interface for
displaying, creating and editing SNePS networks, SNACTor, a
preliminary version of the SNePS Acting component, and SNIP 2.2, a new
implementation of the SNePS Inference Package that uses rule shadowing
and knowledge migration to speed up inference. SNeRE (the SNePS
Rational Engine), which is part of Deepak Kumar's dissertation about
the integration of inference and acting, will replace the current
implementation of SNACTor. SNePS is written in Common Lisp, and has
been tested in Allegro CL 4.1, Lucid CL 4.0, TI Common Lisp, CLISP
May-93, and CMU CL 17b. It should also run in Symbolics CL, AKCL 1.600
and higher, VAX Common Lisp, and MCL. The XGinseng interface is built
on top of Garnet. SNePS 2.1 is free according to the GNU General
Public License version 2. The SNePS distribution is available by
anonymous ftp from
ftp.cs.buffalo.edu:/pub/sneps/ [128.205.32.9]
as the file rel-x-yyy.tar.Z, where 'x-yyy' is the version. The other
files in the directory are included in the distribution; they are
duplicated to let you get them without unpacking the full distribution
if you just want the bibliography or manual. If you use SNePS, please
send a short message to sha...@cs.buffalo.edu and
sn...@cs.buffalo.edu. Please also let them know whether you'd like to
be added to the SNUG (SNePS Users Group) mailing list.
URANUS is a logic-based knowledge representation language. Uranus is
an extension of Prolog written in Common Lisp and using the syntax of
Lisp. Uranus extends Prolog with a multiple world mechanism for
knowledge representation and term descriptions to provide
functional programming within the framework of logic programming.
It is available free by anonymous ftp from
etlport.etl.go.jp:/pub/uranus/ftp/ [192.31.197.99]
for research purposes only. For more information contact the author,
Hideyuki Nakashima <naka...@etl.go.jp>.
Machine Learning:
COBWEB/3 -- Contact: cob...@ptolemy.arc.nasa.gov
IND -- Contact: NASA COSMIC, <ser...@cossack.cosmic.uga.edu>
Tel: 706-542-3265 (ask for customer support)
Fax: 706-542-4807
IND is a C program for the creation and manipulation of
decision trees from data, integrating the CART,
ID3/C4.5, Buntine's smoothing and option trees, Wallace
and Patrick's MML method, and Oliver and Wallace's MML
decision graphs which extend the tree representation to
graphs. Written by Wray Buntine, <wr...@kronos.arc.nasa.gov>.
AUTOCLASS -- Contact: tay...@ptolemy.arc.nasa.gov
AutoClass is an unsupervised Bayesian classification system for
independent data.
FOIL -- ftp.cs.su.oz.au:/pub/ [129.78.8.208]
as the files foil4.sh, foil5.sh, and foil6.sh.
Each shell archive contains source, a brief manual,
and several sample datasets. FOIL2 should be available
from sumex-aim.stanford.edu:/pub/FOIL.sh. FOIL 6.0 now uses
ANSI C.
Contact: J. Ross Quinlan <qui...@cs.su.oz.au>
Mike Cameron-Jones <m...@cs.su.oz.au>
RWM -- Contact: H. Altay Guvenir <guv...@trbilun.bitnet>
RWM is a program for learning problem solving strategies,
written in Common Lisp (tested on Suns and NeXT).
MOBAL is a system for developing operational models of application
domains in a first order logic representation. It integrates a manual
knowledge acquisition and inspection environment, an inference engine,
machine learning methods for automated knowledge acquisition, and a
knowledge revision tool. By using MOBAL's knowledge acquisition
environment, you can incrementally develop a model of your domain in
terms of logical facts and rules. You can inspect the knowledge you
have entered in text or graphics windows, augment the knowledge, or
change it at any time. The built-in inference engine can immediately
execute the rules you have entered to show you the consequences of
your inputs, or answer queries about the current knowledge. MOBAL also
builds a dynamic sort taxonomy from your inputs. If you wish, you can
use several machine learning methods to automatically discover
additional rules based on the facts that you have entered, or to form
new concepts. If there are contradictions in the knowledge base due to
incorrect rules or facts, there is a knowledge revision tool to help
you locate the problem and fix it. MOBAL (release 3.0b) is available
free for non-commercial academic use by anonymous ftp from
ftp.gmd.de:/gmd/mlt/Mobal/
The system runs on Sun SparcStations, SunOS 4.1, and includes a
graphical interface implemented using Tcl/TK.
PEBLS (Parallel Exemplar-Based Learning System) is a nearest-neighbor
learning system designed for applications where the instances have
symbolic feature values. PEBLS has been applied to the prediction of
protein secondary structure and to the identification of DNA promoter
sequences. PEBLS 3.0 is written in ANSI C and is available by
anonymous ftp from blaze.cs.jhu.edu:/pub/pebls/pebls.tar.Z
[128.220.13.50] for research purposes only. For more information,
contact Steven Salzberg <salz...@cs.jhu.edu>.
OC1 (Oblique Classifier 1) is a multivariate decision tree induction
system designed for applications where the instances have numeric
feature values. OC1 builds decision trees that contain linear
combinations of one or more attributes at each internal node; these
trees then partition the space of examples with both oblique and
axis-parallel hyperplanes. OC1 has been used for classification of
data from several real world domains, such as astronomy and cancer
diagnosis. A technical decription of the algorithm can be found in
the AAAI-93 paper by Sreerama K. Murthy, Simon Kasif, Steven Salzberg
and Richard Beigel. A postscript version of this paper is included in
the distribution. OC1 is a written entirely in ANSI C. OC1 is
available by anonymous ftp from
blaze.cs.jhu.edu:/pub/oc1/ [128.220.13.50]
This distribution is provided for non-commercial purposes only. For
more information, contact Sreerama K. Murthy <mur...@cs.jhu.edu>
(primary contact), Steven Salzberg <salz...@cs.jhu.edu>, or Simon
Kasif <ka...@cs.jhu.edu>, Department of Computer Science, The Johns
Hopkins University, Baltimore, MD 21218.
Set-Enumeration (SE) Trees for Induction/Classification. Significant
research in Machine Learning, and in Statistics, has been devoted to
the induction and use of decision trees as classifiers. An induction
framework which generalizes decision trees using a Set-Enumeration
(SE) tree is outlined in
Rymon, R. (1993), An SE-tree-based Characterization of the Induction
Problem. In Proc. of the Tenth International Conference on Machine
Learning, Amherst MA, pp. 268-275.
In this framework, called SE-Learn, rather than splitting according to
a single attribute, one recursively branches on all (or most) relevant
attributes. An induced SE-tree can be shown to economically embed many
decision trees, thereby supporting a more expressive hypothesis
representation. Also, by branching on many attributes, SE-Learn
removes much of the algorithm-dependent search bias. Implementations
of SE-Learn can benefit from many techniques developed for decision
trees (e.g., attribute-selection and pruning measures). In particular,
SE-Learn can be tailored to start off with one's favorite decision
tree, and then improve upon it by further exploring the SE-tree. This
hill-climbing algorithm allows trading time/space for added accuracy.
Current studies (yet unpublished) show that SE-trees are particularly
advantageous in domains where (relatively) few examples are available
for training, and in noisy domains. Finally, SE-trees can provide a
unified framework for combining induced knowledge with knowledge
available from other sources (Rymon, 1994).
Rymon, R. (1994), On Kernel Rules and Prime Implicants. To appear in
Proc. of the Twelfth National Conference on Artificial Intelligence,
Seattle WA.
A Lisp implementation of SE-Learn is available from Ron Rymon
<Ry...@ISP.Pitt.edu>. A commercial version in C is currently under
development.
MLC++ is a Machine Learning library of C++ classes being developed at
Stanford. More information about the library can be obtained at URL
http://robotics.stanford.edu:/users/ronnyk/mlc.html
The utilities are available by anonymous ftp from
starry.stanford.edu:/pub/ronnyk/mlc/util/
They are currently provided only as object code for Sun, but source code
will be distributed to sites that wish to port the code to other compilers.
For more information write to Ronny Kohavi <ron...@CS.Stanford.EDU>.
Mathematics:
SymbMath is a "symbolic calculator that can solve symbolic math
problems" written by Weiguang Huang <w.h...@unsw.edu.au>. It runs on
IBM PCs (8086) under MS-DOS. Shareware versions are available by
anonymous ftp from
wsmr-simtel20.army.mil:/calculator/sm22a.zip
rana.cc.deakin.oz.au:/huang/sm22a.zip
from the URL
http://acsusun.acsu.unsw.edu.au/~s9300078/symbmath.html
or by e-mail from list...@vm1.nodak.edu (list...@ndsuvm1.bitnet). To
subscribe to the symb...@explode.unsw.edu.au mailing list, send email
to majo...@explode.unsw.edu.au with
subscribe symbmath
in the message body.
Medical Reasoning:
TMYCIN -- sumex-aix.stanford.edu:/tmycin
Natural Language Processing:
YACC -- ftp.cs.cmu.edu:/user/ai/lang/lisp/code/parsing/lalr/
Contact: Mark Johnson <m...@cs.brown.edu>
Lisp YACC/Parser.
BABBLER -- Contact: rs...@ra.msstate.edu
Markov chains/NLP
PENMAN -- Contact: ho...@isi.edu
Natural Language Generation.
PC-KIMMO -- msdos.archive.umich.edu:/msdos/linguistics/pckim105.zip
An implementation of KIMMO morphological analyzer
for the IBM PC.
FUF -- Contact: elh...@bengus.bgu.ac.il
ftp: black.bgu.ac.il:/pub/fuf/fuf5.2.tar.Z
cs.columbia.edu:/pub/fuf/fuf5.2.tar.Z
Natural language generation system based on
Functional Unification Grammars.
Includes unifier, large grammar of English (surge)
user manual and many examples. Written in Common Lisp.
[A WAM-based C compiler for FUF is in the works.]
RegEx -- csd4.csd.uwm.edu:/pub/compilers/regex/
Translates regular expressions to DFAs. Written in C.
Mark Hopkins <ma...@csd4.csd.uwm.edu>
Tom -- csd4.csd.uwm.edu:/pub/compilers/tomita/
C implementation of the Tomita parsing algorithm
Mark Hopkins <ma...@csd4.csd.uwm.edu>
Common Lisp versions of the miniature natural language understanding
programs from "Inside Computer Understanding" by Schank and Riesbeck,
1981, are available by anonymous ftp from
cs.umd.edu:/pub/schank/icu/
This includes the SAM and ELI miniatures. It will
eventually include copies of the miniature versions of PAM, POLITICS,
and Tale-Spin. The FOR macro is also available in this directory, as
are a set of functions for manipulating and matching lisp
representations of Conceptual Dependency formulas. Contact Bill
Andersen <waa...@cs.umd.edu> for more information.
The Link Parser is a highly efficient English parser written by Danny
Sleator and Davy Temperley. It uses a novel grammatical formalism known
as Link Grammar to represent a robust and diverse collection of
English-language phenomena. The system is available by anonymous ftp from
ftp://ftp.cs.cmu.edu/user/sleator/link-grammar/
Read the README file for more information. To see an online demo of
the parser, visit
http://bobo.link.cs.cmu.edu/cgi-bin/grammar/build-intro-page.cgi
Further information can be found on Danny Sleator's web page,
http://www.cs.cmu.edu/~sleator
The Xerox part-of-speech tagger is available by anonymous ftp from
parcftp.xerox.com:/pub/tagger/tagger-1-0.tar.Z. It is implemented in
Common Lisp and has been tested in Allegro CL 4.1, CMU CL 16e, and
Macintosh CL 2.0p2. For more information, contact the authors, Doug
Cutting <cut...@parc.xerox.com>, and Jan Pedersen
<pede...@parc.xerox.com>.
Eric Brill's trainable rule-based part of speech tagger (version 1.0.2)
is available by anonymous ftp from
ftp.cs.jhu.edu:/pub/BRILL/Programs/
This tagger is based on transformation-based error-driven learning, a
technique that has been effective in a number of natural language
applications, including part of speech and word sense tagging,
prepositional phrase attachment, and syntactic parsing. For more
information, you can obtain relevant papers in
ftp.cs.jhu.edu:/pub/BRILL/Papers/
If you do download the tagger and wish to be on the mailing list for
future releases, bug reports, etc, please send mail to Eric Brill
<br...@cs.jhu.edu> or <br...@goldilocks.lcs.mit.edu>.
The Prolog and DCG programs from Pereira and Shieber's book, "Prolog
and Natural Language Analysis", are available by anonymous ftp from
das.harvard.edu:/pub/shieber/pnla/. See the file README for the
conditions under which the material is distributed. If you retrieve
the files, please send an email message to the authors letting them
know how you plan to use them. For further information, write to
Fernando Pereira <per...@research.att.com> or Stuart Shieber
<shi...@das.harvard.edu>.
LHIP is a left-head-corner island parser compiler. The system compiles
grammar rules to Prolog code in much the same way as the Prolog DCG
system does. The rules themselves are an extended version of the DCG
rules, allowing optional constituents, negation, disjunction, the
specification of adjacency, and the ability to mark multiple heads in
a rule body. It requires an Edinburgh style Prolog and is known to
work in Sicstus 0.6. LHIP may be retrieved by anonymous ftp from
issun14.unige.ch:/pub/lhip_v1.1.tar.Z [129.194.177.14]
A more efficient version withou negation is also available:
issun14.unigh.ch:/pub/plhip_v1.0.tar.Z [129.194.177.14]
Both are also available from:
ftp.cs.cmu.edu:/user/ai/areas/nlp/parsing/lhip/lhip_v10.tar.gz
Please send a message to the author, Afzal Ballim <af...@divsun.unige.ch>,
to let him know that you're using the package.
PAPPI is a Prolog-based natural language parser for theories in the
Principles-and-Parameters framework. The PAPPI system includes an
X Windows user interface and a sample implementation of classic GB
theory. PAPPI is available by anonymous FTP from
external.nj.nec.com:/pub/sandiway/Pappi-2.0f.tar.gz
For more information, please contact Dr. Sandiway Fong
<sand...@research.nj.nec.com>.
Hdrug is an environment to develop logic grammars, parsers, and
generators for natural languages. The package comes with a number of
example grammars, including a Categorial Grammar, a Tree Adjoining
Grammar, a Unification Grammar in the spirit of Head-driven Phrase
Structure Grammar, an Extraposition Grammar, a Definite Clause
Grammar, and a port of the HPSG grammar from Bob Carpenter's ALE
system. Each of the grammars comes with a set of parsers, such as
Earley-like chart parsers, left-corner parsers and head-driven
parsers. Some grammars come with variants of the head-driven
generator. The package allows easy comparison of different
parsers/generators, extensive possibilities of compiling feature
equations into Prolog terms, graphical (Tk), LaTeX and ordinary Prolog
output of trees, feature structures and Prolog terms, and plotted
graphs and tables of statistical information. Hdrug runs in Sicstus
Prolog and requires ProTcl and Tcl/Tk. It is available by anonymous
FTP from
tyr.let.rug.nl:/pub/prolog-app/Hdrug/
or by WWW from
http://tyr.let.rug.nl/~vannoord/prolog-app/Hdrug/
For more information, write to Gertjan van Noord <vann...@let.rug.nl>.
Neural Networks:
A draft review of roughly 40 neurosimulators is available by anonymous
ftp from
ftp.mrc-apu.cam.ac.uk:/pub/nn/
as the file neurosim1.ps.Z (text version in neurosim1.txt and
WordPerfect 5.1 version in neurosim1.w51.Z). The review will appear in
the "Handbook of Brain Research and Neural Networks" (MIT Press, 1995).
Please send comments to Dr. Jacob M.J. Murre <jaap....@mrc-apu.cam.ac.uk>.
Aspirin/MIGRAINES is a neural network simulator available free from the
MITRE Corporation. It contains a neural network simulation code generator
which generates high performance C code implementations for
backpropagation networks. It runs on the following platforms: Apollo,
Convex, Cray, DecStation, HP, IBM RS/6000, Intel 486/386 (Unix System V),
NeXT, News, Silicon Graphics Iris, Sun3, Sun4, Mercury i860 (40MHz)
Coprocessors, Meiko Computing Surface w/i860 (40MHz) Nodes, Skystation
i860 (40MHz) Coprocessors, and iWarp Cells. The software is available by
anonymous ftp from the CMU simulator collection on pt.cs.cmu.edu
(128.2.254.155) in the directory /afs/cs/project/connect/code (you must
cd to this directory in one atomic operation) and UCLA's cognitive
science collection on ftp.cognet.ucla.edu [128.97.8.19] in the
directory alexis as the file am6.tar.Z, am6.readme, am6.notes. They
include many examples in the release, include an implementation of NETtalk.
For more information, contact Russell Leighton <tay...@world.std.com>
or <leig...@mitre.org>. [As of 7/7/93, the mitre email address bounced.]
MUME (Multi-Module Neural Computing Environment) is a simulation
environment for multi-modules neural computing. It provides an object
oriented facility for the simulation and training of multiple nets
with various architectures and learning algorithms. The object
oriented structure makes simple the addition of new network classes
and new learning algorithms. MUME includes a library of network
architectures including feedforward, simple recurrent, and
continuously running recurrent neural networks. Each architecture is
supported by a variety of learning algorithms, including backprop,
weight perturbation, node perturbation, and simulated annealing. MUME
can be used for large scale neural network simulations as it provides
support for learning in multi-net environments. It also provide pre-
and post-processing facilities. MUME can be used to include
non-neural computing modules (decision trees, etc.) in applications. _
MUME is being developed at the Machine Intelligence Group at Sydney
University Electrical Engineering. The software is written in 'C' and
is being used on Sun and DEC workstations. Efforts are underway to
port it to the Fujitsu VP2200 vector processor using the VCC
vectorising C compiler, HP 9000/700, SGI workstations, DEC
Alphas, and PC DOS (with DJGCC). MUME is available to research
institutions on a media/doc/postage cost arrangement after
signing a license agreement. The license agreement is available by
anonymous ftp from mickey.sedal.su.oz.au:/pub/license.ps [129.78.24.170].
An overview of mume is available from the same machine as
/pub/mume-overview.ps.Z. It is also available free for MSDOS by
anonymous ftp from
brutus.ee.su.oz.au:/pub/MUME-0.5-DOS.zip
For further information, write to Marwan Jabri, SEDAL, Sydney
University Electrical Engineering, NSW 2006 Australia,
call +61-2-692-2240, fax +61-2-660-1228, or send email to
Marwan Jabri <mar...@sedal.su.oz.au>. To be added to the mailing
list, send email to mume-r...@sedal.su.oz.au.
Adaptive Logic Network (ALN)
The atree adapative logic network simulation package is available by
anonymous ftp from
ftp.cs.ualberta.ca:pub/atree/ [129.128.4.241]
as the file atree2.tar.Z (Unix). The MS-Windows 3.x version for the
IBM PC is available as either atre27.exe (includes C/C++ sources) or
a27exe.exe (just the executables). The PC version has a lot more
documentation than the Unix version. The Unix version has been ported
to the Macintosh, Amiga, and other machines. Documentation is in
atree2.ps.Z. Also in this directory is a rather impressive OCR demo
using atree. To be added to the mailing list, send email to
alnl-r...@cs.ualberta.ca. For more information, contact William W.
Armstrong, <ar...@cs.ualberta.ca>.
BPS
Neural network simulator. Other files of interest. Executables are
free; source code for a small fee.
gmuvax2.gmu.edu:nn [no longer there?]
NeuralShell
Availible by anonymous ftp from
quanta.eng.ohio-state.edu:/pub/NeuralShell/ [128.146.35.1]
as the file NeuralShell.tar. [No longer available, due to an
alleged trademark infringement.]
CONDELA
A neural network definition language.
tut.cis.ohio-state.edu:/pub/condela
ROCHESTER CONNECTIONIST SIMULATOR
Available from ftp.cs.rochester.edu:/pub/packages/simulator [192.5.53.209].
Includes a backprop package and an X11/SunView interface.
UCLA-SFINX
retina.cs.ucla.edu:/pub/sfinx_v2.0.tar.Z [131.179.16.6]
Use username sfinxftp, password joshua. Contact sf...@retina.cs.ucla.edu
for more information.
XERION
A neural network simulator from Drew van Camp at the University
of Toronto. It provides a library of routines for building networks
and graphically displaying them. Written in C and uses the X window
system for graphics. Example simulators include Back Propagation,
Recurrent Back Propagation, Boltzmann Machine, Mean Field Theory, Free
Energy Manipulation, Kohonnen Net, and Hard and Soft Competitive
Learning. Xerion runs on SGI Personal Iris, SGI 4d, Sun3 (SunOS), Sun4
(SunOS). Available by anonymous ftp from
ai.toronto.edu:/pub/xerion/
See the file /pub/xerion.README for more information. Also included
is a little program called sciam that contains the basic kernel that
was published in the September 1992 issue of Scientific American.
To be added to the mailing list, send mail to xerion-...@ai.toronto.edu.
Bugs should be reported to xerio...@ai.toronto.edu. Complaints,
suggestions or comments may be sent to xer...@ai.toronto.edu.
SNNS (Stuttgart Neural Network Simulator) is a software simulator for
neural networks on Unix workstations developed at the Institute for
Parallel and Distributed High Performance Systems (IPVR) at the
University of Stuttgart. The SNNS simulator contains a simultor kernel
written in ANSI C and a 2D/3D graphical user interface running under
X11R4/X11R5. It runs under Sun Sparc (SLC, ELC, SS2, GX, GS), DECstation
(2100, 3100, 5000/200), IBM RS 6000, HP 9000, and IBM-PC (386/486). SNNS
includes the following learning procedures: backpropagation (online,
batch, with momentum and flat spot elimin., time delay),
counterpropagation, quickprop, backpercolation 1, and generalized radial
basis functions (RBF), RProp, recurrent ART1, ART2 and ARTMAP, Cascade
Correlation and Recurrent Cascade Correlation, Dynamic LVQ, and Time
delay networks (TDNN). (Elman networks and some other network paradigms
have already been implemented but are scheduled for a later release.)
The SNNS simulator can be obtained via anonymous ftp from
ftp.informatik.uni-stuttgart.de:/pub/SNNS/SNNSv2.1.tar.Z [129.69.211.2].
The PostScript version of the user manual can be obtained as file
SNNSv2.1.Manual.ps.Z. To be added to the mailing list, send a message
to list...@informatik.uni-stuttgart.de with "subscribe snns <Your Full
Name>" in the message body. Submissions may be sent to
sn...@informatik.uni-stuttgart.de. For further information, contact
Andreas Zell, <ze...@informatik.uni-stuttgart.de>.
NEOCOGNITRON SIMULATOR
The Neocognitron Simulator is written in C and is available by
anonymous ftp from
tamsun.tamu.edu:/pub/neocognitron.tar.Z [128.194.15.32]
unix.hensa.ac.uk:/pub/uunet/pub/ai/neural/neocognitron.tar.Z
[129.12.21.7]
PLANET (aka SunNet)
Simulator that runs under X Windows. Written by Yoshiro Miyata
<miy...@sccs.chukyo-u.ac.jp> of Chukyo University, Japan.
Available by anonymous ftp from
tutserver.tut.ac.jp:/pub/misc/PlaNet5.7.tar.Z [133.15.64.6]
boulder.colorado.edu:/pub/generic-sources/PlaNet5.7.tar.Z [128.138.240.1]
Includes documentation.
LVQ_PAK and SOM_PAK
LVQ_PAK (Learning Vector Quantization) and SOM_PAK (Self-Organizing Maps)
were written by the LVQ/SOM Programming Team of the Helsinki
University of Technology, Laboratory of Computer and Information
Science, Rakentajanaukio 2 C, SF-02150 Espoo, FINLAND. The PAKs
run in Unix and MS-DOS systems. Available by anonymous ftp from
cochlea.hut.fi:/pub/lvq_pak/ [130.233.168.48]
cochlea.hut.fi:/pub/som_pak/
ToolDiag
ToolDiag is a feature selection program that increases the accuracy of
classifiers and reduces their complexity by providing them with a
subset containing only the most relevant features. It has interfaces
to LVQ_PAK and SNNS, and uses a data file format that is compatible
with that of LVQ_PAK. The 2-d graphics can be displayed using the
GNUPLOT plotting package. ToolDiag implements many concepts from
Devijver and Kittler's book "Pattern Recognition -- A Statistical
Approach" (Prentice Hall, 1982), including the optimal branch and
bound search strategy, together with several different selection
criteria. ToolDiag can also perform an error estimation using the
leave-one-out method and a K-nearest-neighbor classifier. It also
includes a learning module (Q*) that has the same functionality as
LVQ. ToolDiag cannot handle missing values and requires continuous or
ordered discrete numerical features. ToolDiag is implemented in C and
documentation and source code are available by anonymous ftp from
ftp.fct.unl.pt:/pub/di/packages
For more information, contact Thomas Rauber <t...@fct.unl.pt>.
MACTIVATION
ftp.cs.colorado.edu:/pub/cs/misc/ [128.138.243.151]
as the file Mactivation-3.3.sea.hqx.
DartNet
A Macintosh-based Neural Network Simulator with a nice graphical
interface. Available by anonymous ftp from
dartvax.dartmouth.edu:/pub/mac/dartnet.sit.hqx [129.170.16.4]
or by email from bhar...@dartmouth.edu. New network architectures
and learning algorithms can be added to the system by writing small
XCMD-like CODE resources called nDEF's ("Network Definitions"). For
more information, send email to Sean P. Nolan,
<se...@coos.dartmouth.edu>. [As of 7/7/93, email bounced.]
NevProp is a C implementation of general purpose backpropagation
software, based on Quickprop 1.0 by Scott Fahlman, as translated from
Common Lisp into C by Terry Regier. It runs on Unix, Macintosh, and
DOS. The quickprop algorithm itself has not changed substantially, but
it now includes options to force gradient descent (per-epoch or
per-pattern), generalization & stopped training, c index, and interface
enhancements. It is available by anonymous ftp from
unssun.scs.unr.edu:/pub/goodman/nevpropdir/ [134.197.10.128]
as the file npxxx.shar (replace xxx with the version number) or
from the CMU Simulator Collection. For further information, contact
Phil Goodman <goo...@unr.edu>.
TCS (Tasmanian Connectionist Simulator) is a neural network
simulation package written in Borland C++ for Windows available by
anonymous ftp from
ftp.psychol.utas.edu.au:/pub/tcs [131.217.35.98]
For further information, write to Zoltan Schreter Dept. Psychology
University of Tasmania Hobart, Tasmania AUSTRALIA,
<zol...@psychnet.psychol.utas.edu.au>.
The HYPERPLANE ANIMATOR is a program that allows convenient graphical
display of the training data and weights in a back-propagation neural
network. As learning progresses and the weights in a neural net
alter, the hyperplane positions move. At the end of the training they
are in positions that roughly divide training data into partitions,
each of which contains only one class of data. Observations of
hyperplane movement can yield valuable insights into neural network
learning. The Animator, developed by Lori Pratt and Steve Nicodemus
of the Colorado School of Mines, uses the Motif toolkit on an IBM
RS6000 with X-Windows. The system currently animates only hyperplanes
representing input-to-hidden weights. The animator is available by
anonymous ftp from
mines.colorado.edu:/pub/software/hyperplane-animator/ [138.67.1.3]
as the file hyperplane-animator.tar. An openwindows version of the
animator is available by anonymous ftp from
cs.rutgers.edu:/pub/hyperplane.animator
For more information, write to lpr...@mines.colorado.edu.
SUZY is a simple neural net classifier system for PCs written in C++
and Turbo Vision. RBFs are used to implement the classifier system
with a class-based algorithm being applied to find the centres and
radii of the RBS units. The program is not intended for any serious
applications and is quite slow, but may be of interest to some people.
It is available by anonymous ftp from
rhino.cis.vutbr.cz:/pub/software/ai/suzy.tar.Z [147.229.3.10]
For further information, contact tgr...@psycho.fme.vutbr.cz.
MBP (Matrix Back Propagation) is an efficient implementation of the
back-propagation algorithm for current-generation workstations. The
algorithm includes a per-epoch adaptive technique for gradient
descent. All the computations are done through matrix multiplications
and make use of highly optimized C code. The goal is to reach almost
peak-performances on RISCs with superscalar capabilities and fast
caches. On some machines (and with large networks) a 30-40x speed-up
can be measured respect to conventional implementations.
The software is available by anonymous ftp from
risc6000.dibe.unige.it:/pub/ [130.251.89.154]
as MBPv1.1.tar.Z (unix version) and MBPv11.zip (DOS version). The
documentation is included in the distribution as the postscript file
mbpv11.ps. For more information, contact Davide Anguita
<ang...@dibe.unige.it> or <ang...@icsi.berkeley.edu>.
THE BRAIN is a neural network (backpropagation) simulator for MSDOS
systems. It is simple enough to be used by non-technical people,
yet sophisticated enough for serious research work. It is available
by anonymous ftp from
ftp.technion.ac.il:/pub/unsupported/dos/local/ [132.68.1.10]
ftp.tu.clausthal.de:/pub/msdos/misc/ [139.174.2.10]
as the file brain12.zip. For more information, write to
David Perkovic <d...@mep.com> or <perk...@cleese.apana.org.au>.
PO Box 712, Noarlunga Center SA 5168, Australia.
Neural Systems (Biological Simulation):
BIOSIM is a biologically-oriented neural network simulator. It
implements four neuron models: a simple model only switching ion
channels on and off, the original Hodgkin-Huxley model, the SWIM model
(a modified HH model) and the Golowasch-Buchholz model (the most
enhanced model). Dendrites consist of a chain of segments without
bifurcation. It is in the public domain and runs on Unix workstations
(a less-powerful PC version is also available). BIOSIM includes a
graphical user interface and was designed for research and teaching.
It is available by anonymous ftp from
ftp.uni-kl.de:/pub/bio/neurobio [131.246.9.95]
For more information, write to Stefan Bergdoll <berg...@zxa.basf-ag.de>.
GENESIS (GEneral NEural SImulation System) is a general purpose
simulation platform which supports the simulation of neural systems
ranging from complex models of single neurons to simulations of large
networks made up of more abstract neuronal components. Most current
GENESIS applications involve realistic simulations of biological
neural systems. Although the software can also model more abstract
networks, other simulators are more suitable for backpropagation and
similar connectionist modeling. GENESIS and its graphical front-end
XODUS are written in C and run on SUN and DEC graphics work stations
under UNIX (Sun version 4.0 and up, Ultrix 3.1, 4.0 and up), and
X-windows (versions X11R3, X11R4, and X11R5). The current version of
GENESIS has also been used with Silicon Graphics (Irix 4.0.1 and up)
and the HP 700 series (HPUX). The distribution includes full source
code and documentation for both GENESIS and XODUS as well as fourteen
demonstration and tutorial simulations. Documentation for these
simulations is included, along with three papers that describe the
general organization of the simulator. GENESIS is available by
anonymous ftp from genesis.cns.caltech.edu (131.215.137.64). Before
using ftp, you must telnet to genesis.cns.caltech.edu and login as the
user "genesis" (no password required) to register. If you answer all
the questions asked of you an 'ftp' account will automatically be
created for you. You can then 'ftp' back to the machine and download
the software. Further inquiries concerning GENESIS may be addressed
to gen...@cns.caltech.edu.
Probabilistic Reasoning:
BELIEF is a Common Lisp implementation of the Dempster and Kong fusion
and propagation algorithm for Graphical Belief Function Models and the
Lauritzen and Spiegelhalter algorithm for Graphical Probabilistic
Models. It includes code for manipulating graphical belief models such
as Bayes Nets and Relevance Diagrams (a subset of Influence Diagrams)
using both belief functions and probabilities as basic representations
of uncertainty. It is available by anonymous ftp from
ftp.stat.washington.edu [128.95.17.34]
and by email from the author, Russell Almond <alm...@stat.washington.edu>.
Contact the author at alm...@statsci.com for information about a
commercial version GRAPHICAL-BELIEF currently in the prototype stages.
IDEAL is a LISP system developed for building and evaluating influence
diagrams and Bayesian networks. It is accompanied with a graphical
user interface (CLIM-based) for constructing, editing, and solving
belief networks and influence diagrams. For more information, write
to srin...@rpal.rockwell.com.
Planning:
NONLIN -- cs.umd.edu:/pub/nonlin (128.8.128.8)
Contact: nonlin-use...@cs.umd.edu
nonli...@cs.umd.edu
AbTweak is a complete hierarchical, non-linear planner that extends
David Chapman's (MIT 1986) "Tweak" planner as described by
Yang (Waterloo) and Tenenberg (Rochester) in 1989. This implementation
by Steven Woods (1991 Masters Thesis) includes a complete search
strategy suited to abstraction hierarchies known as LEFT-WEDGE (Woods 1991).
This planner and related work predates that of SNLP. AbTweak has a
WWW homepage containing source & related papers accessible on
http://logos.uwaterloo.ca/sgwoods/
AbTweak is also available by anonymous FTP from
logos.uwaterloo.ca:/pub/abtweak/
For more information send mail to Qiang Yang <qy...@logos.uwaterloo.ca>.
RHETORICAL -- ftp.cs.rochester.edu:/pub/packages/knowledge-tools
Contact: Brad Miller <mil...@cs.rochester.edu>
SNLP -- cs.washington.edu:/pub/snlp.tar.Z
Contact: we...@cs.washington.edu
Nonlinear planner.
IDM -- sauquoit.gsfc.nasa.gov (128.183.101.29)
Contact: idm-...@chelmsford.gsfc.nasa.gov
STRIPS-like planning.
PRODIGY -- Contact: pro...@cs.cmu.edu
Integrated Planning and Learning System
SOAR -- ftp.cs.cmu.edu:
/afs/cs.cmu.edu/project/soar/public/Soar5/ -- Lisp Version
/afs/cs.cmu.edu/project/soar/public/Soar6/ -- C Version
Contact: soar-r...@cs.cmu.edu
Integrated Agent Architecture.
Supports learning through chunking.
----------------------------------------------------------------
Subject: [5-2b] FTP and Other Resources: Qualitative Reasoning --
Theorem Proving
Qualitative Reasoning/Qualitative Physics:
QSIM -- cs.utexas.edu:/pub/qsim
Contact: Ben Kuipers <kui...@cs.utexas.edu>
QPE -- multivac.ils.nwu.edu:/pub/QPE
contact: Prof. Kenneth D. Forbus <for...@ils.nwu.edu>
Qualitative Process Engine (an implementation of QP theory)
Robotics (Planning Testbeds and Simulators):
See Steve Hanks, Martha E. Pollack, and Paul R. Cohen, "Benchmarks,
Test Beds, Controlled Experimentation, and the Design of Agent
Architectures", AI Magazine 14(4):17-42, Winter 1993.
The ARS MAGNA abstract robot simulator provides an abstract world in
which a planner controls a mobile robot. This abstract world is more
realistic than typical blocks worlds, in which micro-world simplifying
assumptions do not hold. Experiments may be controlled by varying
global world parameters, such as perceptual noise, as well as building
specific environments in order to exercise particular planner
features. The world is also extensible to allow new experimental
designs that were not thought of originally. The simulator also
includes a simple graphical user-interface which uses the CLX
interface to the X window system. ARS MAGNA can be obtained by
anonymous ftp from
ftp.cs.yale.edu:/pub/nisp
as the file ars-magna.tar.Z. Installation instructions are in the file
Installation.readme. The simulator is written in Nisp, a macro-package
for Common Lisp. Nisp can be retrieved in the same way as the
simulator. Version 1.0 of the ARS MAGNA simulator is documented in
Yale Technical Report YALEU/DCS/RR #928, "ARS MAGNA: The Abstract
Robot Simulator". This report is available in the distribution as a
PostScript file. Comments should be directed to Sean Philip
Engelson <enge...@cs.yale.edu>.
Erratic, a mobile robot simulator and controller by kono...@ai.sri.com is
available by anonymous ftp from
ftp.ai.sri.com:pub/konolige/erratic-ver1.tar.Z
The Michigan Intelligent Coordination Experiment (MICE) testbed is a
tool for experimenting with coordination between intelligent systems
under a variety of conditions. MICE simulates a two-dimensional
grid-world in which agents may move, communicate, and affect their
environment. MICE is essentially a discrete-event simulator that
helps control the domain and a graphical representation, but provides
relatively few constraints on the form of the domain and the agents'
abilities. Users may specify the time required by various activities,
the constraints on an agents' sensors, the configuration of the domain
and its properties, etc. MICE runs under XWindows on Un*x boxes, on
Macs, and on TI Explorers, with relatively consistent graphical
displays. Source code, documentation, and examples are available via
anonymous ftp to ftp.eecs.umich.edu:/software/Mice/Mice.tar.Z. MICE was
produced by the University of Michigan's Distributed Intelligent Agent
Group (UM DIAG). For further information, write to
umdia...@caen.engin.umich.edu.
RSIM, a SGI-based simulator from the University of Melbourne, with very
nice graphics, is available by anonymous ftp from
krang.vis.citri.edu.au:/pub/robot
Write to cdi...@vis.citri.edu.au for more information.
Simderella is a robot simulator consisting of three programs: CONNEL
(the controller), SIMMEL (the robot simulator), and BEMMEL (the
X-windows oriented graphics back-end). SIMMEL performs a few matrix
multiplications, based on the Denavit Hartenberg method, calculates
velocities with the Newton-Euler scheme, and communicates with the
other two programs. BEMMEL only displays the robot. CONNEL is the
controller, which must be designed by the user (in the distributed
version, CONNEL is a simple inverse kinematics routine.) The programs
use Unix sockets for communication, so you must have sockets, but you
can run the programs on different machines. The software is available
by anonymous ftp from
galba.mbfys.kun.nl:/pub/neuro-software/pd/ [131.174.82.73]
as the file simderella.2.0.tar.gz. The software has been compiled using
gcc on SunOS running under X11R4/5 on Sun3, Sun4, Sun Sparc 1, 2, and
10, DEC Alpha, HP700, 386/486 (Linux), and Silicon Graphics
architectures. For more information, send email to Patrick van der
Smagt, <sm...@fwi.uva.nl>.
TILEWORLD -- cs.washington.edu:/new-tileworld.tar.Z
Planning testbed
Search:
AISEARCH is a C++ class library for search algorithms implemented by
Peter Bouthoorn <pe...@icce.rug.nl>. It includes implementations of
DFS, BFS, uniform cost, best-first, bidirectional DFS/BFS, and AND/OR
DFS/BFS search algorithms. It is available by anonymous ftp from
obelix.icce.rug.nl:/pub/peter/ as aisearch.zip or aisearch.tar.Z.
Simulated Annealing:
ASA (Adaptive Simulated Annealing) is a powerful global optimization
C-code algorithm especially useful for nonlinear and/or stochastic
systems. Most current copies can be obtained by anonymous ftp from
ftp.alumni.caltech.edu:/pub/ingber/ASA.tar.gz [131.215.48.62]
an uncompressed version, asa, also is in that archive. There are several
related (p)reprints in the Caltech archive, including sa_pvt93.ps.Z,
"Simulated annealing: Practice versus theory." The first VFSR code was
developed by Lester Ingber in 1987, and the reprint of that paper is
vfsr89.ps.Z, "Very fast simulated re-annealing". If you cannot use
ftp or ftpmail, then copies of the code are also available by email
from the author at ing...@alumni.caltech.edu. To be added to the
mailing list, send mail to asa-r...@alumni.caltech.edu.
The VFSR code was made publicly available in 1992 under the GNU GPL, by
Lester Ingber and Bruce Rosen. The last version of that code before
the introduction of ASA is available via anonymous ftp from
ringer.cs.utsa.edu:/pub/rosen/vfsr.tar.Z. Bruce Rosen has a comparison
study, "Function Optimization based on Advanced Simulated Annealing,"
which is available via anonymous ftp from
archive.cis.ohio-state.edu:/pub/neuroprose/rosen.advsim.ps.Z.
[VFSR is no longer supported, but ASA is. --mk]
Speech:
RECNET is a complete speech recognition system for the DARPA TIMIT and
Resource Management tasks. It uses recurrent networks to estimate phone
probabilities and Markov models to find the most probable sequence of
phones or words. The system is a snapshot of evolving research code.
There is no documentation other than published research papers. It is
configured for the two specific databases and is unlikely to be of use as
a complete system for other tasks. It is available by anonymous ftp from
svr-ftp.eng.cam.ac.uk:/misc/recnet-1.3.tar.Z
Related publications can be found in
svr-ftp.eng.cam.ac.uk:/reports/ (see the ABSTRACT file first).
You will need the relevant CDROMs, 150MByte of free space for TIMIT and
300MByte for RM. If you use the code, the author would appreciate an
email message so that he can keep you informed of new releases. Write to
Tony Robinson, <a...@eng.cam.ac.uk>, for more information.
CELP 3.2a is available from super.org:/pub/celp_3.2a.tar.Z
[192.31.192.1] with copies available on
svr-ftp.eng.cam.ac.uk:/comp.speech/sources/ The code (C, FORTRAN,
diskio) all has been built and tested on a Sun4 under SunOS4.1.3. If
you want to run it somewhere else, then you may have to do a bit of
work. (A Solaris 2.x-compatible release is planned soon.) Written by
Joe Campbell <jpc...@afterlife.ncsc.mil> of the Department of
Defense. Distribution facilitated by Craig F. Reese
<cfr...@super.org>, IDA/Supercomputing Research Center.
The OGI Speech Tools are set of speech data manipulation tools
developed at the Center for Spoken Language Understanding (CSLU) at
the Oregon Graduate Institute of Science and Technology (Portland
Oregon). The tools can be used to compute and display signal
representations, label speech at different levels (e.g., phonetic,
phonemic and word), train neural network classifiers, and display the
output of classification or recognition algorithms time-aligned with
the speech. The OGI Speech Tools were written in ANSI C. The OGI
Speech Tools are available by anonymous ftp from
speech.cse.ogi.edu:/pub/tools/
as ogitools.v1.0.tar.Z. For more information, write to Johan Schalkwyk
<to...@cse.ogi.edu>. If you're using the tools, please let Johan know
by sending him a mail message.
PC Convolution is a educational software package that graphically
demonstrates the convolution operation. It runs on IBM PC compatibles
using DOS 4.0 or later. A demo version is available by anonymous ftp
from
ee.umr.edu:/pub/ [131.151.4.11]
as pc_conv.*. University instructors may obtain a free, fully
operational version by contacting Dr. Kurt Kosbar <k...@ee.umr.edu> at
117 Electrical Engineering Building, University of Missouri/Rolla,
Rolla, Missouri, 65401, phone 314-341-4894.
The LOTEC Speech Recognition Package is all you need to build a
single-speaker, small-vocabulary, low-quality continuous speech
recognition module, for use as part of a larger system. It accepts
input in the form of Sun .au format sound files, along with a set
of word templates in the same format, and outputs a lattice of word
hypotheses. LOTEC is available by anonymous ftp from
ftp.sanpo.t.u-tokyo.ac.jp:/pub/nigel/lotec/ [130.69.134.32]
as the files lotec.tar.Z or lotec-no-bin.tar.Z. For more
information, write to Nigel Ward <ni...@sanpo.t.u-tokyo.ac.jp>.
Temporal Reasoning:
See also KNOWBEL above.
MATS -- Metric/Allen Time System
Contact: Henry Kautz <ka...@research.att.com>
MATS is a Common Lisp program which solves temporal
constraint problems. Input constraints are either
difference inequalities or Allen-style qualitative constraints.
TMM -- New implementation of Dean & McDermott's Temporal Map
Manager system written in Common Lisp.
See SIGART Bulletin 4(3), July 1993.
Contact: carc...@src.honeywell.com
MTMM -- Modified version of Dean & McDermott's TMM written in
MCL. Available on diskette.
Contact: Eckehard Gross <gr...@gmd.de>
TimeGraph-- Metric and Qualitative temporal reasoning system which
handles (<, =, >) point relations, bounds on absolute
calendar/clock times, and bounds on durations. Data entry
and retrieval is through interval or point relations.
The system is scalable in the sense that storage
remains linear in the number of relations added.
Efficient retrieval is achieved through a simple
timepoint numbering scheme and metagraph structure.
See SIGART Bulletin 4 (3), pp. 21-25, July 1993.
Contact: Lenhart Schubert (schu...@cs.rochester.edu)
TimeGraph II (TG-II) handles the set of the relations of the Point
Algebra and of the Pointizable Interval Algebra (also called Simple
Interval Algebra by P. van Beek). Temporal relations are represented
through a "timegraph", a graph partitioned into a collection of "time
chains" which are automatically structured for efficiency. The system
is scalable, in the sense that the storage tends to remain linear in
the number of relations asserted. Efficient query handling is achieved
through a time point numbering scheme and a "metagraph" data
structure. TG-II is written in Common Lisp. For a description of the
theory underlying the system see:
[1] Alfonso Gerevini and Lenhart Schubert, "Efficient Temporal
Reasoning through Timegraphs", in Proceedings of IJCAI-93.
[2] Alfonso Gerevini and Lenhart Schubert, "Temporal Reasoning in
TimeGraph I-II", SIGART Bulletin 4(3), July 1993.
[3] Alfonso Gerevini and Lenhart Schubert, "Efficient Algorithms
for Qualitative Reasoning about Time", Artificial Intelligece,
to appear. Also available as IRST Technical Report 9307-44,
IRST 38050 Povo, TN Italy; or Tech. report 496, Computer Science
Department, University of Rochester, Rochester 14627 NY, USA.
TimeGraph II is available by anonymous ftp from
ftp.cs.rochester.edu:/pub/packages/knowledge-tools/
as the files tg-ii.readme and tg-ii-1.tar.gz. If you retrieve a copy
of TimeGraph II by anonymous ftp, please let them know that you've
retrieved a copy by sending a message to
For more information, contact Alfonso Gerevini <gere...@irst.it> or
Lenhart Schubert <schu...@cs.rochester.edu>.
Tachyon -- Performs constraint satisfaction for point-based metric
reasoning. Qualitative constraints are also handled by
translation into quantitative ones. Written in C++.
See SIGART Bulletin 4(3), July 1993.
Contact: Richard Arthur (art...@crd.ge.com)
TimeLogic-- The TimeLogic system is an interval-based forward
chaining inference engine and database manager of
temporal constraints. Relational constraints,
indicating relative order between intervals, are based
on Allen's interval logic. The TimeLogic system also
supports durational constraints, indicating relative
magnitude between intervals, and reference links, used
for the explicit or automatic construction of interval
hierarchies. Constraints are posed and propagated in
user-defined contexts with inheritance. Supports relative
metric constraints but no absolute dates or times.
Written in Common Lisp.
Contact: Peggy Meeker (timelogi...@cs.rochester.edu)
TemPro -- A temporal constraint system that uses both interval
algebra and point-based algebra. Written in Common Lisp.
Contact: J-P Haton <j...@loria.fr> or
F. Charpillet <ch...@loria.fr>
TIE -- Temporal Inference Engine. Written in Common Lisp.
Contact: E. Tsang (Essex University, UK)
TCNM (Temporal Constraint Network Manager) manages non-disjunctive
metric constraints on time-points and on durations in an integrated
way. These constraints allow us express absolute, qualitative and
metric constraints on time-points and on durations, which are managed
in an integrated way. In the updating processes, a non-redundant and
global consistent Temporal Constraint Network is always maintained by
means of an efficient and complete propagation method, with a O(n**2)
temporal complexity. Sound and complete retrieval processes have a
constant cost. Written in Common Lisp. For more information, contact
Federico A. Barber <fba...@dsic.upv.es>. See also SIGART Bulletin
4(3), July 1993.
Theorem Proving/Automated Reasoning:
Coq is the Calculus of Inductive Constructions. It runs in
Caml-Light and is available by anonymous ftp from
ftp.inria.fr:/INRIA/coq/V5.8.3 (unix version)
ftp.inria.fr:/INRIA/coq/V5.8.2 (mac version)
The Mac version is standalone, not requiring Caml-Light. The unix
version requires Caml-Light, however, which is available from
ftp.inria.fr:/lang/caml-light
Documentation is included in the distribution. Questions and comments
should be directed to the Coq hotline <c...@pauillac.inria.fr>.
DTP is a general first-order theorem prover incorporating intelligent
backtracking and subgoal caching, as well as a trace facility that can
display proof spaces graphically. Implemented in CLtL2 Common Lisp, it runs
in Franz Allegro, Lucid, and Macintosh (MCL) Common Lisp. DTP is available
on the Web at
http://logic.stanford.edu/dtp/
Contact Don Geddis <Ged...@CS.Stanford.EDU> for more information.
Elf implements the LF Logical Framework (based on the theory of
dependent types) and gives it a logic programming interpretation in
order to support search and the implementation of other algorithms (e.g.
evaluation or compilation in programming languages). It comes with a
number of examples from logic and the theory of programming languages
such as the Church Rosser theorem for the untyped lambda-calculus and
type soundness for Mini-ML. It is written in Standard ML and includes
some support code for editing and interaction in gnu-emacs. It is
available by anonymous ftp from
ftp.cs.cmu.edu:/afs/cs/user/fp/public/
as the files README (general information), elf-04.tar.Z (Version 0.4
of Elf, 1 Jul 1993), elf-examples.tar.Z (Version 0.4 of Elf examples,
unchanged from Version 0.3), and elf-papers/ (DVI files for papers
related to LF and Elf, including a "tutorial" and a bibliography). For
more information, contact Frank Pfenning <f...@cs.cmu.edu>,
Department of Computer Science, Carnegie Mellon University.
FRAPPS (Framework for Resolution-based Automated Proof Procedures) is
a portable resolution theorem-prover written in Common Lisp. It is
available via anonymous ftp from a.cs.uiuc.edu:/pub/frapps [128.174.252.1].
If you take a copy of FRAPPS, please send a short note to Prof.
Alan M. Frisch <fri...@cs.uiuc.edu>.
Gazer is a sequent calculus based system for first order logic with a
novel inference rule, gazing, that enables the system to determine
which of a possibly large number of definitions and lemmas should be
used at any point in a proof. Available from the authors, Dave
Barker-Plummer <plu...@cs.swarthmore.edu> and Alex Rothenberg
<al...@cs.swarthmore.edu>.
ISABELLE-93. Isabelle is a highly automated generic theorem prover
written in Standard ML. New logics are introduced by specifying their
syntax and rules of inference. Proof procedures can be expressed
using tactics and tacticals. Isabelle comes with 8 different logics,
including LCF, some modal logics, first-order logic, Zermelo-Fraenkel
set theory, and higher-order logic. Isabelle-93 is not upwardly
compatible with its predecessor, but comes with advice on converting
to the new simplifier. Isabelle-93 is available by anonymous ftp from
the University of Cambridge,
ftp.cl.cam.ac.uk:/ml/ [128.232.0.56]
as Isabelle93.tar.gz. It is also available from the Technical
University of Munich,
ftp.informatik.tu-muenchen.de:/lehrstuhl/nipkow/ [131.159.0.198]
The distribution includes extensive documentation, including a 71-page
introduction, an 85-page reference manual, and a 166-page description of
the various logics supplied with Isabelle. For more information, write
to Larry....@cl.cam.ac.uk and Tobias...@informatik.tu-muenchen.de.
An Emacs-Lisp package for Isabelle by David.A...@dcs.ed.ac.uk
is available from
ftp.dcs.ed.ac.uk:/pub/da/isa-mode.tar.gz
The users mailing list is isabell...@cl.cam.ac.uk and is moderated.
KEIM is a collection of software modules, written in Common Lisp with
CLOS, designed to be used in the production of theorem proving
systems. KEIM is intended to be used by those who want to build or
use deduction systems (such as resolution theorem provers) without
having to write the entire framework. KEIM is also suitable for
embedding a reasoning component into another Common Lisp program.
KEIM offers a range of datatypes implementing a logical language of
type theory (higher order logic), in which first order logic can be
embedded. KEIM's datatypes and algorithms include: types; terms
(symbols, applications, abstractions), environments (e.g., associating
symbols with types); unification and substitutions; proofs, including
resolution and natural deduction style. KEIM also provides
functionality for the pretty-printing, error handling, formula parsing
and user interface facilities which form a large part of any theorem
prover. Implementing with KEIM thus allows the programmer to avoid a
great deal of drudgery. KEIM has been tested in Allegro CL 4.1 and
Lucid CL 4.0 on Sun 4 workstations. KEIM is available for
noncommercial use via anonymous FTP from
js-sfbsun.cs.uni-sb.de:/pub/keim/keim*
For more information contact Dan Nesmith, Fachbereich Informatik/AG
Siekmann, Universitaet des Saarlandes, Postfach 1150, D-66041
Saarbruecken, Germany, or send email to ke...@cs.uni-sb.de. A mailing
list for KEIM users is also being set up. Send mail to
keim-user...@cs.uni-sb.de to be put on the list.
MVL -- t.uoregon.edu:/mvl/mvl.tar.Z [128.223.56.46]
Contact: gins...@t.stanford.edu
Multi-valued logics
Boyer-Moore -- ftp.cli.com:/pub/nqthm/nqthm.tar.Z
rascal.ics.utexas.edu:/pub/nqthm 128.83.138.20
See also the pub/proof-checker/ subdirectory, which contains Matt
Kaufmann's proof checking enhancements to nqthm.
Nqthm-1992 is the Boyer-Moore theorem prover. The 1992 version of the
theorem prover is upwardly compatible with the previous (1987)
version. Included in the distribution are thousands of Nqthm-checked
theorems formulated by Bevier, Boyer, Brock, Bronstein, Cowles,
Flatau, Hunt, Kaufmann, Kunen, Moore, Nagayama, Russinoff, Shankar,
Talcott, Wilding, Yu, and others. The release of Nqthm-1992 includes
three revised chapters of the book `A Computational Logic Handbook',
including Chapter 4, on the formal logic for which the system is a
prover, and Chapter 12, the reference guide to user commands. Nqthm
runs in Common Lisp, and has been tested in AKCL, CMU CL, Allegro CL,
Lucid CL, MCL, and Symbolics CL. Nqthm-1992 is available by anonymous
ftp from
ftp.cli.com:/pub/nqthm/nqthm-1992/ [192.31.85.129]
as the file nqthm-1992.tar.Z. See the file README in the same
directory for instructions on retrieving nqthm. See also the
/pub/pc-nqthm/pc-nqthm-1992/
directory (files README-pc and pc-nqthm-1992.tar.Z), which contains
Matt Kaufmann's interactive proof-checking enhancements to Nqthm-1992.
For more information, contact Robert S. Boyer <bo...@cli.com>, J.
Strother Moore <mo...@cli.com>, or Matt Kaufmann <kauf...@cli.com>,
Computational Logic Inc., 1717 West 6th Street, Suite 290, Austin, TX
78703-4776. Send mail to nqthm-use...@cli.com to be added to
the mailing list.
The Nuprl Proof Development System is available by anonymous ftp
from ftp.cs.cornell.edu:/pub/n/. Nuprl should run in any Common
Lisp with CLX. There are also (obsolete) interfaces for Symbolics Lisp
machines and Suns running the SunView window system. Nuprl has been
tested with Allegro, Lucid, AKCL. For further information, contact
Elizabeth Maxwell, <max...@cs.cornell.edu>, Nuprl Distribution
Coordinator, Department of Computer Science, Upson Hall, Cornell
University, Ithaca, NY 14853.
Otter -- info.mcs.anl.gov:/pub/Otter/Otter-2.2/otter22.tar.Z
anagram.mcs.anl.gov:/pub/Otter/
Contact: ot...@mcs.anl.gov
Resolution-based theorem prover.
RRL -- herky.cs.uiowa.edu:/public/rrl [128.255.28.100]
Rewrite Rule Laboratory
See SEQUEL entry in the Lisp FAQ, part 6.
SETHEO -- flop.informatik.tu-muenchen.de:/pub/fki/ [131.159.8.35]
Get the files setheo.info and setheo.tar.Z.
SETHEO (SEquential THEOrem prover) is an automated
theorem prover for formulae of predicate logic.
SETHEO is based on the calculus of ``connection
tableaux''. SETHEO runs on Sun SPARCs only.
Contact: set...@informatik.tu-muenchen.de
XPNet (X Proof Net) is a graphical interface to proof nets with an
efficient proof checker. It is available by anonymous ftp to
ftp.cis.upenn.edu:/pub/xpnet.tar.Z [130.91.6.8]. For further
information, write to Jawahar Chirimar <chir...@saul.cis.upenn.edu>,
Carl A. Gunter <gun...@saul.cis.upenn.edu>, or Myra VanInwegen
<my...@saul.cis.upenn.edu>.
Theorem Proving/Automated Reasoning (Problems):
ATP Problems -- anagram.mcs.anl.gov:/pub/ATP_Problems/*
Collection of ATP problems from Otter, CADE, and JAR.
The problems include algebra, analysis, circuits,
geometry, logic problems, Pelletier's problem set,
program verification, puzzles, set theory, and topology.
The TPTP (Thousands of Problems for Theorem Provers) Problem Library
is a collection of test problems for automated theorem provers (ATPs),
using the clausal normal form of 1st order predicate logic. The goal
of the TPTP is to provide a firm basis for the testing, evaluation,
and comparison of ATP systems through a comprehensive library of ATP
test problems in a general purpose format. The TPTP includes tools to
convert the problems to existing ATP formats, such as the OTTER, MGTP,
PTTP, SETHEO, and SPRFN formats. Each problem includes a list of
references and other relevant information. The TPTP also aims to
supply general guidelines outlining the requirements for ATP system
evaluation. The TPTP can be obtained by anonymous ftp from either the
Department of Computer Science, James Cook University, Australia,
coral.cs.jcu.edu.au:/pub/research/tptp-library/ [137.219.17.4]
or the Institut fuer Informatik, TU Muenchen, Germany,
flop.informatik.tu-muenchen.de:/pub/tptp-library/ [131.159.8.35]
as the files ReadMe (general information about the library),
TPTP-v1.1.0.tar.gz (the library itself), and
TR-v1.0.0.ps.gz (a postscript technical report about the TPTP).
The TPTP is also accessible through WWW using either of the URLs
ftp://coral.cs.jcu.edu.au/users/GSutcliffe/WWW/TPTP.HTML
http://wwwjessen.informatik.tu-muenchen.de/~suttner/tptp.html
Additions and corrections may be sent to Geoff Sutcliffe
<ge...@cs.jcu.edu.au> (Fax: +61-77-814029) or Christian Suttner
<sut...@informatik.tu-muenchen.de> (Fax: +49-89-526502). If you
would like to be kept informed of new versions of the TPTP, please
send email to either of them.
Truth Maintenance:
The truth maintenance system and problem solver implementations
described in the book "Building Problem Solvers" by Ken Forbus and
Johan de Kleer are available by anonymous ftp from
multivac.ils.nwu.edu:/pub/BPS/
parcftp.xerox.com:/pub/bps/
For more information send mail to Johan de Kleer <deK...@parc.xerox.com>.
Send bug reports to bug...@ils.nwu.edu.
Miscellaneous:
University of Toronto:
ftp -- ftp.cs.toronto.edu:/pub/ailist
Archives of ailist mailing list, defunct as of January 19, 1990
PAIL (Portable AI Lab)
ftp -- pobox.cscs.ch:/pub/ai/ [148.187.10.13]
contact: pail...@idsia.ch
authors: Mike Rosner <mi...@idsia.ch>