[5-2b] FTP and Other Resources: Qualitative Reasoning -- Theorem Proving

Qualitative Reasoning/Qualitative Physics:

   QSIM     -- cs.utexas.edu:/pub/qsim
               Contact: Ben Kuipers <kuipers@cs.utexas.edu>

   QPE      -- multivac.ils.nwu.edu:/pub/QPE
               contact: Prof. Kenneth D. Forbus <forbus@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 <engelson@cs.yale.edu>.

   Erratic, a mobile robot simulator and controller by konolige@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
   umdiagmice@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 cdillon@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, <smagt@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 <peter@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 ingber@alumni.caltech.edu. To be added to the
   mailing list, send mail to asa-request@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, <ajr@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 <jpcampb@afterlife.ncsc.mil> of the Department of
   Defense. Distribution facilitated by Craig F. Reese
   <cfreese@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
   <tools@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 <kk@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 <nigel@sanpo.t.u-tokyo.ac.jp>.

Temporal Reasoning:

   See also KNOWBEL above.

   MATS     -- Metric/Allen Time System
               Contact: Henry Kautz <kautz@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: carciofi@src.honeywell.com

   MTMM     -- Modified version of Dean & McDermott's TMM written in
               MCL.  Available on diskette.
               Contact: Eckehard Gross <gross@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 (schubert@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 
      bug-tg2-request@cs.rochester.edu
   For more information, contact Alfonso Gerevini <gerevini@irst.it> or
   Lenhart Schubert <schubert@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 (arthurr@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 (timelogic-request@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 <jph@loria.fr> or
                        F. Charpillet <charp@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 <fbarber@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 <coq@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 <Geddis@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 <fp+@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 <frisch@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 <plummer@cs.swarthmore.edu> and Alex Rothenberg
   <alex@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.Paulson@cl.cam.ac.uk and Tobias.Nipkow@informatik.tu-muenchen.de.
   An Emacs-Lisp package for Isabelle by David.Aspinall@dcs.ed.ac.uk
   is available from  
      ftp.dcs.ed.ac.uk:/pub/da/isa-mode.tar.gz
   The users mailing list is isabelle-users@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 keim@cs.uni-sb.de.  A mailing
   list for KEIM users is also being set up.  Send mail to
   keim-users-request@cs.uni-sb.de to be put on the list.

   MVL      -- t.uoregon.edu:/mvl/mvl.tar.Z [128.223.56.46]
               Contact: ginsberg@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 <boyer@cli.com>, J.
   Strother Moore <moore@cli.com>, or Matt Kaufmann <kaufmann@cli.com>,
   Computational Logic Inc., 1717 West 6th Street, Suite 290, Austin, TX
   78703-4776.  Send mail to nqthm-users-request@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, <maxwell@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: otter@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: setheo@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 <chirimar@saul.cis.upenn.edu>, 
   Carl A. Gunter <gunter@saul.cis.upenn.edu>, or Myra VanInwegen
   <myra@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
   <geoff@cs.jcu.edu.au> (Fax: +61-77-814029) or Christian Suttner
   <suttner@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 <deKleer@parc.xerox.com>.
   Send bug reports to bug-bps@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-info@idsia.ch
      authors: Mike Rosner <mike@idsia.ch> 
               Dean Allemang <allemang@lia.di.epfl.ch>
Go Back Up

Go To Previous

Go To Next