List of Research Groups in Logic and Theoretical Computer Science World-wide

Software, Theorem Provers

General Sites

• Mechanized Reasoning (Stanford)
• ORA Bibliography of Automated Deduction
• Automated Induction (by David McAllester)
• Automated Deduction (by Tomás Uribe)
• Logical Frameworks
• Formal Methods Library (Oxford)

LaTeX, TeX

• Latex for Logicians

Theorem Provers

• Agda
  • Archive of the Agda email list
  • Official website of Agda
  • Agda2
  • Agda Wiki
  • Documentation about Agda by Catarina Coquand (refers to old Agda
• Alf
  • Overview over Alf with literature
• Tutch theorem prover From Munich (Abel). Suitable for teaching. Uses notation similar to imperative programming languages (begin - end).
• Proof General (Generic emacs interface for interactive proof assistants)
• Twelf
• TPS (Theorem proving software; with ETPS, teaching software for TPS)
• TPTP
• QED
• PVS (based on Church's theory of types)
• Metamath Solitaire (Theorem proofer as a Java Applet, ZFC and other logics)
• Automated Reasoning Project, Australian National University
• The Logics Workbench (LWB) from Bern, Switzerland
• Logic Software from St. Andrews
  • Mac Logic
  • Other Theorem provers for intuitionistic logic and Dummett logic
• Minlog
• Alf
• Alfa
• REDLOG (predicate logic, quantor elimination decidability procedures for theories of fields)
• Web page drawing type assignment figures (by Sachio Hirokawa)
• The HOL Theorem Proving System
• Isabelle (Some informations from Munich)
• IMPS
• Cornell Nuprl Automated Reasoning Project
• Logical Frameworks
• COQ documentation
• The LEGO Proof Assistant
  • LEGO Literature
• Logic Software from CSLI (by Jon Barwise and John Etchemendy)
  • Hyperproof
  • The Language of First-order Logic,
  • Tarski's World
  • Turing's World
• ftp-Server in Chalmers, for getting ALF
• Porgi - Proof-Or-Refutation Generator for Intuitionistic propositional logic
• Lambda, a program for solving lambda definability problems of order at most two

Functional Programming Languages

• Clean
• Cayenne
• Haskell

Teaching Software

• Logic Software from CSLI (by Jon Barwise and John Etchemendy)
  • Hyperproof
  • The Language of First-order Logic,
  • Tarski's World
  • Turing's World
• ARACNE Project
  • Tools for Teaching

Other Symbolic Computations

• Maple

FTP-servers and other sites

• ftp-Server in Chalmers, for getting ALF
• Ftp-Server on the Lics-Server
  • The LICS anonymous ftp area is research.bell-labs.com, directory /dist/lics.
    It contains, among others, recent announcements, in various formats
    (e.g. LaTeX, postscript, plain text).
• TU-ftp server
• Server in Erlangen
• Server in Mainz
• Software in Mathematics, (European Mathematical Society)

Programming Languages

• CHARITY - a categorical programming language
• Visual Prolog

• back to table of contents for Logic Servers Worldwide
• back to Theoretical Computer Science at Swansea
• back to Computer Science at Swansea

Please mail additions and corrections to Anton Setzer , .

---

Dept. of Computer Science, University of Wales Swansea | Last modified: Oct 12, 1999 | URL http://www-compsci.swan.ac.uk/~csetzer/logic-server/software.html | Anton Setzer,

• University of Wales Swansea
  • Department of Computer Science
    • Theoretical Computer Science