Research teams and centers : Europe - North America - Other

Publications
- Blogs - Organizations
- Online groups -
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 in 2008 : does not accept further submission but published papers remain available.
- Logic Journal of the IGPL (Interest Group in Pure and Applied Logics) - (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. - Chicago Journal of Theoretical Computer Science
- Discrete Mathematics & Theoretical Computer Science
- The Electronic Journal of Combinatorics
- 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.
- LMS Journal of Computation and Mathematics closed to new submissions in October 2015.

- 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 Logic and Algebraic Programming (formerly Journal of Logic Programming)
- 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.
- Theory and Practice of Logic Programming

- 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

- Jon Cohen's That Logic Blog - Logic in general, proof theory, philosophy.
- Richard Zach's
Logic and Philosophy Blog - Logic. Philosophy. Other Fun
Stuff. New address

- The Logic Blog Frontend by André Nies. Researchers from computability theory, algorithmic randomness, and related fields contribute to it.
- Computational complexity
- Todd Eisworth "Are you bored yet?" - old blog "Reading Shelah"
- A kind of library, by Andrés E. Caicedo
- Ali Sadegh Daghighi : The Kingdom of Logic
- 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
- Infinitesimals: Their Mathematics, Philosophy, History
- 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 Informal Logic & Critical Thinking
- Association for Logic in India
- Association for Logic Programming (ALP) (other url)
- 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 Science foundation has sponsored some research programs : AutoMathA (from May 2005 to May 2010) - Games for Design and Verification (March 2008 to March 2013)
- 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 (AILA - Associazione Italiana di Logica e sue Applicazioni)
- Italian Society for Logic and Philosophy of Science
- Kurt Gödel Society
- Polish Association for Logic and Philosophy of Science (in Polish : Polskie Towarzystwo Logiki i Filozofii Nauki)
- 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...
- Types project to develop the technology of formal reasoning and computer programming based on Type Theory (in EU′s 6th framework programme).
- European Society for Fuzzy Logic and Technology (EUSFLAT) - working group on Mathematical Fuzzy Logic
- 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.

Mailing lists:

- Abstract State Machines
- Categories, with also a big list of conferences on category theory - home pages of members
- PetriNets Mailing List with a list of other mailing lists.
- DMANET, an electronic news and research network for discrete mathematics and algorithms with about 1900 members worldwide.
- Foundations of Mathematics
- Gmane : mailing list archive (undergoing rebuild, 01/2017). There was a group "Frogs" (gmane.science.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

- Logical Aspects of Multi-Agent Systems was an international research network and now consists in annual workshops without a fixed site : 2015, 2016...
- Automated Deduction and its Application to Mathematics (ADAM) (most often in University of New Mexico)
- International Joint Conference on Automated Reasoning
- 12th International Workshop on the Implementation of Logics + 21st International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-21) in Maun, Botswana, May 2017.
- Conference on Automated Deduction
- List of organizations making logic-related conferences and workshops that have an overlap with logic in computer science, maintained by the LICS organization
- Workshop on Logic, Language, Information and Computation (WoLLIC)
- The First International ARCADE (Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements) Workshop will take place in association with The 26th International Conference on Automated Deduction (CADE-26) on the August 6, 2017.
- Fifth Workshop on Proof eXchange for Theorem Proving (23-24 September 2017, Brasilia, Brazil)
- Journées sur les
Arithmétiques Faibles (Weak Arithmetics Days)

- New York Logic
- Set Theory Talks : Global set theory seminar and conference announcements, with a list of speakers
- ACM/IEEE Symposium on Logic in Computer Science

- A list of software on the site of Toccata
- 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.
- Agda is a dependently typed functional programming language and a proof assistant
- 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.
- 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.
- G12 Constraint Programming Platform project at NICTA (Australia's ICT research centre): 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), 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.
- 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.
- 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)
- A list of resources by Ullrich Hustadt
- 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

Formal
Methods Education Resources Tool Pages

More resources in
the Formal Methods Wiki

Homotopy Type Theory

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? and many other papers in pdf by Solomon Feferman

University of Manchester there were "Mathematical Foundations Lecture Notes" at mfg.cs.manchester.ac.uk/notes.html ; now there are other lecture notes here and there and there and there

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, had mathematical logic courses at janwillemklop.nl/Jan_Willem_Klop/Courses_and_Notes.html, now offline

Dick van Leijenhorst

Richard Zach's papers

Open problems in logic

Mathoverflow : set theory

Hilbert’s
program then and now by Richard Zach

Hilbert's
Program Revisited by Panu Raatikainen (2003)

Formalized Mathematics by John Harrison

Proof Theory on Wikipedia

Samuel R. Buss : An Introduction to Proof Theory
- lecture
notes

Foundations
of logic programming and deduction
systems lecture notes

Encyclopedia articles:

- Set Theory - Article from Stanford Encyclopedia of Philosophy
- Hilbert's Program - Article from Stanford Encyclopedia of Philosophy
- Wikipedia articles : Foundations of Mathematics - Axiom - Axiomatic system
- Mathematical logic at New World Encyclopedia
- Foundations of mathematics article of Encyclopaedia Britannica

Beginnings of Set Theory

The Logic Cafe

History of Mathematics

There was a section Mathematical logic and foundations (http://www.math.niu.edu/Papers/Rusin/known-math/index/03-XX.html) in the Mathematical Atlas now offline

Foundations of Mathematics by Steve Simpson : publications, lecture notes and other course materials. Was the creator of the FOM mailing list.

Harvey's Foundational Adventures : downloadable lecture notes- downloadable manuscripts

Formal methods education resources

John Crossley 's "What is mathematical logic? A survey (PDF)" (including non-classical logics).

Russell's paradox : a short, a long and a very long article.

Burali-Forti Paradox : the ordinals do not form a set

Cantor's paradox : the cardinals do not form a set

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 had a free online logic course (videos with basic contents in long details), seems not working anymore

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

Roger Bishop Jones series of short paragraphs : Logic - Formal maths - Formal methods - philo of maths - foundations of maths - philosophy of logic

Some notes by Don Monk

Lecture notes in German by Prof. Dr. Peter Schroeder-Heister (old page)

Blogic : a Web logic textbook online interactive logic tutor

Karlis Podnieks presents an Hyper-textbook for students "What is Mathematics: Gödel's Theorem and Around" and an introduction to mathematical logic.

In French : La logique pour les nuls : pdf - html archive

Foundations of Artificial Intelligence lecture notes

Oliver Deiser (School of Education, Technische Universität München): books in German (there was a page "logic and sets at www.aleph1.info/logicandsets.html)

Lance Fortnow survey talks on complexity

Logic in Hebrew

- 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
- A list of logic and TCS related web-resources
- Model Theory
- Theoretical
Computer Science On The Web

- Herbert B. Enderton, who made a list of links to ASL members and wrote some books, died October 20, 2010
- MathGuide: Mathematical logic and foundations
- Set Theorists
- Archive of links on computability theory
- Computability Logic
- The Math Forum Internet library
- Set
theory links

- Statistical natural language processing and corpus-based computational linguistics: An annotated list of resources
- Philosophy links
- 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
- Steffen Lempp
- Formal Methods Education Resources
- The
Axiom of Choice

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

Other scientific pages and lists of links