Directory of links on logic and set theory
teams and centers : Europe - North America
- Blogs - Organizations
lists - Software
of the EATCS (European Association for Theoretical
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
- Electronic Colloquium
on Computational Complexity
Newsletter/News Journal on Reasoning about actions and change
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
of Functional and Logic Programming closed down in 2000 :
does not accept further submission but published papers remain
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
- Logic Journal of
the IGPL - (Oxford University Press) Official publication
of the Interest Group in Pure and Applied Logic, since 1993.
Trianguli (6 numbers, 1997 - 2002)
Journal of Philosophical Logic : archive (last number in
Mathematics and Applications (Algebra and Theoretical Computer
- 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.
General directories of mathematical publications
Analitica is a learned society for the development of
logic and analytic philosophy based in Bosnia and Herzegovina.
(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
- Association for Computational
- Association for Computing
- Association for Logic in India
for Logic Programming (ALP) (other url)
- Association for Symbolic
- Belgian National Center
of Research in Logic
Colloquium for Theoretical Computer Science (BCTCS)
- British Logic
- Brazilian Logic
- 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.
in Europe (CiE) Network
- Computing Research Association (CRA)
for Order in Algebra and Logic
Vereinigung für Mathematische Logik und für
Grundlagenforschung der Exakten Wissenschaften (DVMLG)
- European Association for
Computer Science Logic
Association for Programming Languages and Systems (EAPLS)
- European Association for
Theoretical Computer Science
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
- Interest Group in
Pure and Applied Logics (IGPL)
- International Federation for
Computational Logic (IFCoLog)
Federation for Information Processing
- Italian Association
of Logic and its applications
- Italian Society for
Logic and Philosophy of Science
- Kurt Gödel Society
- Logical Aspects of Multi-Agent
Systems international research network
Association for Logic and Philosophy of Science
- Scandinavian Logic
- 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...
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
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.
- Categories, with
also a big list of conferences on category theory - home
pages of members
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.
an electronic news and research network for discrete mathematics
and algorithms with about 1900 members worldwide.
- Proof-theoretic discussion group, mainly focused on the
calculus of structures
model theory mailing list
- Linguist list
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.
Complexity mailing list
- Scottish Theorem
Net at North Dakota
list of mailing lists at the University of Edinburgh
- A list of software on the site of Toccata
- 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
- 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
State Machines: Tools
- 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
- 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
- Coq is a formal proof
management system. Typical applications include the
formalization of programming languages semantics, the
formalization of mathematics, and teaching.
Category Theory is a system encoding constructions in
category theory, including finite limits and colimits,
adjunctions and constructions of categories. It consists of a
suite of functional programs written in Standard ML.
CPP (aka G12): Constraint Programming Platform (NICTA project)
- software platform for solving large-scale industrial
combinatorial optimisation problems.
- DC Proof Online -
Proof-writing software to teach the fundamentals of logic and
proof. Enables users/students to write error-free proofs by
selecting rules of inference, axioms, etc. from convenient
drop-down menus. Includes tutorial and exercises.
- automated theorem prover for first order clausal logic / Model
Evolution Calculus (Instance-based methods) (E- = with Equality)
of Existing Mechanized Reasoning Systems - A list (over 50
entries) of automatic resolution provers (like Otter),
interactive provers (like PVS) and other mechanized reasoning
- A Disconnection Calculus Theorem Prover
E Theorem Prover for full first-order logic with equality.
Methods Applied to Electronic Voting Systems
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.
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
- The HR system
performs automated theory formation
logic software, by Stanley N. Burris
- an instantiation-based theorem prover for first-order logic
- ileanTAP: An
Intuitionistic Theorem Prover
A Tool for the Verification of Invariants
- 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.
is a tool for automated theorem proving in higher order domains
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."
- 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
(NICTA project) : A Formally Correct Operating System
- LEGO Proof
Assistant (last version November 1998) - LEGO Algebra
- The Logic Machine, at
Texas A&M University, hosts interactive logic software used
for teaching introductory formal logic.
- 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.
Lean Tableau-based Deduction for Propositional Modal Logics
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.
- (Proof Development with Ωmega) is the core of several related
and well integrated research projects of the Ωmega research
- 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.
- 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.
; 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).
- Semantically Constrained Otter theorem prover (Model-Guided
- The TABSPASS
and Schmidt 2000b, Hustadt
and Schmidt 2002a) is a modified version of the
first-order theorem prover SPASS which simulates derivations of
tableaux-based decision procedures for basic modal logic.
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
- The Stanford Temporal
Prover to support the computer-aided formal verification
of reactive, real-time and hybrid systems based on their
- 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
- 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
- Tree Proof Generator
- An implementation of the semantic tableaux method for
classical propositional and predicate logic, written in
- 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.
A SPARK Verification Condition Translator and Prover Driver
- 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
implements various transformations on clause logic formulas for
the purpose of applying first-order bottom-up model generation
Announcement for web programmers that may be available for
a new project : I have defined
this project (and had a few programmers some time ago, who
did something and then stopped), and could usually convice people
interested in economics to whom I had the opportunity to explain its purposes for
at least 1 hour, that this is the right project to change the
world. But I did not have such an opportunity with web
programmers, that are usually too busy to pay any significant
attention, and/or don't want to understand anything else than
lines of code − as, contrary to what most people want to
believe, the originality and specificity of these new concepts
cannot be understood in 2 minutes by referring to what already
exists with similar purposes. So if you can do web programming and
be interested to make a meaningful work on an economic and
political level, you can be interested with my project. Just
contact me after having a look there to ask for further
explanations, thanks !
Proof assistant (comparison table) - Automated
theorem proving (with also a comparison table)
links to logic software
Logic Software by the Committee of Logical Education of ASL
Introductions to logic and foundations
(These links were moved to a separate page)
Created by Sylvain Poirier, author of settheory.net, in July 2012 (with
updated links while the main sources used (world.logic.at, and Anton
Setzer), were all quite incomplete and obsolete, thus visibly
no more maintained).
Still incomplete, more links will be added later.