Directory of links on logic and foundations of mathematics
Research teams and centers : Europe - North America - Other
Publications - Blogs - Organizations - Online groups - Software - Other
- 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) - previous issues
- 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.
- 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
- 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
- Teorema to publish original articles either in Spanish or in English in : Logic, Philosophy of Language, Philosophical Logic, Philosophy of Mind, Philosophy and History of Science, Epistemology and related areas.
- THEORIA is open to original and relevant papers from logic and philosophy of logic, history and philosophy of mathematics, history and philosophy of science, philosophy of technology, philosophy of language and philosophy of mind and cognition. Articles in English and Spanish are preferred, but the journal also accepts articles written in any of the languages of the Iberian Peninsula.
- The Review of Modern Logic (previously Modern Logic) ended in 2007.
General directories of mathematical publications
- 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
- Computability and Complexity in Analysis (CCA) 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
- Logic for INTeraction. LINT is a collaborative research project aimed at developing mathematical foundations for interaction. Gathers logicians, computer scientists and philosophers from six European countries
- 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.
Online groupsFoundations of Logic list of Facebook groups.
- The 15th Asian Logic Conference, July 10 - 14, 2017, Daejeon, Korea
- Logical Aspects of Multi-Agent Systems was an international research network and now consists in annual workshops without a fixed site : 2015, 2016...
- 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)
- Workshop on Computability Theory Series
- 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
- International Summer School for Proof Theory in First-Order Logic, August 22 - 27, 2017, Madeira, Portugal
- 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)
- 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.
- 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.
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
OtherNew Foundations (an axiomatic set theory with a universal set)
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.
Formal Methods Wiki
The Continuum Hypothesis is neither a definite mathematical problem nor a definite logical 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
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)
Formal Systems, proof theory
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
Introductions to logic and foundationsSet theory and the foundations of mathematics, in the present site.
Encyclopedia articles: Teach Yourself Logic 2017 A Study Guide
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
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