Research teams and centers : Europe - North America - Other

Publications
- Blogs
- Organizations
- Mailing
lists - Software
- Other

- Mathematics Arxiv Front: LO Logic - Front end for the logic section of the mathematics e-print arXiv. @ Los Alamos XXX Mathematics Archive
- Handbook of Set Theory
- Set Theory Preprint Sites (by author)
- Changes in "Set Theory Preprint Sites", an automated blog keeping track of changes in the preprint webpages of some people working in set theory.

- Bulletin of the EATCS (European Association for Theoretical Computer Science)
- Bulletin of Symbolic Logic - All articles in postscript format.
- Bulletin of the Section of Logic invites especially the contributions on topics dealing directly with logical calculi, their methodology, and algebraic interpretation.
- CLE e-Prints (Centre for Logic, Epistemology and the History of Science at UNICAMP)
- Electronic Colloquium on Computational Complexity
- Electronic Newsletter/News Journal on Reasoning about actions and change (ENRAC)
- Electronic Transactions on Artificial Intelligence (ETAI)
- Information and Computation (International journal of theoretical Computer Science published by Academic Press)
- International Journal of Mathematics and Computer Science
- Journal of Formalized Mathematics
- Journal of Functional and Logic Programming closed down in 2000 : does not accept further submission but published papers remain available.
- Journal of the IGPL (Interest Group in Pure and Applied Logics) with freely available articles in dvi and .ps formats. They forgot to specify the dates of publication but the last volume (4) seems to be from 1996.
- Logic Journal of the IGPL - (Oxford University Press) Official publication of the Interest Group in Pure and Applied Logic, since 1993.
- Logica Trianguli (6 numbers, 1997 - 2002)
- Nordic Journal of Philosophical Logic : archive (last number in December 2000)
- Pure Mathematics and Applications (Algebra and Theoretical Computer Science)
- Reports on Mathematical Logic Jagiellonian University Press, Krakow
- Theory and Applications of Categories (TAC)
- The
Reasoner

A monthly digest highlighting exciting new research on reasoning and interesting new arguments. It is interdisciplinary, covering research in, e.g., philosophy, logic, AI, statistics, cognitive science, law, psychology, mathematics and the sciences. - Australasian Journal of Logic - freely available electronic journal covering all areas of research in pure logic, and logic as it is applied in mathematics, computer science, linguistics and philosophy.

- Algebra and Logic
- Algebra Universalis (Springer)

- Annals of Mathematics and Artificial Intelligence
- Annals of Pure and Applied Logic (Elsevier - also at sciencedirect) - Formerly Annals of Mathematical Logic.
- Archive for Mathematical Logic (Springer - Editorial Manager) - Tables of contents from vol.34 (1995) on.
- Dissertationes Mathematicae
- Fundamenta Informaticae
- Fundamenta Mathematicae (Polish Academy of Sciences). Tables of contents from vol.33 (1945).
- Fuzzy Sets and Systems
- Information and Computation
- International Journal of Foundations of Computer Science
- Israel Journal of Mathematics
- Journal of Applied Logic
- Journal of Applied Non-Classical Logics
- Journal of Automated Reasoning -
Interdisciplinary Journal covering theory, implementation
and application. Online archive and full text for
subscribers.

- Journal of Logic and Computation
- Journal of Logic, Language and Information - Explores the foundations of natural, formal, and programming languages, as well as the different forms of human and mechanized inference. It covers the logical, linguistic, and information-theoretic parts of the cognitive sciences.
- Journal of Functional Programming
- Journal of Mathematical Logic - World Scientific. Contents and abstracts of all issues; full text to institutional subscribers.
- Journal of Multiple-Valued Logic and Soft Computing
- Journal of Symbolic Logic - Official
organ of the Association of Symbolic Logic. Also
electronically available to ASL members.

- Journal of the ACM (Association for Computing Machinery) (computer science) - hypertext bibliography
- Logica Universalis : editors - springer - springerlink)

- Mathematical Logic Quarterly - Formerly Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. Publisher's site. Table of contents from 2000. Full text to subscribers.
- Notre Dame Journal of Formal Logic Published by Duke University Press on behalf of the University of Notre Dame.
- The Review of Symbolic Logic
- Transactions on Computational Logic - Devoted to research concerned with all uses of logic in computer science.

- Analysis covers a wide range of topics including: philosophical logic and philosophy of language, metaphysics, epistemology, philosophy of mind, moral philosophy, and political philosophy.
- Argumentation - Argumentation Library
- Erkenntnis
- History and Philosophy of Logic
- Informal Logic
- Journal of Philosophical Logic - Journal devoted to philosophical applications of logic, and the philosophical underpinnings of logic. Sample copy and an archive of tables of contents.
- Journal of Semantics
- Linguistics and Philosophy
- Logical Analysis and History of Philosophy
- Logic and Logical Philosophy
- Logique et Analyse - Quarterly published by the National Centre for Logical Investigation
- Mathesis Universalis
- Philosophia Mathematica
- Smarandache Notions Journal : electronic and hard copy journal in many languages about Smarandache type functions, sequences, etc.
- Studia Logica
- The Review of Modern Logic (previously
*Modern Logic*) ended in 2007.

- Summa logicae : digital library, reference book for logic students and researchers, specially Spanish speakers involved in innovation and paedagogical systematization. Include software, a selection of links and a glossary.
- Shelah's papers
- Bibliography on Linear Logic
- The Collection of Computer Science Bibliographies
- DBLP Computer Science Bibliography
- CUNY Logic Bibliography

- Jon Cohen's That Logic Blog - Logic in general, proof theory, philosophy.
- Richard Zach's Logic and Philosophy Blog - Logic. Philosophy. Other Fun Stuff.
- Computational complexity
- A kind of library, by Andrés E. Caicedo
- The n-Category Café : a group blog on math, physics and philosophy
- Joel David Hamkins : mathematics and philosophy of the infinite
- Some mathematics of theoretical computer science
- Gödel’s Lost Letter and P=NP
- Theory Matters
- Jim Huggins (computer science and
other subjects)

- Academia Analitica is a learned society for the development of logic and analytic philosophy based in Bosnia and Herzegovina.
- Arché (official name: Arché - Philosophical Research Centre for Logic, Language, Metaphysics and Epistemology) is a research centre at the University of St Andrews, Scotland.
- Association
for Automated Reasoning

- Association for Computational Linguistics
- Association for Computing Machinery
- Association for Logic in India
- Association for Logic Programming
- Association for Symbolic Logic
- Belgian National Center of Research in Logic
- British Colloquium for Theoretical
Computer Science (BCTCS

- British Logic Colloquium
- Brazilian Logic Society
- COMPULOG Americas (after a European Compulog Net programme that no more exists) aims to serve as a forum where users, researchers and developers of logic programming systems and techniques can come together for common good.
- Computability in Europe (CiE) Network
- Computing Research Association (CRA)
- Consortium for Order in Algebra and Logic

- Deutsche Vereinigung für Mathematische Logik und für Grundlagenforschung der Exakten Wissenschaften (DVMLG)
- European
Association for Computer Science Logic

- European Association for Programming Languages and Systems (EAPLS)
- European Association for Theoretical Computer Science
- European Set Theory Society

- FoLLI - European Association for Logic, Language and Information. Includes : Interest Group in Pure and Applied Logics. Publications and preprints; holds an annual academic conference called the European Summer School in Logic, Language and Information (ESSLLI).
- FACS (Formal Aspects of Computing Science) Group of the British Computer Society
- Formal
Methods Europe

- IEEE Computer Society

- Interest Group in Pure and Applied Logics (IGPL)
- International
Federation for Computational Logic (IFCoLog)

- International Federation for Information Processing
- Italian Association of Logic and its applications
- Italian Society for Logic and Philosophy of Science
- The Japan Institute of Logic in Tokyo, is an educational institution dedicated to organize tests of logic in English for science and engineering students
- Kurt Gödel Society
- Logical Aspects of Multi-Agent Systems international research network
- Polish Association for Logic and Philosophy of Science
- Scandinavian Logic Society
- SIGACT (Special Interest Group on Algorithms and Computation Theory) is an international organization that fosters and promotes the discovery and dissemination of high quality research in theoretical computer science (TCS), the formal analysis of efficient computation and computational processes.
- Swiss Society for Logic and Philosophy of Sciences
- Texas Action Group interested in the study of formal and automated reasoning about the effects of actions using action languages and logic programming...
- European Research Consortium for Informatics and Mathematics
- ERCIM Working Group on Constraints Constraints have recently emerged as a research area that combines researchers from a number of fields, including Artificial Intelligence, Programming Languages, Symbolic Computing and Computational Logic. - Background, objectives, members and workshops.
- Young
Set Theory Network :New frontiers of infinity:
mathematical, philosophical, and computational prospects, a
Research Networking Programme of the European Science
Foundation. Aims to stimulate the exchange of ideas among
researchers pursuing different approaches to infinity.

- Abstract State Machines
- Categories, with also a big list of conferences on category theory - home pages of members
- Concurrency moderated email forum focusing on concurrent process theory, especially operational and abstract semantics, specification, and verification of: concurrent, distributed, reactive, real-time and hybrid systems.
- DMANET, an electronic news and research network for discrete mathematics and algorithms with about 1900 members worldwide.
- Foundations of Mathematics
- Frogs - Proof-theoretic discussion group, mainly focused on the calculus of structures
- Finite model theory mailing list
- Linguist list
- Moca mailing list on models for mobility and concurrency
- Proof Theory Mailing List - Mailing list devoted to proof theory, also accessible as a newsgroup. List of participants with their web sites, archive of messages.
- Proof Complexity mailing list
- Scottish
Theorem Proving

- Theory Net at North Dakota
- Types
- A list of mailing lists at the University
of Edinburgh

- List of organizations making logic-related conferences and workshops that have an overlap with logic in computer science, maintained by the LICS organization
- Mid-Atlantic Mathematical Logic Seminar
- New York
Logic

- Set Theory Talks : Global set theory seminar and conference announcements, with a list of speakers

- ACL2 - A programming language in which you can model computer systems and a tool to help prove properties of those models. Available under GPL and runs on various platforms. Includes related download links.
- Automath Archive
- A language designed by N.G. the Bruijn (1918-2012) in the
late sixties in order to represent mathematical proofs in
the computer.

- Abstract State Machines: Tools

- Bertrand - Bertrand solves sets of first-order predicate logic statements for satisfiability (consistency), validity, and equivalence. It also checks single statements for "logical truth" (tautology) and "logical falsity" (self-contradiction). Subject-identity is supported. User can "step through" the solution algorithm as Bertrand solves a problem, and/or check the graphic tree produced.
- bonsai - prooftrees in natural deduction

- Church - Program understands the different types of lambda expressions, can extract lists of variables (both free and bound) and subterms, and can simplify complicated expressions. Uses Python.
- Clean is a general purpose, state-of-the-art, pure and lazy functional programming language designed for making real-world applications.
- Coq is a formal proof management system. Typical applications include the formalization of programming languages semantics, the formalization of mathematics, and teaching.
- Computational Category Theory is a system encoding constructions in category theory, including finite limits and colimits, adjunctions and constructions of categories. It consists of a suite of functional programs written in Standard ML.
- CPP (aka G12): Constraint Programming Platform (NICTA project) - software platform for solving large-scale industrial combinatorial optimisation problems.
- DC Proof Online - Proof-writing software to teach the fundamentals of logic and proof. Enables users/students to write error-free proofs by selecting rules of inference, axioms, etc. from convenient drop-down menus. Includes tutorial and exercises.
- DARWIN, then E-Darwin - automated theorem prover
for first order clausal logic / Model Evolution Calculus
(Instance-based methods) (E- = with Equality)

- Database of Existing Mechanized Reasoning Systems - A list (over 50 entries) of automatic resolution provers (like Otter), interactive provers (like PVS) and other mechanized reasoning tools.
- DCTP - A Disconnection Calculus Theorem
Prover

- The E Theorem Prover for full first-order logic with equality.
- Formal Methods Applied to Electronic Voting Systems
- Gateway to Logic - A collection of web-based logic programs offering a number of logical functions: interactively or automatically build proofs, check theorems, and operate on propositional logic formulae.
- Geo is a prover for full-first order logic, writen in C++, is based on a new calculus called geometric resolution. The latest version is geo2007F
- HOL - environment for interactive theorem proving in a higher-order logic.
- The HR system performs automated theory
formation

- Interactive logic software, by Stanley N. Burris
- iProver - an instantiation-based theorem prover for first-order logic
- ileanTAP: An Intuitionistic Theorem Prover
- InVeSt: A Tool for the Verification of
Invariants

- Isabelle - A generic theorem proving
environment developed at Cambridge University (Larry
Paulson) and TU Munich (Tobias Nipkow). Includes logic,
documentation and free download. Isabelle mailing list. See also IsaPlanner

- j'Imp Theorem Prover - An automatic theorem prover based on set of support and ordered resolution for first-order logic. j'Imp is part of the Orbital library. This library is a Java class providing object-oriented representations and algorithms for logic, mathematics, and artificial intelligence.
- LambdaCLAM is a tool for automated theorem proving in higher order domains
- Lean, Tableau-based Deduction "written
in Prolog and implements a complete and sound theorem prover
for classical first-order logic based on free-variable
semantic tableaux... probably the smallest theorem prover
around."

- llprover - A linear logic prover that searches a cut-free proof for the given two-sided sequent of first-order linear logic.
- The Logics Workbench (LWB) is an application developed at the University of Berne in Switzerland. It offers the possibility to work in a user-friendly way in classical and non-classical propositional logics
- L4-Verified (NICTA project) : A Formally Correct Operating System Kernel
- LEGO Proof Assistant (last version November 1998) - LEGO Algebra Group
- The Logic
Machine, at Texas A&M University, hosts
interactive logic software used for teaching introductory
formal logic.

- LOOM - A language and environment for constructing intelligent applications. It is a research project in the Artificial Intelligence research group at the University of Southern California's Information Sciences Institute. The goal of the project is to develop and field advanced tools for knowledge representation and reasoning in Artificial Intelligence.
- LWB - Logics Workbench, application developed at the University of Berne in Switzerland, offers the possibility to work in a user-friendly way in classical and non-classical propositional logics, including nonmonotonic approaches
- Online tableau tool for the multi-agent epistemic logic MAEL
- Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program.
- Mizar consists of a formal language for writing mathematical definitions and proofs, a proof assistant which is able to mechanically check proofs written in this language, and a library of formalized mathematics which can be used in the proof of new theorems. The Mizar Mathematical Library is the largest coherent body of strictly formalized mathematics.
- ModLeanTAP: Lean Tableau-based Deduction
for Propositional Modal Logics

- MSPASS Theorem-prover, now incorporated into SPASS.
- MUltlog - Takes as input the specification of a finitely-valued first-order logic and produces a sequent calculus, a natural deduction system, and clause formation rules for this logic.
- MUltseq - A generic sequent prover for propositional finitely-valued logics.
- Omega
- (Proof Development with Ωmega) is the core of several
related and well integrated research projects of the Ωmega
research group.

- PVS - The PVS Specification and Verification System. Available for Sparc machines with Solaris 2 and Intel x86 Machines with Linux compatible with Redhat 5 or later. Required is Emacs (version 19 or later), recommended LaTeX and Tcl/Tk. Download by FTP.
- Proof General - Comprehensive Gnu-Emacs and XEmacs interface for several theorem provers including Coq, Isabelle, Lego, and Phox.
- ProofPower - A suite of tools supporting specification and proof in Higher Order Logic (HOL) and in Z notation.
- Propositional Satisfiability (SAT)
- Solver based on Clause Learning (Tinisat)
- Solvers based on Lookahead (Satz) or on Stochastic Local Search
- Prosper (Proof and Specification Assisted Design Environments) is a collaboration involving the Universities of Glasgow, Cambridge Edinburgh, Karlsruhe and Tübingen, IFAD, and Prover Technology. Developing an extensible, open proof tool architecture for incorporating formal verification into industrial CAD/CASE tool flows and design methodologies.
- Prover9 and Mace4 : Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.
- Quantomatic ; graph-based language for reasoning about quantum computation
- The SCAN tool is a tool for the elimination of second-order quantifiers; facilitates automated correspondence theory (mentioned on the Page of Positive Reviews of Research in Logical AI).
- SCOTT - Semantically Constrained Otter theorem prover (Model-Guided Proof Search)
- The TABSPASS theorem-prover (Hustadt and Schmidt 2000b, Hustadt and Schmidt 2002a) is a modified version of the first-order theorem prover SPASS which simulates derivations of tableaux-based decision procedures for basic modal logic.
- Setheo E-SETHEO is a strategy-parallel compositional theorem prover for first-order logic with equality.
- SPASS: An Automated Theorem Prover for First-Order Logic with Equality
- Tau theorem prover
- The Stanford Temporal Prover to support the computer-aided formal verification of reactive, real-time and hybrid systems based on their temporal specification.
- The Tableaux Workbench - a general framework for implementing tableau calculi
- TPS - Theorem Proving System, automated theorem-prover for first-order logic and type theory ; ETPS = Educational Theorem Proving System
- The TRP theorem-prover (Temporal Resolution Prover) (Hustadt and Schmidt 2001, Hustadt and Schmidt 2002b) is a prototypical implementation of a temporal resolution calculus for propositional linear-time logic.
- Tree Proof Generator - An implementation of the semantic tableaux method for classical propositional and predicate logic, written in JavaScript/DOM.
- VeriFun - A semi-automated system for the verification of statements about programs written in a functional programming language. The system is capable of following fully-automated routines for theorem proving and hypotheses formation, as well as operating interactively when these routines fail.
- Victor: A SPARK Verification Condition
Translator and Prover Driver

- Watson theorem prover

- WinKE - An interactive proof assistant based on analytic tableaux, and designed for the teaching of deductive reasoning. Ordering information is available at this site, as are academic papers on the design of the software.
- Vampire is a theorem prover by Andrei Voronkov that won the CASC world cup in theorem proving in 2009
- Yarralumla implements various transformations on clause logic formulas for the purpose of applying first-order bottom-up model generation (BUMG) systems.

- SRI International's Artificial Intelligence Center software list - Representation and Reasoning technologies

Theory Related Software

Wikipedia : Proof assistant (comparison table) - Automated theorem proving (with also a comparison table)

Some links to logic software

Educational Logic Software by the Committee of Logical Education of ASL

- New Foundations
- Transparent Intensional Logic (TIL) is a system for the logical analysis of natural language, applicable in philosophy as well as cumputational linguistic.
- International Olympiad in Mathematical Logic, a game for predicate logic (Java required).
- Formal Methods Wiki
- Is the Continuum Hypothesis a definite mathematical problem?
- Mathematical Foundations Lecture Notes
- Metamath Proof Explorer
- Gregory Chaitin, well known for his work on metamathematics and randomness in pure mathematics.
- The Alan Turing Home Page
- Jan Willem Klop, mathematical logic, courses and notes
- Dick van Leijenhorst

- Set theory
and the foundations of mathematics, in the present
site.

- Beginnings of Set Theory
- History of Mathematics
- Mathematical logic and foundations in the Mathematical Atlas
- Alexander Sakharov's online resource center for materials that relate to the Foundations of Mathematics
- Foundations of Mathematics by Steve Simpson
- Formal methods education resources
- Karlis Podnieks presents an Hyper-textbook for students "What is Mathematics: Gödel's Theorem and Around" and an introduction to mathematical logic.
- John Crossley 's "What is mathematical logic? A survey (PDF)"
(including non-classical logics)

- Stanley N. Burris : A Course in Universal Algebra - Logic for Mathematics and Computer Science.
- Some lecture notes by Onderwijspagina Jaap van Oosten
- Some basic lecture notes on mathematical logic and set theory
- Jouko Väänänen : " free online logic course. Anyone can login as a guest. After guest login, choose "Logic One" on the right of the screen." (videos with basic contents in long details)
- Understanding Mathematics by Peter Alfeld at the University of Utah
- Some notes on set theory
- A high level course on logic and set theory
- Fundamentals of Model Theory, a book
by William Weiss and Cherie D’Mello, University of Toronto

- In French : La logique pour les nuls
- Foundations of Artificial Intelligence lecture notes
- Oliver Deiser (School of Education, Technische Universität München): logic and sets - books in German
- Lance
Fortnow survey talks on complexity

- Logic systems list (started as a list of Modal Logic systems)
- A big directory with thousands of links on logic and foundations, by subject, especially articles - Some links are serious but much are rubbish, commercial or outdated. Probably no better than search results pages.
- Fuzzy sets and systems

- Set Theorists
- Recursion / Computability Theorists and other links
- Computability Logic
- The Math Forum Internet library
- Set theory links

- Statistical natural language processing and corpus-based computational linguistics: An annotated list of resources
- The Compendium of NP Optimization Problems
- Some links by Denis Roegel
- Some links and names of researchers in computability
- Ressource lists of the Gateway to Logic
- Computability Theory
- The Axiom of Choice

(These links were moved to a separate page)

Created by Sylvain Poirier, author of settheory.net, in July 2012 (with updated links while the main sources used (world.logic.at, and Anton Setzer), were all quite incomplete and obsolete, thus visibly no more maintained).

Still incomplete, more links will be added later.