RESEARCH SITES:

This collection of papers and FTP sites is focused mostly on Automated Deduction and related matters. This page is rather informal and haphazard, please send suggestions/updates/corrections to uribe@CS.Stanford.EDU.

For a more organized page on deduction, see the Mechanized deduction worldwide page maintained by Michael Kohlhase and Carolyn Talcott.

Indexes to other areas:

  • Programming Languages index at CMU.
  • The home page for Formal Methods and the one for Logic Programming at Oxford University.
  • The CMU page on Logical Frameworks.
  • The home page for research in Unification theory.
    • The TIELT Testbed for Integrating and Evaluating Learning Techniques at NRL.

    Australia:

  • The Australian National University Automated Reasoning Project; the ftp site includes subdirectories for John Slaney's FINDER and various papers (including Finite Algebra papers). The James Cook University is the home of the TPTP library (there's a mirror copy at TU Muenchen), and some QED and Mizar-related items.

    • Denmark:

  • BRICS (Basic Research in Computer Science) publications at the University of Aarhus.

    • France:

  • Here is the University of Nancy ftp site.
  • The INRIA home page is here, including the COQ project.
  • Here's Projet Cristal at Inria.
  • The LORIA home page.
  • The ORME rewriting lab ftp site.
  • The REVEAL prover ftp site at Orleans. Here one can also find the STORM matching system.
  • At Bordeaux one finds Anigraf, and "interactive system for the animation of graph relabeling systems with priorities."

    • Germany:

  • Here are the papers from the Max Plank Institut for Informatik in Germany. Here's the ftp site.
  • At Munich, there's the Web page for the European Community Research Center (ECRC) and the ECLiPSe CLP system.
  • The Karlsruhe Interactive Verifier (KIV) at Karlsruhe.
  • The home page for the Hardware Verification Group at Karlsruhe is here, and here's an ftp site.
  • There's also the page for The First Intl. Conference on Constraints in Computational Logics (Sept. 1994).
  • A general page for Automated Deduction in Germany, at Saarbrucken.
  • Saarbruecken DFKI is here (and the FTP site including Jorg Siekmann's unification survey).
  • Papers from Franz Weber about higher-order unification, in this directory.
  • The ReDuX rewrite system available via FTP.
  • The Technical University of Munich, where the "High Performance Theorem Prover" SETHEO, the TPTP library and the prover Isabelle can also be found.
  • The leanTAP theorem prover (360 bytes long) at Karlsruhe.
  • The Artificial Intelligence Group at the University of Koblenz, including the PROTEIN theorem prover.

    • Italy:

  • The FTP site for the Mechanized Reasoning Group at Trento.

    • Japan:

  • Here are the ICOT archives, which are mirrored at this ftp site at SICS.
  • Hitachi's Advanced Research Laboratory.

    • Spain:

  • The SATURATE theorem-prover from Barcelona and MPI (Germany), written in Prolog.

    • Sweden:

  • The Swedish Institute for Computer Science (SICS) and their ftp site.
  • The Noether system and a paper on parallel unification algorithms.

    • United Kingdom:

  • Here's a WEB index for comp.constraints and other constraint-related matters.
  • The FTP site for the Department of AI at Endinburgh is here. Also, this is the ftp site for Alan Bundy's DREAM group (here are the abstracts).
  • The WWW home page for the Imperial College theory division.
  • The Glasgow University Dept. of CS web server. The Equational Reasoning system Merrill is available via FTP there.
  • At Cambridge University one can find the Isabelle theorem prover in the ML ftp subdirectory.
  • The HOL system information page at Cambridge (here's the University of Cambridge Computer Laboratory FTP site; and an HOL prover documentation page at Brigham Young.

    • United States

    Various:

  • Papers from the ESPRIT project on Construction of Computational Logics (CCL) of the European Community.
  • Extended abstracts for the 1994 Workshop on Conditional Term Rewriting Systems (ftp site).
  • The Constraint Programming archive at Aarhus.

    • The Stanford home page.

    The Computer Science Department home page.

    The Theory Division home page.

    Tomás E. Uribe

    uribe@CS.Stanford.EDU