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. New address

- 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 (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 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
- Logical Aspects of Multi-Agent Systems international research network
- 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 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.
- New frontiers of infinity
(Research Networking Programme of the European Science Foundation):
mathematical, philosophical, and computational prospects, . 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

- International Joint Conference on Automated Reasoning
- List of organizations making logic-related conferences and workshops that have an overlap with logic in computer science, maintained by the LICS organization
- 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

- 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.
- 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.
- G12 Constraint Programming Platform project at NICTA (Australia's Information Communications Technology Research Centre of Excellence): 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)
- 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 (or ps.gz) by Solomon Feferman

Mathematical Foundations Lecture Notes at the University of Manchester

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

Richard Zach's papers

Open problems in logic

Mathoverflow : set theory

Hilbert’s
program then and now by Richard Zach

Hilbert's Program - Article from Stanford Encyclopedia of Philosophy

Hilbert's
Program Revisited by Panu Raatikainen (2003)

Formalized Mathematics by John Harrison

Formal
Languages and Systems by Heinrich Herre and Peter
Schroeder-Heister

Proof Theory on Wikipedia

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

Foundations
of logic programming and deduction
systems lecture notes

Teach Yourself Logic 2016 A Study Guide

Beginnings of Set Theory

Set Theory - Article from Stanford Encyclopedia of Philosophy

History of Mathematics

Mathematical logic and foundations in the Mathematical Atlas

Foundations of mathematics article of Encyclopaedia Britannica

Wikipedia articles : Foundations of Mathematics - Axiom - Axiomatic system

Foundations of Mathematics by Steve Simpson : publications, lecture notes and other course materials. Historical note :

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 : " 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

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

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): logic and sets - books in German

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

- 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

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