![allanswers.org - Artificial Intelligence FAQ:6/6 AI Software [Monthly posting]](/logo.gif "allanswers.org - Artificial Intelligence FAQ:6/6 AI Software [Monthly posting]"){kind=logo}
|
|
| Home > Science > ai-faq > general > |
Artificial Intelligence FAQ:6/6 AI Software [Monthly posting] |
Section 3 of 3 - Prev - Next
All sections - 1 - 2 - 3
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, .
* RP1 is a Java-based robot simulator. It allows applications to build
arbitrary landscapes and a data-configurable robot which can interact with
a simulated environment or solve a virtual maze. The system provides
abstract features that model real-world objects such as walls, light
sources, and goals. For more information, see:
http://rossum.sourceforge.net
TILEWORLD -- cs.washington.edu:/new-tileworld.tar.Z
Planning testbed
-----------------------------------------------------
Subject: [6-13] Temporal Reasoning - Truth Maintenance
Temporal Reasoning:
See also KNOWBEL above.
MATS -- Metric/Allen Time System
Contact: Henry Kautz
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
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 or
Lenhart Schubert .
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 or
F. Charpillet
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 . 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 .
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. It is
implemented in (CLtL2) Common Lisp, and is available on the web at
http://don.geddis.org/dtp/
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 ,
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 .
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 and Alex Rothenberg
.
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 , J.
Strother Moore , or Matt Kaufmann ,
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, , 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 ,
Carl A. Gunter , or Myra VanInwegen
.
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
(Fax: +61-77-814029) or Christian Suttner
(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 .
Send bug reports to bug-bps@ils.nwu.edu.
-----------------------------------------------------
Subject: [6-14] Search
Search:
AISEARCH is a C++ class library for search algorithms implemented by
Peter Bouthoorn . 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]
________________________________________________________
Subject: [6-14] Constraint Satisfaction
COMERCIAL PRODUCT COMERCIAL PRODUCT COMERCIAL PRODUCT
Koalog Constraint Solver. Koalog Constraint Solver is a
constraint solver written in the JavaTMprogramming language.
It provides technology for solving satisfaction and optimization
problems, including:
* scheduling;
* time-tabling;
* resource-allocation;
* configuration:
COMERCIAL PRODUCT COMERCIAL PRODUCT COMERCIAL PRODUCT
---
[ comp.ai is moderated. To submit, just post and be patient, or if ]
[ that fails mail your article to , and ]
[ ask your news administrator to fix the problems with your system. ]
Section 3 of 3 - Prev - Next
All sections - 1 - 2 - 3
| Back to category general - Use Smart Search |
| Home - Smart Search - About the project - Feedback |
© allanswers.org | Terms of use