Top Document: Artificial Intelligence FAQ: Open Source AI Software 6/6 [Monthly posting] Previous Document: [612] Robotics Next Document: [614] Search See reader questions & answers on this topic!  Help others by sharing your knowledge 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 Allenstyle 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. 2125, July 1993. Contact: Lenhart Schubert (schubert@cs.rochester.edu) TimeGraph II (TGII) 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. TGII 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 IJCAI93. [2] Alfonso Gerevini and Lenhart Schubert, "Temporal Reasoning in TimeGraph III", 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 930744, 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/knowledgetools/ as the files tgii.readme and tgii1.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 bugtg2request@cs.rochester.edu For more information, contact Alfonso Gerevini <gerevini@irst.it> or Lenhart Schubert <schubert@cs.rochester.edu>. Tachyon  Performs constraint satisfaction for pointbased 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 intervalbased 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 userdefined contexts with inheritance. Supports relative metric constraints but no absolute dates or times. Written in Common Lisp. Contact: Peggy Meeker (timelogicrequest@cs.rochester.edu) TemPro  A temporal constraint system that uses both interval algebra and pointbased algebra. Written in Common Lisp. Contact: JP 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 nondisjunctive metric constraints on timepoints and on durations in an integrated way. These constraints allow us express absolute, qualitative and metric constraints on timepoints and on durations, which are managed in an integrated way. In the updating processes, a nonredundant 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 CamlLight and is available by anonymous ftp from ftp://ftp.inria.fr/INRIA/coq/ (unix version) ftp://ftp.inria.fr/INRIA/coq/ (mac version) The Mac version is standalone, not requiring CamlLight. The unix version requires CamlLight, however, which is available from ftp://ftp.inria.fr/lang/ Documentation is included in the distribution. Questions and comments should be directed to the Coq hotline <coq@pauillac.inria.fr>. DTP is a general firstorder 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/ 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 lambdacalculus and type soundness for MiniML. It is written in Standard ML and includes some support code for editing and interaction in gnuemacs. It is available by anonymous ftp from ftp://ftp.cs.cmu.edu/afs/cs/user/fp/public/ as the files README (general information), elf04.tar.Z (Version 0.4 of Elf, 1 Jul 1993), elfexamples.tar.Z (Version 0.4 of Elf examples, unchanged from Version 0.3), and elfpapers/ (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 Resolutionbased Automated Proof Procedures) is a portable resolution theoremprover 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 BarkerPlummer <plummer@cs.swarthmore.edu> and Alex Rothenberg <alex@cs.swarthmore.edu>. ISABELLE93. 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, firstorder logic, ZermeloFraenkel set theory, and higherorder logic. Isabelle93 is not upwardly compatible with its predecessor, but comes with advice on converting to the new simplifier. Isabelle93 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://ftp.informatik.tumuenchen.de/lehrstuhl/nipkow/ [131.159.0.198] The distribution includes extensive documentation, including a 71page introduction, an 85page reference manual, and a 166page description of the various logics supplied with Isabelle. For more information, write to Larry.Paulson@cl.cam.ac.uk and Tobias.Nipkow@informatik.tumuenchen.de. An EmacsLisp package for Isabelle by David.Aspinall@dcs.ed.ac.uk is available from ftp.dcs.ed.ac.uk:/pub/da/isamode.tar.gz The users mailing list is isabelleusers@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 prettyprinting, 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 jssfbsun.cs.unisb.de:/pub/keim/keim* For more information contact Dan Nesmith, Fachbereich Informatik/AG Siekmann, Universitaet des Saarlandes, Postfach 1150, D66041 Saarbruecken, Germany, or send email to keim@cs.unisb.de. A mailing list for KEIM users is also being set up. Send mail to keimusersrequest@cs.unisb.de to be put on the list. MVL  ftp://t.uoregon.edu/mvl/ [128.223.56.46] Contact: ginsberg@t.stanford.edu Multivalued logics BoyerMoore  ftp.cli.com:/pub/nqthm/nqthm.tar.Z rascal.ics.utexas.edu:/pub/nqthm 128.83.138.20 See also the pub/proofchecker/ subdirectory, which contains Matt Kaufmann's proof checking enhancements to nqthm. Nqthm1992 is the BoyerMoore theorem prover. The 1992 version of the theorem prover is upwardly compatible with the previous (1987) version. Included in the distribution are thousands of Nqthmchecked theorems formulated by Bevier, Boyer, Brock, Bronstein, Cowles, Flatau, Hunt, Kaufmann, Kunen, Moore, Nagayama, Russinoff, Shankar, Talcott, Wilding, Yu, and others. The release of Nqthm1992 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. Nqthm1992 is available by anonymous ftp from ftp.cli.com:/pub/nqthm/nqthm1992/ [192.31.85.129] as the file nqthm1992.tar.Z. See the file README in the same directory for instructions on retrieving nqthm. See also the /pub/pcnqthm/pcnqthm1992/ directory (files READMEpc and pcnqthm1992.tar.Z), which contains Matt Kaufmann's interactive proofchecking enhancements to Nqthm1992. 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 787034776. Send mail to nqthmusersrequest@cli.com to be added to the mailing list. The Nuprl Proof Development System is available by anonymous ftp from ftp://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  ftp://info.mcs.anl.gov/pub/Otter/Otter2.2/ anagram.mcs.anl.gov:/pub/Otter/ Contact: otter@mcs.anl.gov Resolutionbased theorem prover. RRL  ftp://herky.cs.uiowa.edu/public/ [128.255.28.100] Rewrite Rule Laboratory See SEQUEL entry in the Lisp FAQ, part 6. SETHEO  ftp://flop.informatik.tumuenchen.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.tumuenchen.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, ftp://coral.cs.jcu.edu.au/pub/research/tptplibrary/ [137.219.17.4] or the Institut fuer Informatik, TU Muenchen, Germany, ftp://flop.informatik.tumuenchen.de/pub/tptplibrary/ [131.159.8.35] as the files ReadMe (general information about the library), TPTPv1.1.0.tar.gz (the library itself), and TRv1.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/ http://wwwjessen.informatik.tumuenchen.de/~suttner/tptp.html Additions and corrections may be sent to Geoff Sutcliffe <geoff@cs.jcu.edu.au> (Fax: +6177814029) or Christian Suttner <suttner@informatik.tumuenchen.de> (Fax: +4989526502). 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 bugbps@ils.nwu.edu. User Contributions:Comment about this article, ask questions, or add new information about this topic:Top Document: Artificial Intelligence FAQ: Open Source AI Software 6/6 [Monthly posting] Previous Document: [612] Robotics Next Document: [614] Search Part1  Part2  Part3  Part4  Part5  Part6  Part7  Single Page [ Usenet FAQs  Web FAQs  Documents  RFC Index ] Send corrections/additions to the FAQ Maintainer: crabbe@usna.edu, adubey@coli.unisb.de
Last Update March 27 2014 @ 02:11 PM
