Directory of links on logic and foundations of
mathematics
Research
teams and centers : Europe - North America
- Other
Publications
- Blogs - Organizations
- Online groups -
Software
- Other
Publications
Preprints
Online Journals
- 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 (Oxford University Press, 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.
Ordinary journals
Philosophy journals
- 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 ended activity (last issue : January 2004).
- 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
Bibliographies
Activities
Blogs
Organizations
- 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.
- Association Computability
in Europe (CiE)
- Computability and Complexity in Analysis (CCA) Network
- Computing Research Association (CRA)
- Consortium
for Order in Algebra and Logic (no more online ?)
- 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 (IGPL). 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
- International Federation for
Computational Logic (IFCoLog): website no more working, seems organization no more exists http://www.ifcolog.net/
- 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.
Foundations of Logic list of Facebook groups.
Mailing lists:
Conferences
- 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
Software
- 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
- BEAGLE
- 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
- An Interactive Mathematical
Proof System (IMPS)
- 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.
-
MINLOG
interactive proof system
- 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
is a fully automatic theorem prover for proving the unsatisfiability of formulae in first-order clause logic
(another page disappeared: 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.
(an old list)
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
Other
New
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
Hilbert’s
program then and now by Richard Zach
Partial
Realizations of Hilbert's Program (1988) by Steve Simpson
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 foundations
Set theory and the foundations of
mathematics, in the present site.
Encyclopedia articles:
Open Logic Project
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 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
More portals
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