---
Science - Math - Logic and Foundations
---

Click here!

Goldstern, Martin - University of Technology, Vienna - Set theory.

Grossberg, Rami - Carnegie Mellon University - Model theory.

Herwig, Bernhard - University of Freiburg - Model theory.

Hjorth, Greg - UCLA - Descriptive set theory, countable models, definable equivalence relations.

Hodges, Wilfrid - University of London - Model theory.

Holmes, Randall - Boise State University - Set theory: New Foundations, automated theorem proving.

Howard, Paul - Eastern Michigan University - Axiom of choice.

Hustadt, Ullrich - University of Liverpool - Resolution-based and tableaux-based decision procedures for decidable fragments of first-order logic.

Hyland, J. Martin E. - University of Cambridge - Categorical logic, game semantics and logic in computer science.

Jech, Thomas - Pennsylvania State University - Set theory.

Jockusch, Carl G. - University of Illinois, Urbana Champaign - Recursion theory.

Junker, Markus - University of Freiburg - Model theory.

Kaiser, Klaus - University of Houston - Mathematical logic, universal algebra, lattice theory and logic programming.

Kanamori, Akihiro - Boston University - Set theory.

Kaye, Richard - University of Birmingham - Model theory.

Kechris, Alexander S. - Caltech - Foundations of mathematics, mathematical logic and set theory, interactions with analysis.

Kunen, Kenneth - University of Wisconsin, Madison - Set theory.

Lafont, Yves - University of Marseille II - Linear logic, lambda calculus, proof theory, term rewriting. Lafont invented the theory of interaction nets, an elegant theory of graph rewriting.

Larson, Jean A. - University of Florida - Set theory, combinatorics.

Lascar, Daniel - CNRS / University of Paris 7 - Model theory.

Lempp, Steffen - University of Wisconsin, Madison - Computability, recursion theory.

Lessmann, Olivier - University of Illinois, Chicago - Model theory.

Luo, Zhaohui - Durham University, UK - Type theory, theoretical computer science and semantics of natural languages.

Makowsky, Johann (Janos) A. - Technion, Israel - Logic in computer science, finite model theory.

Marcos, João - State University of Campinas, Brazil - Interested in both mathematical and philosophical logic, and especially non-classical logics such as paraconsistent, many-valued and modal logics, as well as formal semantics to them, and combinations of logics.

Marker, David - University of Illinois, Chicago - Model theory.

Matiyasevich, Yuri - Steklov Institute, St. Petersburg - Algorithmical number theory.

McKenzie, Ralph - Vanderbildt University and UC Berkeley - Algebra, logic, combinatorics.

Miller, Dale - Penn State University - Linear logic, proof search and declarative programming languages.

Mitchell, William - University of Florida - Set theory.

Monk, Donald - University of Colorado, Boulder - Boolean algebras.

Moreno, Javier - University of Illinois, Urbana-Champaign - Model theory and applications.

Moschovakis, Yiannis N. - UCLA - Set theory, recursion theory.

Nelson, Edward - Princeton University - Bounded arithmetic, automated proof verification (QED).

Nerode, Anil - Cornell University - Computability theory, logic in computer science, history of logic.

Nies, Andre - University of Chicago - Recursion theory.

Ong, C.-H. Luke - Merton College, Oxford - Categorical logic, game semantics, type theory, lambda calculus, semantics of programming languages, and sequentiality.

Paris, Jeff - University of Manchester - Mathematical Logic, in particular uncertain reasoning.

Pedicini, Marco - Institute for Applied Calculus, Rome - Theoretical computer science, linear logic, geometry of interaction, optimal reductions.

Pfenning, Frank - Carnegie Mellon University - Logic and programming languages, logical frameworks, type theory.

Pitts, Andrew - University of Cambridge - Categorical logic, type theory, semantics of programming languages and logic in computer science.

Portier, Natacha - ENS Lyon.

Pratt, Vaughan - Stanford University - Linear logic, Chu spaces, foundations of mathematics, theoretical computer science and wearable computing.

Prest, Mike - University of Manchester - Algebra and model theory.

Pym, David J. - Queen Mary and Westfield College - Semantics of programming languages, type theory, proof-search, logic programming, theorem proving.

Quigley, Peter - Manchester Metropolitan University - Computational logic, formal methods, formal specification, automated reasoning and proof planning.

Rathjen, Michael - University of Leeds - Proof theory.

Regnier, Laurent - University of Marseilles - Linear logic, lambda calculus and abstract machine interpretations.

Restall, Greg - Macquarie University - Philosophy of logic, substructural logics.

Robinson, Edmund - Queen Mary and Westfield College - Categorical logic and the semantics of programming languages and type theories.

Rubin, Jean E. - Purdue University - Set theory, axiom of choice.

Scedrov, Andre - University of Pennsylvania - Logic in computer science, linear logic.

Schmidt, Renate - University of Manchester - Modal logic, resolution theorem proving, resolution decision problems, relation algebras, Peirce algebras and knowledge representation.

Scott, Dana - Carnegie Mellon University - Model theory, set theory, foundations of logic and mathematics, symbolic mathematical computation.

Vlad, Serban E. - Independent scholar, Bucharest - Asynchronous automata and binary valued mathematical analysis.

Setzer, Anton - Uppsala University - proof theory (ordinal analysis), Martin-Löf type theory.

Shelah, Saharon - Rutgers University and Hebrew University - includes paper archive.

Shore, Richard A. - Cornell University - Recursion theory.

Shramko, Yaroslav - State Pedagogical University, Kryvyi Rih, Ukraine - Intuitionistic and relevant logics.

Sieg, Wilfried - Carnegie Mellon University - Proof theory, philosophy of mathematics, history of 19th and 20th century logic and mathematics.

Sipser, Michael - MIT - Complexity theory.

Slaman, Theodore A. - University of California, Berkeley - Recursion theory.

Soare, Robert I. - University of Chicago - Recursion theory.

Solovay, Robert M. - University of California, Berkeley.

Statman, Richard - Carnegie Mellon University - Theory of computation, lambda calculus, combinatory logic.

Stewart, Charles - Technische Universität Berlin, Theory and Formal Specifications group - Proof theoretic semantics, lambda calculus, linear logic, theoretical computer science, philosophy of language.

Taylor, Paul - Queen Mary and Westfield College, London - Foundations of Mathematics and Computation.

Thiel, Christian - University of Erlangen-Nürnberg - History of logic.

Vermeir, Timothy - University of Ghent, Belgium, Centre for Logic and Philosophy of Science - nonmonotonic, adaptive, nonclassical, paraconsistent logics and logic programming.

Vickers, Steven - Imperial College, London - Geometric logic, topos theory, quantales and semantics of programming languages.

Wansing, Heinrich - Institute of Logic and the Philosophy of Science, Leipzig - Substructural and non-classical logics, modal logic, proof-theoretic semantics, philosophy of logic, philosophy of language.

Welch, Philip - University of Bristol - Set theory, inner models, descriptive set theory.

White, Graham - Queen Mary and Westfield College, London - Philosophy and linear logic.

Wilkie, Alex - Oxford University - Models of arithmetic.

Wilmers, George - University of Manchester - Applications of mathematical logic in the foundations of uncertain reasoning; natural prior probability distributions in uncertain reasoning.

Zach, Richard - University of Calgary - Non-classical logics, proof theory, philosophy of mathematics, history and philosophy of logic.

Ziegler, Martin - University of Freiburg - Model theory.

Zilber, Boris - University of Oxford - Model theory.

Hindley, J. R. - University of Wales, Swansea - Lambda-calculus, combinatory logic and type-theory.

Friedman, Harvey - Ohio State University.

Hähnle, Reiner - Chalmers University of Technology, Sweden - Tableau-based automated theorem proving, many-valued logic, formal verification.

Chatzidakis, Zoé - CNRS/University of Paris 7 - Model theory.

Darnière, Luck - University of Angers, France - Model theory.

Simpson, George - Fuondations of Mathematics and Logic.

Cholak, Peter - University of Notre Dame - Recursion theory.

Knight, Julia F. - University of Notre Dame - Recursion theory.

Peckhaus, Volker - University of Erlangen-Nürnberg - History of logic.

Pym, David - University of Bath, England - Proof theory, logic and computation.

Research groups in Logic and Theoretical Computer Science - Maintained by Anton Setzer, Uppsala.

Mathematical Logic around the world - A service provided by the Mathematical Logic Group in Bonn

Logic Programming - Section of WWW Virtual Library.

Logic and Set Theory - Groups and conferences.

Computability Theory - Information on this site includes a Bibliographic Database for Computability Theory, a list of Open Questions in Recursion Theory as well as links to many researchers working in the field. Maintained by Peter Cholak.

Description Logics - Maintained by Carsten Lutz.

Logic and Set Theory - Category of Topics in Mathematics (MathArchives).

Logic Page - Maintained by Christian Gottschall, Vienna philosophy department.

Stanford Encyclopedia of Logic Technology - A compendium of information including theoretical material, an index to currently available technology, and a survey of applications.

Logic Links - Gustavus Philosophy Department.

ASL members - List of web pages of Association for Symbolic Logic members. Maintained by Herbert Enderton.

Formal Logic - Directory of encyclopedia articles and related websites. [epistemelinks.com]

Logic on the World Wide Web - Based on the compilation of Boris Piwinger (Mathematical Logic Group at the University of Bonn).

Australian Logic Home Page - Lists institutions, research groups and individuals; updated 1996.

Knowledge Representation - With Automated Reasoning, Computational Logics and Advanced Databases. Projects, people, conferences and specific resources.

Mathematical Logic and Foundations - Section of Math Guide.

Model Theory and Applications to Algebra and Analysis - Research session at the Isaac Newton Institute for Mathematical Sciences, Cambridge, UK; 17 January -- 15 July 2005.

Set Theory and Analysis - Semester long program at the Fields Institute, Toronto, Ontario, along with some shorter workshops. September through December, 2002.

Logic and Mathematics: Connections and Interactions - Conference on applications of logic in mathematics; Urbana-Champaign, Illinois, May 21-25, 2003.

World Congress on Paraconsistency - The WCP3 will take place in Toulouse (France) from 28-31 July 2003, and will focus on mathematics, philosophy and applications of paraconsistent logics.

ISMVL 2003 - Tokyo, Japan, May 16-19, 2003.

ISMVL 2002 - Boston, Massachusetts, May 15-18, 2002.

ISMVL 2001 - Warsaw, Poland, May 22-24, 2001.

ISMVL 2000 - Portland, Oregon, May 23--25, 2000.

WoLLIC - Vision - A series of workshops which started in 1994 with the aim of fostering interdisciplinary research in pure and applied logic. Proceedings, reports and comments on the series.

WoLLIC '97 - 4th Workshop on Logic, Language, Information and Computation. Fortaleza, (Ceará), Brazil; 19/20--22 August 1997. Abstracts.

WoLLIC'2000 - 7th Workshop on Logic, Language, Information and Computation. Hotel Barreira Roxa, Natal, Brazil; 15--18 August 2000. Proceedings in PostScript.

WoLLIC'2001 - 8th Workshop on Logic, Language, Information and Computation. Brasília, Brazil; 31 July -- 3 August 2001. Abstracts.

WoLLIC'2002 - 9th Workshop on Logic, Language, Information and Computation. Rio de Janeiro, Brazil; 30 July -- 2 August 2002.

WoLLIC '99 - 6th Workshop on Logic, Language, Information and Computation. Hotel Simon, Itatiaia National Park, Rio de Janeiro, Brazil; 25--28 May 1999. Abstracts.

Logic Colloquium '96 - European Summer Meeting of the Association for Symbolic Logic. San Sebastián, Spain; 9--15 July 1996.

Logic Colloquium '95 - Haifa, Israel; 9--17 August 1995.

Logic Colloquium '99 - Utrecht, The Netherlands; 1--6 August 1999. Photographs.

Logic Colloquium '97 - Leeds, UK; 6--13 July 1997.

Logic Colloquium '98 - Prague, Czech Republic; 9--15 August 1998.

Logic Colloquium 2000 - Incorporating the European Logic Summer School 2000 (ELSS 2000). Paris, France; 23--31 July 2000.

Logic Colloquium 2002 - (ASL European Summer Meeting) Münster, Germany; 3--10 August 2002.

Logic Colloquium 2001 - Vienna University of Technology, Vienna, Austria; 6--11 August 2001.

ESSLLI'98 - 10th European Summer School in Logic, Language and Information. Saarbrücken, Germany; 17--28 August 1998.

ESSLLI 2001 - 13th European Summer School in Logic, Language and Information. On-line registration. University of Helsinki, Finland; 13--24 August, 2001.

ESSLLI'99 - 11th European Summer School in Logic, Language and Information. Utrecht University, the Netherlands; 9--20 August 1999.

ESSLLI 2001 Student Session - The sixth ESSLLI Student Session.

ESSLLI 2000 - 12th European Summer School in Logic, Language and Information. Birmingham, UK; 6--18 August 2000.

ESSLLI'97 - 9th European Summer School in Logic, Language and Information. Aix-en-Provence, France; 11--22 August 1997.

ESSLI 2002 - 14th European Summer School in Logic, Language and Information. Trento, Italy; 5--16 August 2002.

European Summer School in Logic, Language and Information - Under the auspices of FoLLI (The European Association for Logic, Language and Information). List of previous and forthcoming meetings.

Amsterdam Colloquium 1999 - The Twelfth Amsterdam Colloquium, bringing together logicians, philosophers, linguists and computer scientists who share an interest in the formal semantic study of natural and formal languages. University of Amsterdam, the Netherlands; 18--21 December 1999.

ICLP'99 - Sixteenth International Conference on Logic Programming. Las Cruces, New Mexico; 29 November -- 4 December, 1999.

CSL 2000 - Computer Science Logic. Fischbachau/Munich, Germany; 21--26 August 2000.

CATS 2000 - Computing: The Australasian Theory Symposium. Australian National University, Canberra; 1 -- 2 February 2000.

DEON'98 - Fourth International Workshop on Deontic Logic in Computer Science. Bologna, Italy; 8--10 January 1998.

The Future of the Turing Test - Dartmouth College, USA; 28--30 January 2000. Loebner Competition results.

FroCoS 2000 - 3rd International Workshop on Frontiers of Combining Systems. Combining logics and deduction systems and logical modelling of multi-agent systems. Nancy, France; 22--24 March 2000.

SPbDLC'99 - First St.Petersburg Days of Logic and Computability. St. Petersburg, Russia; 26--29 May 1999. Abstracts, photos.

FroCoS'96 - First International Workshop on Frontiers of Combining Systems. Munich, Germany; 26--29 March 1996. Abstracts.

LPNMR'99 - 5th International Conference on Logic Programming and Nonmonotonic Reasoning. El Paso, Texas, USA; 2--4 December 1999.

LFCS'97 - Logic at Yaroslavl - Symposium on Logical Foundations of Computer Science. Yaroslavl, Russia; 6--12 July 1997.

FroCoS'98 - Second International workshop on Frontiers of Combining Systems. ILLC, University of Amsterdam; 2--4 October 1998.

JoLL'2000 - Workshop on Logic and Language. Seville,Spain; 29 November -- 1 December 2000.

LPNMR'97 - 4th International Conference on Logic Programming and Non-Monotonic Reasoning. Dagstuhl, Germany; 28--31 July 1997.

JELIA 2000 - 7th European Workshop on Logics in Artificial Intelligence. Malaga, Spain; 29 September -- 2 October 2000.

9th Annual Logic Summer School - Automated Reasoning Group, Research School of Information Sciences and Engineering, Australian National University, Canberra; 4--15 December 2000.

ISMVL 2000 - International Symposium for Multiple-Valued Logic. Portland, Oregon, USA; 23--25 May 2000. Photos.

LFM'99 - Workshop on Logical Frameworks and Meta-languages. Held as part of the Colloquium on Principles, Logics, and Implementations of High-Level Programming Languages. Paris, France; 28 September 1999. Proceedings in PostScript.

TABLEAUX 2000 - Automated Reasoning with Analytic Tableaux and Related Methods. Held in conjunction with the International Workshop on First-Order Theorem Proving. University of St Andrews, Scotland; 4--7 July 2000. Tutorial notes, photos.

FLOPS'99 - 4th Fuji International Symposium on Functional and Logic Programming. Tsukuba, Japan; 11--13 November 1999.

FOSSACS 2000 - Foundations of Software Science and Computation Structures. Berlin, Germany; 27--31 March 2000.

GÖDEL'96 - Logical Foundations of Mathematics, Computer Science and Physics -- Kurt Gödel's Legacy. Brno, Czech Republic; 25--29 August 1996.

LPAR 2000 - Logic Programming and Automated Reasoning. Reunion Island, France; 11--12 November 2000.

WCP 2000 - Second World Congress on Paraconsistency. Campinas, Brazil; 8--12 May 2000.

FTP 2000 - First-Order Theorem Proving. St. Andrews, Scotland; 3--5 July 2000. Proceedings available.

LPAR'99 - 6th International Conference on Logic for Programming and Automated Reasoning. Tbilisi, Republic of Georgia; 6--10 September 1999.

MFCS'99 - 24th International Symposium on Mathematical Foundations of Computer Science. Szklarska Poreba, Poland; 6--10 September 1999.

TABLEAUX'97 - Analytic Tableaux and Related Methods. Abbaye des Prémontrés, Pont-à-Mousson, France; 13--16 May 1997.

TABLEAUX'99 - Saratoga Springs, NY, USA; 7--11 June 1999.

MFCS'98 - The 23rd International Symposium on Mathematical Foundations of Computer Science. Held jointly with CSL'98, CCA'98, FICS'98 and 68th PSSL. Brno, Czech Republic; 24--28 August 1998.

LFM 2000 - NASA Langley Formal Methods Workshop. Williamsburg, VA, USA; 13--15 June 2000. Photos, tutorial presentations.

ICoS-1 : Inference in Computational Semantics - Amsterdam, the Netherlands; 15 August 1999.

ALP/PLILP/SAS 1996 - Joint meeting of the Fifth International Conference on Algebraic and Logic Programming; Eighth International Symposium on Programming Languages, Implementations, Logics, and Programs; Third International Static Analysis Symposium. Aachen, Germany; 24--27 September 1996.

NMR-2000 - 8th International Workshop on Non-Monotonic Reasoning. Held with KR'2000. Breckenridge, Colorado, USA; 9--11 April 2000. Slides, proceedings.

ARW 2000 - Seventh Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice. King's College London, UK; 20--21 July 2000.

CL 2000 - Conference on Computational Logic. Incorporating DOOD2000 and LOPSTR2000, collocated with ILP2000. Imperial College, London, UK; 24--28 July 2000.

ITRS'00 - Workshop on Intersection Types and Related Systems. Geneva, Switzerland; 15 July 2000. Abstracts, papers and slides.

LOFT4 - Logic and the Foundations of Game and Decision Theory. ICER, Torino, Italy; 30 June -- 2 July 2000.

MPC 2000 - Mathematics of Program Construction. Ponte de Lima, Portugal; 3--5 July 2000. Photos.

Set Theory and its Neighbours 9 - De Morgan House, London; 25 April 2001.

CADE-17 - The 17th International Conference on Automated Deduction. Pittsburgh, PA, USA; 17--20 June 2000.

CADE-16 - The 16th International Conference on Automated Deduction. Trento, Italy; 7--10 July 1999.

TPHOLs 2000 - 13th International Conference on Theorem Proving in Higher Order Logics. Portland, Oregon, USA; 14--18 August 2000.

PLS-2 - 2nd Panhellenic Logic Symposium. Delphi, Greece; 13--17 July 1999.

ICALP'00 - 27th International Colloquium on Automata, Languages, and Programming. Geneva, Switzerland; 9--15 July 2000.

ICALP'98 - 25th International Colloquium on Automata, Languages, and Programming. Aalborg, Denmark; 13--17 July 1998.

PLI'00 - Principles, Logics, and Implementations of High-Level Programming Languages. Including ICFP 2000 and PPDP 2000. Montreal, Canada; 18--23 September 2000.

ICFP 2000 - International Conference on Functional Programming. Associated with PLI 2000. Montreal, Canada; 18--20 September 2000.

PLS-1 - First Panhellenic Logic Symposium. Nicosia, Cyprus; 21--24 July 1997.

TLCA - 5th International Conference on Typed Lambda Calculi and Applications, Krakow, Poland - Krakow, Poland; 2--5 May 2001.

RTA 2000 - 11th International Conference on Rewriting Techniques and Applications. University of East Anglia, Norwich, UK; 10--12 July 2000. Joint with 3rd International Workshop on Explicit Substitutions and Applications; 13 July 2000.

Application of Multiple-Valued Logic to Artificial Intelligence and Data Mining - A MathFIT Workshop. School of Computer Science, Queen's University Belfast; 27 -- 28 April 2001.

LUATCS '99 - First Southern African Summer School and Workshop on Logic, Universal Algebra, and Theoretical Computer Science. Rand Afrikaans University, Johannesburg, South Africa; 1--10 December 1999.

ICC'01 - Third international workshop on Implicit Computational Complexity. Aarhus, Denmark; 20--21 May 2001.

RTA 2001 - 12th International Conference on Rewriting Techniques and Applications. Utrecht, The Netherlands; 22--24 May 2001.

BEST 10 - Boise Extravaganza in Set Theory. Boise State University; 23--25 March 2001.

Seventh Asian Logic Conference - Hsi-Tou, Taiwan; 6--10 June 1999.

Conference and Workshop in Honor of Professor Saharon Shelah - Ben-Gurion University of the Negev, Israel; 21--25 May 2001.

Conference in Honor of D. A. Martin's 60th Birthday - Held in coordination with the Mathematical Sciences Research Institute workshop on The Continuum Hypothesis. University of California, Berkeley, CA, USA; 27--28 May 2001.

2001 Greater Boston Logic Meeting - Boston, MA, USA; 11--13 May 2001.

ICoS-3 : Inference in Computational Semantics - Held jointly with IJCAR 2001. Siena, Italy; 19--20 June 2001.

MFPS XVII - Seventeenth Conference on the Mathematical Foundations of Programming Semantics. Aarhus University, Denmark; 23--27 May 2001.

OntoLex'2000 - Workshop on Ontologies and Lexical Knowledge Bases. Bringing together researchers interested in the dependencies between formal ontologies and lexical semantics in general, and more specifically in the construction of lexical knowledge bases. Sozopol, Bulgaria; 8--10 September 2000. On-line presentations.

BI-DIALOG 2001 - 5th Workshop on Formal Semantics and Pragmatics of Dialogue. ZiF, Bielefeld, Germany; 14--16 June 2001.

The Continuum Hypothesis - A workshop featuring a number of lectures surveying the current insights into the continuum problem and its variations. MSRI, Berkeley, CA, USA; 29 May -- 1 June 2001.

TARK VIII - 8th conference on Theoretical Aspects of Rationality and Knowledge. Certosa di Pontignano, University of Siena, Italy; 8--10 July 2001.

Complexity 2001 - 16th Annual Conference on Computational Complexity. CTI, DePaul University, Chicago IL, USA; 18--21 June 2001.

SAS'01 - The 8th International Static Analysis Symposium. La Sorbonne, Paris, France; 16--18 July 2001.

PLS-3 - 3rd Panhellenic Logic Symposium. 17--22 July 2001; Anogia, Greece.

FLA 2001 - Fuzzy Logic and Applications. Part of the International ICSC Congress on Computation Intelligence Methods and Applications (CIMA 2001). Bangor, Wales, UK; 19--22 June 2001.

Logical Methods - EEF Foundations Summer School on Logical Methods. BRICS, Aarhus, Denmark; 25 June -- 6 July 2001.

ICALP 2001 - 28th International Colloquium on Automata, Languages and Programming. Crete, Greece; 8--12 July 2001.

LACL 2001 - 4th International Conference on Logical Aspects of Computational Linsguistics. Le Croisic, France; 27--29 June 2001.

IJCAR 2001 - International Joint Conference on Automated Reasoning - The fusion of three major events discussing this topic. Includes information on workshop discussions, invited speakers and accepted tutorials. Siena, Italy; 18--23 June 2001.

DL2001 - International Workshop on Description Logics. Stanford University, California, USA; 1--3 August 2001. On-line proceedings.

Description Logics Workshops - Proceedings of past workshops, some on-line.

Semantic Knowledge Acquisition and Categorisation - Workshop at the ESSLLI XIII (European Summer School in Logic, Language and Information). Helsinki, Finland; 13--17 August 2001.

LICS 2001 - IEEE Symposium on Logic in Computer Science. Boston, MA, USA; 16--19 June 2001.

MOL7 - Seventh Meeting on Mathematics of Language. University of Helsinki, Finland; 10--12 August 2001.

Proof and System Reliability - Marktoberdorf Summer School, Germany; 24 July -- 5 August 2001.

The Logic Programming Paradigm: Current Trends and Future Directions - Shakertown, Kentucky, USA; 27--27 April 1998. Photos.

Algebra and Discrete Mathematics - A Euresco conference on the interplay between model theory, infinite combinatorics and various subfields of algebra. Hattingen, Germany; 18 -- 23 August 2001.

Coordination and Action - Workshop in conjunction with ESSLLI 2001. Helsinki, Finland; 13--25 August 2001.

GETCO 2001 - 3rd workshop on Geometric and Topological Methods in Concurrency. In conjunction with CONCUR'01. Aalborg University, Denmark; 25 August 2001.

LCCS 2001 - International Workshop on Logic and Complexity in Computer Science. Créteil, France; 3--5 September 2001.

LICS 2002 - LICS 2002 will be part of the 2002 Federated Logic Conference (FLoC 2002). Copenhagen, Denmark; 20 July -- 1 August 2002.

MFCS 2001 - 26th International Symposium on Mathematical Foundations of Computer Science. Marianske Lazne, Czech Republic; 27--31 August 2001.

FICS'2001 Fixed Points in Computer Science - A Satellite Workshop to PLI'2001. Florence, Italy; 8 September 2001.

Foundational Theories in Mathematics - Department of Mathematics, University of Trento, Italy; 3--7 September 2001.

PLI 2001 - Principles, Logics, and Implementations of high-level programming languages. Including ICFP and PPDP. Firenze, Italy; 2--8 September 2001.

ILP 2001 - Eleventh International Conference on Inductive Logic Programming. Co-located with the Third International Workshop on Learning Language in Logic. Strasbourg, France; September 8--9, 2001.

LLL 2001 - 3rd Learning Language in Logic Workshop. Co-located with ILP 2001. Strasbourg, France; 8--9 September 2001.

CSL'01 - Annual Conference of the European Association for Computer Science Logic. Paris, France; 10--13 September 2001.

LPNMR'01 - 6th International Conference on Logic Programming and Nonmonotonic Reasoning. Vienna, Austria; 17--19 September 2001.

Fourth International Tbilisi Symposium on Language, Logic and Computation - Borjomi, Georgia; 23--28 September 2001.

WFLP 2001 - International Workshop on Functional and (Constraint) Logic Programming, comprising the 10th International Workshop on Functional and Logic Programming and the 16th Workshop on Logic Programming. Kiel, Germany; 13--15 September 2001.

FOTFS III - Complexity in Mathematics and Computer Science. A PhD EuroConference. Institut für Formale Logik, Universität Wien, Austria; 21--24 September 2001.

International Workshop on Computability Theory - S.S.Goncharov - 50th Anniversary. Sobolev Institute of Mathematics, Novosibirsk, Russia; 23--26 September 2001.

Workshop on Model Theory - Institut de Matemàtica de la Universitat de Barcelona (IMUB), Spain; 25--27 October 2001.

ICLP'01 - Seventeenth International Conference on Logic Programming. Paphos, Cyprus; 26 November -- 1 December 2001.

AC2001 - The Thirteenth Amsterdam Colloquium. Universiteit van Amsterdam the Netherlands; 17--19 December 2001.

Logic of Soft Computing - Gargnano, Italy; 19--24 November 2001.

Neutrosophy, Neutrosophic Logic, Set, Probability and Statistics - University of New Mexico; 1--3 December 2001.

LPAR 2001 - 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Havana, Cuba; 3--7 December 2001.

SPR-01. - Semantics, Pragmatics, and Rhetoric. Donostia - San Sebastián, Spain; 22--24 November 2001.

ADMW01 - 3rd Augustus De Morgan Workshop on Frontiers of Revision and Contraction. King's College, London, UK; 5--6 November 2001.

CICLOPS 2001 - Colloquium on Implementation of Constraint and LOgic Programming Systems. Coral Beach Hotel, Paphos, Cyprus; 1 December 2001.

Thematic Afternoon on Constructivism - Including the first Arend Heyting Lecture. Amsterdam, the Netherlands; 14 December 2001.

ICALP'96 - 23rd International Colloquium on Automata, Languages, and Programming. Paderborn, Germany; 8--12 July 1996.

LP-01. - Logic Programming for Artificial Intelligence and Information Systems. A thematic worskhop of EPIA 2001. Porto, Portugal 17--20 December 2001.

Springer Forthcoming Proceedings 2001 - LNCS/LNAI Forthcoming Proceedings 2001: A list of conferences the proceedings of which are to be published in LNCS/LNAI. Includes a number of meetings in Logic.

Types Summer School '99 - Giens, France; 30 August -- 10 September 1999. Photos, tutorial notes and software.

Model Theory 2002 - A regional meeting of the LMS followed by a short conference on Model Theory. School of Mathematics, University of Birmingham, UK; 27 February -- 2 March 2002.

Weighted Automata: Theory and Applications - Dresden, Germany; 4--8 March 2002.

BEST-11 - Boise Extravanagza in Set Theory. Department of Mathematics, Boise State University, Idaho, USA; 29--31 March 2002.

Logic-Based Program Synthesis - AAAI 2002 Spring Symposium. Stanford University, CA, USA; 25--27 March 2002.

SSS-02 - Logic-Based Program Synthesis: State-of-the-Art and Future Trends. AAAI 2002 Spring Symposium. Stanford University, Palo Alto, CA, USA; 25--27 March 2002.

Stanislaw Jaskowski Memorial Symposium - Parainconsistent Logic, Logical Philosophy, Mathematics and Informatics. Nicholas Copernicus University of Torun, Poland; 15-18 July 1998.

ACL2-2002 - Third International Workshop on the ACL2 Theorem Prover and Its Applications. (In conjunction with ETAPS 2002). Grenoble, France; 8--9 April 2002.

TPTS - Workshop on Theory and Practice of Timed Systems. (A satellite event of ETAPS 2002.) Grenoble, France; 6--7 April 2002.

CCF'99 - First Workshop on Constructivity, Complexity, and Fuzziness. Galati, România; 26--28 August 1999.

Proof and Computation - Ludwig-Maximilians-Universität, Munich, Germany; 5--6 November 1999.

Proof Theory and Complexity - Aarhus, Denmark; 3--7 August 1998.

ADD'2002 - SpecialSession on Argument, Dialogue, and Decision at NMR'2002. Toulouse, France; 19--21 April 2002.

KR2002 - Eighth International Conference on Principles of Knowledge Representation and Reasoning. In conjunction with AIPS2002, KSCO'02 and NMR'02. Toulouse, France; 22--25 April 2002.

NMR'2002 - 9th International Workshop on Non-Monotonic Reasoning. (Collocated with KR2002 and AIPS'02.) Toulouse, France; 19--21 April 2002.

DEON'02 - Sixth International Workshop on Deontic Logic in Computer Science. Imperial College, London, UK; 22--24 May 2002.

On the Foundations of Mathematics - Conference in honor of Jan Mycielski. University of Colorado at Boulder, USA; 1--2 June 2002.

ISWC 2002 - The International Semantic Web Conference. Sardinia, Italy; 10--12 June 2002.

LOGICA 2002 - 16th in the series organized by The Institute of Philosophy, Academy of Sciences, Czech Republic. Castle Zahrádky; 18--21 June 2002.

NS2002 - Nonstandard Methods and Applications in Mathematics. Pisa, Italy; 10--16 June 2002.

21st Days of Weak Arithmetics - St.Petersburg, Russia; 7--9 June 2002.

Bounded Arithmetic and Complexity Classes (BACC2002) - Lisbon, Portugal; 28--29 June 2002.

CALCULEMUS-2002 - 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning. Marseille, France; 1--5 July 2002.

TIME-2002 - 9th International Symposium on Temporal Representation and Reasoning Symposium. Manchester, UK; 7--9 July, 2002.

MFCSIT2002 - Second Irish Conference on the Mathematical Foundations of Computer Science and Information Technology. National University of Ireland, Galway; 18--19 July 2002.

CADE-18 - The 18th International Conference on Automated Deduction. Copenhagen, Denmark; 27--30 July 2002.

CLIMA'02 - Computational Logic in Multi-Agent Systems - Affiliated with ICLP 2002. Copenhagen, Denmark; 1 August 2002.

FLoC '02 - Federated Logic Conference - Seven concurrent meetings will be held. Copenhagen, Denmark; 20 July -- 1 August 2002.

ICLP'02 - International Conference on Logic Programming. Copenhagen, Denmark; 29 July -- 1 August 2002.

TABLEAUX 2002 - Automated Reasoning with Analytic Tableaux and Related Methods. Copenhagen, Denmark; 30 July -- 1 August 2002.

WoPaLo - Workshop in Paraconsistent Logic, part of the 14th European Summer School in Logic, Language and Information. Trento, Italy; 5--9 August 2002.

Does Mathematics Require a Foundation? - Arché Centre for Philosophy of Logic, Language, Mathematics and Mind, University of St Andrews, Scotland, UK; 12--15 August 2002.

6BLM - 6th Barcelona Logic Meeting, 5-8 July 2000 - Barcelona, Spain - Areas emphasized are algebraic logic, model theory and set theory.

FLoC 1999 - The 1999 Federated Logic Conference, incorporating CADE, CAV, LICS, RTA. Trento, Italy; 30 June -- 12 July 1999.

ICoS-2 : Inference in Computational Semantics - Dagstuhl, Germany; 29--30 July 2000. Photos, slides.

CSL'02 - Annual Conference of the European Association for Computer Science Logic. Edinburgh, Scotland, UK; 22--25 September 2002.

RTA'02 - 13th International Conference on Rewriting Techniques and Applications (part of the Federated Logic Conference FLoC'02). Copenhagen, Denmark; 22--24 July 2002.

British Colloquium for Theoretical Computer Science - Calendar of meetings.

Logic-Related Conferences - A calendar with links to many of the series in Logic and Computer Science.

Association of Logic Programming - Meetings related to logic programming.

LJ-IGPL, Related Conferences and Events - Year 2001 from the IGPL database, maintained by H-J. Ohlbach.

Springer Forthcoming Proceedings 2002 - A list of conferences the proceedings of which are to be published in LNCS/LNAI. Includes a number of meetings in Logic.

Conferences of Interest for Complexity People - Maintained at the Electronic Colloquium on Computational Complexity.

TARK - Theoretical Aspects of Rationality and Knowledge - Binannual conferences on interdisciplinary issues involving reasoning about rationality and knowledge.

AiML - Advances in Modal Logic - A bi-annual workshop and book series. The aim of the workshop series is to report on important new developments in pure and applied modal logic, at varying locations throughout the world. The book series is based on the workshops.

Boise Extravaganza in Set Theory Conferences - (BEST) organized at Department of Mathematics and Computer Science, Boise State University.

CADE - Conference on Automated Deduction. Annual conference series under the auspices of the Association of Automated Reasoning.

TABLEAUX - The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, held every year since 1992. Links to individual meetings.

FMOODS - Formal Methods for Open Object-based Distributed Systems. An annual series of conferences.

NMRW - International Workshops on Nonmonotonic Reasoning.

KR - Principles of Knowledge Representation and Reasoning. An annual series of conferences.

Set Theory and its Neighbours - A series of one-day meetings held at the London Mathematical Society, De Morgan House, Russell Square, London.

Inference in Computational Semantics (ICoS) - An annual series of workshops. Endorsed by SIGSEM, the ACL Special Interest Group in Computational Semantics.

MFPS - Mathematical Foundations of Programming Semantics. An annual series of meetings.

Methods for Modalities - A series of workshops on the relationship between modal formalisms and computer science.

Formal Methods - World Congress on Formal Methods (FM).

Mathematical Foundations of Programming Semantics - Held annually since 1985.

LICS - IEEE Symposium on Logic in Computer Science: an annual international forum on theoretical and practical topics in computer science that relate to logic in a broad sense.

LOPSTR - International Workshop on Logic-based Program Synthesis and Transformation. Held annually since 1991.

British Logic Colloquium 1998 - King's College, Cambridge; 21--22 September 1998.

British Logic Colloquium 1996 - In memoriam Robin Gandy. Oxford; 5-6 July 1996.

British Logic Colloquium 1999 - University of Wales, Gregynog; 23 -- 25 September 1999. Photos.

British Logic Colloquium 2000 - University of East Anglia, Norwich; 7--9 September 2000.

British Logic Colloquium 2001 - Manchester University; 6--8 September 2001.

Infinite Ink: The Continuum Hypothesis, by Nancy McGough - History, mathematics, metamathematics, and philosophy of Cantor's Continuum Hypothesis

The Axiom of Choice - This page gives a brief explanation of the Axiom of Choice and links to other related websites.

Set Theory - Directory of set theorists, maintained by Jean A. Larson.

Set Theory Page - Collection of links related to set theory.

The Beginnings of Set Theory - MacTutor History of Mathematics topic.

A Crash Course in the Mathematics of Infinite Sets - A introductory guide for philosophers by Peter Suber, explaining the use of infinitary set theory.

Set Theory People - Directory of set theorists.

New Foundations - Set theory introduced by W. V. O. Quine in 1937. This is a refinement of Russell's theory of types based on the observation that the types in Russell's theory look the same, as far as one can apparently prove.

Bounded Set Theory - A weak version of ordinary set theory using bounded quantification. Papers and software.

Issues in Commonsense Set Theory - Paper by Müjdat Pakkan and Varol Akman

Programming with Sets - Using set-theoretic primitives as a conceptual tool in programming, includes discussion of SETL and MIRANDA languages.

Set Theoretic Analysis. - On a part of math where Set Theory, Topology and Analysis meet. Has surveys, preprints, conference announcements, book reviews and problems.

Set Theorists - A list of email addresses and affiliations.

Set Theory for the Working Mathematician - Krzysztof Ciesielski, CUP (1997). Contents and preface.

Operational Set Theory - Description, errata and reviews of a book by Luis E. Sanchis.

Sets and Their Sizes - An alternative to Cantor's theory of cardinality. Dissertation by Fred M. Katz in PDF.

Shelah's Archive - Listing of all articles by Shelah, and links to lots of them.

Cantor's Theorem - Article in the Platonic Realms, describing Cantor's diagonal argument that proved that infinity comes in many different 'sizes'.

Set Theory - From Dave Rusin's "Known Math" collection.

The Future of Set Theory by S. Shelah - The text of a talk by S. Shelah given around the millennium.

The Mathematics of Set Theory - Detailed description of parts of introductory set theory.

Set Theory - Survey from the Stanford Encyclopedia of Philosophy by Thomas Jech.

Metamath Proof Explorer - Over 3000 complete formal proofs deriving numbers and beyond from Zermelo-Fraenkel set theory axioms.

Axiom of Choice and Continuum Hypothesis - Part of the Frequently Asked Questions in Mathematics.

(Australia) Canberra - Automated Reasoning Group. Publications, software, meetings, links. Research areas: mathematical properties of non-classical logics; algorithms for reasoning in classical and non-classical systems.

(Israel) Haifa - Logic Seminar.

(Israel) Ben Gurion University of the Negev - Mathematical and Computational Logic Research Group.

(Japan) Kobe - Foundations of Mathematics and Computer Science.

Linear Naming and Computation - A distributed research group associated with the Church Project working on the design and implementation of new forms of procedure calling protocols based on the notion of linear naming, together with relevant supporting formal tools and implementation technology.

(Colombia) Bogotá - Logic at Bogotá (Universidad Nacional de Colombia, Universidad de los Andes).

Berkeley, University of California - Group in Logic and the Methodology of Science.

Brigham Young University - Laboratory for Applied Logic.

Pennsylvania, University of - Logic and Computation Group.

Las Cruces, New Mexico - Laboratory for Logic,Databases and Advanced Programming.

Carnegie Mellon University - Pure and Applied Logic.

Florida, University of - Logic and Set Theory.

Indiana University - Group in Pure and Applied Logic.

Los Angeles, University of California - Logic and Set Theory.

Michigan, University of - Logic and Foundations.

Minnesota, University of - Mathematical Logic.

Notre Dame - Mathematical Logic.

Pennsylvania State - Mathematical Logic.

Stanford - Logic.

SRI International - Computer Science Laboratory: Formal Methods and Dependable Systems; Rewriting Logics and Systems.

Stanford - Logic Group.

New York, City University - Logic at CUNY and in the New York City region.

University of Maryland at College Park - Computer Science Department, Active Logic Group.

University of Calgary - Logic Research Group.

Urbana-Champaign, University of Illinois - Logic.

(Netherlands) Amsterdam - Institute for Logic, Language and Computation.

(Belgium) Ghent - Centre for Logic and Philosophy of Science.

(Finland) Helsinki - Logic Group.

(Russia) Moscow - Logic Department.

(France) Paris 7 - Mathematical Logic Team.

(Austria) Vienna University of Technology - Group in Applications of Formal Logic.

(Hungary) Budapest - Set Theory and Topology.

(Czech Republic) Prague - Academy of Science, Mathematical Institute, Logic Seminar.

Compulog Net - Europe's Network of Excellence in Computational Logic. Events, educational resources, links.

(Belgium) University of Mons-Hainault - Mathematical Logic.

(Czech Republic) Prague - Charles University, Logic Department.

(Russia) St. Petersburg - Laboratory of Mathematical Logic of the Steklov Institute of Mathematics.

(Sweden) Uppsala - Mathematical Logic.

(Austria) University of Vienna - Department of Formal Logic.

(Italy) University of Pavia - Computational Philosophy Lab.

(Italy) LADSEB-CNR - Ontological Foundations - Research group in ontological foundations of knowledge engineering and conceptual modeling. The group performs basic and applied research on the ontological foundations of knowledge engineering and conceptual modeling, exploring the role of ontology in different fields. The group is characterized by a strong interdisciplinary approach that combines Computer Science, Philosophy, and Linguistics, and relies on Logic as an unifying paradigm. On the application side, main emphasis is given on the use of ontologies for electronic commerce, enterprise integration, knowledge management, and information access to the Web.

(Spain) Barcelona - Logic, History and Philosophy of Science.

(Netherlands) Amsterdam - Dutch Research School in Logic (OZSL).

(France) Paris 1 - Logic Seminar.

Interest Group in Pure and Applied Logics - Sponsored by The European Foundation for Logic, Language and Information (FoLLI). Publications and preprints.

ERCIM Working Group on Constraints - Background, objectives, members and workshops.

(Austria) Linz - Hagenberg - Fuzzy Logic Laboratorium, Softwarepark Hagenberg / Johannes Kepler Universität. Lectures, seminars, publications, staff, projects, other resources.

(Czech Republic) Ostrava - Institute for Research and Applications of Fuzzy Modeling. Staff, projects, publications.

(Czech Republic) Charles University - Constraint and Logic Programming research group. People, research projects, publications and resources.

(Italy) Istituto di Elaborazione della Informazione - Information and news on research activities.

(Spain) Universidad Politécnica de Madrid - Computational Logic, Implementation, and Parallelism Lab.

Manchester Metropolitan University - Department of Computing and Mathematics, Logic and Computation Group. Research projects: Proof Methods for Non-Classical Logics; Temporal and Modal Logics; Programming Language Design; Agent-Based Systems. Members, research interests, bibliography.

University of Leeds - Mathematical Logic Group. Research areas: recursion theory, model theory, set theory and foundations, proof theory, and in applications to algebra, analysis and theoretical computer science. Members, events, seminars.

University of London, Queen Mary Westfield College - Knowledge Representation and Reasoning Group, Applied Logic Colloquium. Schedule.

University of London, Queen Mary Westfield College - Department of Computer Science, Logic and Foundations of Programming group. Members, research projects.

University of Manchester - Department of Computer Science, Formal Methods Group. Members, research projects, meetings and seminars.

University of Manchester - Department of Mathematics, Logic Group. Research interests: model theory, uncertain reasoning and logical aspects of AI, variants of classical set theory and their applications, and formalisation in theory and practice. Members, courses.

University of Manchester - Mathematical Foundations Group. An informal group in mathematics and computer science. Members, seminars and lecture notes.

University of Oxford - Mathematical Institute, Mathematical Logic group. Members, seminars. Home of the Model Theoretic Exchange.

University of St. Andrews - School of Philosophical and Anthropological Studies; Department of Philosphy; includes Logic and Metaphysics.

University of St. Andrews - Department of Computer Science, Computational Logic group. Members, events, publications, collaborators.

University of St. Andrews - Arché: Centre for the Philosophy of Logic, Language, Mathematics and Mind.

Aachen - Mathematical Foundations of Computer Science.

Bonn - Mathematical Logic Group.

Freiburg - Institute for Mathematical Logic and Foundations of Mathematics.

Heidelberg - Mathematical Logic.

Karlsruhe - Department for Logic, Complexity, and Deduction Systems. [site is in German; some pages available in English]

Munich - Mathematical Logic.

Introduction to Model Theory - Homepage of a lecture course by Natasha Alechina, with a particular emphasis on topics relevant to computer science, such as bisimulation.

Model Theory. Skolem's Paradox. Ramsey's Theorem. - Introductory essay by Karlis Podnieks, constituting appendices 1 and 2 of his book `Around Goedel's Theorems'.

Model Theory of Fields: Suggested Reading - Short list of online resources compiled by David Marker.

Finite Model Theory Homepage - People, problems, bibliographies, events.

Mission: Critical - Interactive tutorial for critical thinking.

The Daily Translation - Problems on translation into a logical system, drawn from the current news and updated daily.

Stephen Downes : Fallacies - Stephen's Guide to the Logical Fallacies.

Core Concepts in Critical Thinking - A classroom guide.

Logic Software from CSLI - Hyperproof, Tarski's World, Turing's World, and The Language of First-order Logic, educational logic software by Jon Barwise and John Etchemendy

Games Mathematicians Play - Mathematical games from a logical point of view: strategies for games and using games in descriptive complexity.

Infinity - Exploring the logical basis and practical meaning of infinite sets.

University of Alberta Logic Course - Contains an introduction to logic and formal systems, revolving around the Mizar proof checker, and a guide to Mizar.

The Logic Classroom - A course in basic logic consisting of 5 studies with exercises and answers to promote the learning of logic. Homeschool, college, and seminary students.

Around Gödel's Theorem - (Hyper)textbook for students in mathematical logic, by Karlis Podnieks.

Gödel's Theorem and Information - G.J.Chaitin's proof of Gödel's theorem using arguments having an algorithmic information theory flavor.

Mathematics and Logic - Site dedicated to Math and Logic education. Games, software, worksheets, puzzles.

Lyceum Tutorial Services - Philosophy and logic tutoring (paid services).

The Logic Daemon - On-line proof checker, and texts.

Logic for Mathematics and Computer Science - Supplementary material to Stanley Burris' logic textbook, with lecture notes, course development hints, and additional text including historical notes.

A Problem Course in Mathematical Logic; by Stefan Bilaniuk - Volume I: Propositional and First-Order Logic. Volume II: Computability and Incompleteness.

Formal Methods Educational Materials - A repository for information related to formal methods in education, including pointers to existing courses and suggestions for examples and projects.

logic-l - Elementary Logic Discussion List.

Course on Description Logics - Slides and notes by Enrico Franconi.

OBBLOG - Logic construction toybox. Binary logic simulator to explain binary logic and truth tables. Javascript.

Logic Tutorial - An interactive tool teaching basic formal logic, rendering truth tables as clickable Johnston diagrams. With notes on the Buddhist Nagarjuna and modern symbolic logic.

ASL Committee on Logic Education - Reports and resources from the Association of Symbolic Logic.

The Logic Cafe - An online textbook, courseware package, and homework assistant for introductory symbolic logic. Includes multimedia support.

Disjunction - Theory and history of the binary connective 'or'; from the Stanford Encyclopdia of Philosophy by Ray Jennings.

ECCC - Electronic Colloquium on Computational Complexity - The Electronic Colloquium on Computational Complexity is a new forum for the rapid and widespread interchange of ideas, techniques, and research in computational complexity. The Electronic Colloquium on Computational Complexity (ECCC) welcomes papers, short notes and surveys with relevance to the theory of computation

Computability Theory - Directory of researchers working in computability theory, and list of open problems.

Bibliographic Database for Computability Theory - Extensive bibliography on computability and recursion theory, maintained by Peter Cholak.

Computability and Complexity - An online course on complexity.

Problem Solving Environments Home Page - This site contains information about Problem Solving Environments (PSEs), research, publications, and information on topics related to PSEs.

Hypercomputation Research Network - The study of computation beyond that defined by the Turing machine, also known as super-Turing, non-standard or non-recursive computation. Links to people, resources and discussions.

Church-Turing Thesis - Alonzo Church and Alan Turing formulated the thesis that computability coincides with recursivity; by Jack Copeland.

Introduction to Logic and Recursion Theory - Notes from the class taught by Prof. Sacks in the Spring of 1998.

Mizar Project - An attempt to reconstruct mathematical vernacular into a formal language which can be read by humans and also verified by software.

QED Project - Build a single, distributed, computerized repository that rigorously represents all important, established mathematical knowledge

Practical Foundations of Mathematics - Online text of the book by Paul Taylor, together with supporting materials. The text aims to provide a conceptual and formal foundation for mathematics and computer science.

A Century of Controversy over the Foundations of Mathematics - Edited transcript of a lecture by Gregory Chaitin, author of `The Unknowable'.

Arché - The Arche project looks at the foundations of mathematics, especially at Frege's Theorem and its ramifications. Based at the University of St Andrews.

FOM - A closed, moderated, e-mail list for discussing Foundations of Mathematics moderated by Martin Davis. Archive available.

Mediaeval Logic and Philosophy - Resource maintained by Paul Vincent Spade at Indiana University.

The Summulae of John Buridan - A critical introduction by Gyula Klima.

On Dialectic - By St. Augustine. Latin original together with translation by J. Marchand.

Medieval Theories of Analogy - Entry in the Stanford Encyclopaedia of Philosophy, by E. Jennifer Ashworth.

Medieval Theories of Modality - Article at the Stanford Encyclopaedia of Philosophy.

12th Century Logic - A medieval logic resource, maintained by Iwakuma Yukio. Includes many online texts and resources, as well as exhaustive census of medieval logic manuscripts.

Scholastic Logic - Chapter Two of Joseph Perrier's "The Revival of Scholastic Philosophy in the Nineteenth Century" (1909).

Scholasticism - Online text by Joseph Rickaby (1908).

Aristotle's Reform of Paideia - Article by Evelyn Barker, arguing that the principal aim of Aristotle's Organon was to reform the contemporary paedagogical role of dialectic.

Square of Opposition - Article in the Stanford Encyclopaedia of Philosophy, by Terence Parsons.

Logic - Entry in the Catholic Encyclopaedia (1917), dominated by a historical survey from Indian and Pre-Aristotelian philosophy to the Logic of John Stuart Mill.

Aristotle's Logic - Introductory article by Garth Kemerling.

19th Century Logic between Philosophy and Mathematics - Article by Volker Peckhaus.

Peter of Spain (Petrus Hispanus) - Life and work of 13th century logician and author of the Tractatus; from the Stanford Encyclopedia by Joke Spruyt.

Who are Boole, Fitch, and Tarski? - Brief biographies of the logicians whose names appear in Barwise and Etchemendy's textbook Language, Proof and Logic.

Georg Cantor - Biography of Georg Cantor (1845-1918) from the MacTutor History of Mathematics Archive.

Georg Cantor - Brief biography from the Real Analysis website.

Cantor Set and Function - Introduction to the Cantor discontinnuum.

Georg Cantor - Complete bibliography of Cantor's writings.

The Late 19th Century Origins of Set Theory - Historical survey by Phillip E. Johnson, with a focus on Cantor's life and work.

The Church-Turing Thesis - Article from the Stanford Encyclopedia.

Alan Mathison Turing - Undergraduate biographical essay by John M. Kowalik.

Alan Turing - Biography from the MacTutor History of Mathematics archive.

Turing Digital Archive - Digital archive of items relating to Alan Turing.

Alan Mathison Turing (1912-1954) - British mathematician, cryptographer, and one of the key inventors of the modern computer. After his profound contributions to helping win World War II, he was persecuted for his homosexuality by his own government, and driven to suicide. Superb site maintained by noted Turing biographer Andrew Hodges: extensive resources and links, online versions of several long essays on Turing's extraordinary impact.

Alan Turing - Biographical entry in the FOLDOC.

Turing Machine - Article on Turing Machines from the Stanford Encyclopedia.

Alan Turing Archive - Archive and historical records pertaining to the work of computing pioneer Alan Turing.

On Computable Numbers with an Application to the Entscheidungsproblem - Turing's paper which discusses the halting problem in the context of Gödel's Incompleteness Theorem. HTML.

Wired Archive: Alan Turing - Stories involving Turing.

Alan Turing Papers - Collection record of Turings papers at Kings College, Cambridge.

Alan Turing: The Biography Project - Biography, bibliography and links.

Alan Turing - Encyclopedia biography from Wikipedia.

Alan M. Turing - Entry from the Stanford Encyclopedia of Philosophy by Andrew Hodges.

Gottlob Frege - Short biography from the Metaphysics Research Lab at Stanford.

Frege, Logic, and Jena - Extensive biographical site on Frege and Jena, the city where he lived and worked (in German).

Gottlob Frege - Biography from the MacTutor History of Mathematics archive.

Frege's Logic, Theorem, and Foundations for Arithmetic - Stanford Encyclopedia article on Frege's work on the foundations of mathematics.

Frege - Interpretative essay on Frege's philosophy by Rainer Born.

Gottlob Frege - Brief biography from The Window.

Gottlob Frege - Entry from the Stanford Encyclopedia.

Gottlob Frege - Brian Carver's resources page on Gottlob Frege.

Frege: Two Theses, Two Senses - Article by Carlo Penco discusses a vacillation by Frege in his account of the relation between thoughts and sentences. Penco discusses the attempts to resolve this uncertainty by Currie, Dummett and others before advancing his own account.

A Slice of Philosophy: Gottlob Frege (1848-1925) - A slice of Frege's life and works. Listing of all his works and suggestions to secondary literature.

Frege - Article in Björn's Guide To Philosophy.

Gödel's Ontological Argument - Paper by Chris Small about Gödel's proof of the existence of God.

Kurt Gödel in Blue Hill - A brief account of Kurt Gödel's trip to Blue Hill, Maine, in the summer of 1942, by Peter Suber.

Kurt Gödel Society - International organization for the promotion of research in the areas of Logic, Philosophy, History of Mathematics, above all in connection with the biography of Kurt Gödel, and in other areas to which Gödel made contributions, especially mathematics, physics, theology, philosophy.

Kurt Gödel - Biography from the MacTutor History of Mathematics archive.

Collected Works I - Publications 1929-1936. Oxford University Press catalog entry.

Collected Works II - Publications 1938-1974.

Collected Works III - Unpublished essays and lectures.

Gödel: A Life of Logic - By John L. Casti and Werner DePauli. Book review of this biography.

Alonzo Church - Biography from the MacTutor History of Mathematics archive.

Church-Turing Thesis - Article in the Stanford Encyclopedia.

The Need for Abstract Entities - Philosophical paper by Alonzo Church

The Bulletin of Symbolic Logic, December 1995 - Contains obituary by H. B. Enderton.

George Boole - Biography from the MacTutor History of Mathematics archive.

Boole, George (1815-1864) - Entry in the Jones Telecommunications and Multimedia Encyclopedia.

The Calculus of Logic - Seminal paper of 1848 available in various formats.

George Boole - the Lincoln Genius - Biography from Roger Parsons' "Lincolnshire World", by Eileen Harrison.

Papers of George Boole - Brief overview of his papers at University College Cork Library.

Georges Boole : Philosophe ou matématicien? - Paper by Sabine Séguin (in French).

Charles S. Peirce Studies - Web site devoted to the life and works of C. S. Peirce.

Peirce Edition Project (IUPUI) - Organize and date the manuscripts to produce an approved scholarly edition of Peirce's writings (Indianapolis, USA).

Charles Sanders Peirce - Essay from Encephi, by Robert Tremblay (in French).

Peirce's Logic - Entry from the Stanford Encyclopedia.

Charles S. Peirce - Biography from the MacTutor History of Mathematics archive.

Institute for Studies in Pragmaticism - Center for research on the life and works of Charles Sanders Peirce.

Arisbe - Home of the International Peirce Telecommunity (papers online).

Digital Encyclopedia of Charles Sanders Peirce - Brings together the most recent writings about Pierce, and new works inspired by the logician.

Charles Sanders Peirce - Discusses the scientist's interest in infinite sets, probability theory, two distinct kinds of induction and other topics. Includes a brief biography. Entry from the Stanford Encyclopedia by Robert Burch.

Transactions of the Charles S. Peirce Society - Journal specializing in the history of American philosophy. Includes list of editors, table of contents and subscription information.

Mathematical Problems of David Hilbert - Text of Hilbert's 1900 address in English.

David Hilbert - Biography from the MacTutor History of Mathematics Archive.

David Hilbert - Brief biography and the full text of the lecture on Mathematical Problems (in German).

David Hilbert - Brief biography with references.

Hilbert's Problems - Article in the Platonic Realms. Lists 23 problems posed to the second international mathematics congress in 1900 AD.

Jan Lukasiewicz - Page at the Polish Philosophy site; includes biobliography, papers on Lukasiewicz.

Jan Lukasiewicz - Biography from the MacTutor History of Mathematics archive.

Alfred Tarski - Biography from MacTutor History of Mathematics archive.

Alfred Tarski - Page at the Polish Philosophy site.

Introduction to Logic - "Introduction to Logic and to the Methodology of the Deductive Sciences"; Oxford University Press catalog entry.

The Bulletin of Symbolic Logic, June 1999 - Contains paper on Tarski's system of geometry, by Tarski and Givant.

The Semantic Conception of Truth - Famous paper by Alfred Tarski (1944).

Emil Post - Biography of Emil Leon Post (1897-1954).

Post's Problem of Creativity - An essay discussing some of Post's philosophical ideas in a biographic setting.

Post's Correspondence Problem - A page dedicated to one of the original algorithmically undecidable problems.

E.L. Post Manuscript Guide - Notes on papers and correspondence by Post at the American Philosophical Society.

PCP@HOME Contest - A project to find short instances of Post's Correspondence Problem with large shortest solutions.

Post's Problem - A short historic note describing the problem and mentioning some of the major contributors.

Skolem Issue of the Nordic Journal of Philosophical Logic - Special issue with articles by Jens Erik Fenstad, Herman Ruge Jervell, Hao Wang, Grigori Mints, Matti Eklund on Skolem's life and work.

Thoralf Skolem (1887-1963) - Biography from MacTutor History of mathematics archive.

Bernays, Paul - Biography of Paul Bernays (1888-1977) from the MacTutor History of Mathematics Archive.

The Bernays Project - Research project to edit and translate Bernays's philosophical writings into English.

Zermelo Project - Scientific biography of Ernst Zermelo, site contains bibliography of Zermelo's writings and papers on Zermelo.

Ernst Zermelo - Biography from the MacTutor History of Mathematics archive.

Old Directions in Free Logic - Article by Gyula Klima. An analysis of the controversy over existential import in syllogistic theory, relating it to modern work in Free Logic.

Aristotelian and Modern Logic - Article by Katalin Havas, discussing the nature of progress in logic, and the idea of logic as a perfected discipline.

Aristotle's Singular Negative Syllogistic and Free Logic - Article by V.I. Markin, Moscow State University.

The Modernity of Aristotle's Logical Investigations - Article by George Boger, presented at the 20th World Congress in Philosophy.

Colibri Home Page - Colibri is an electronic newsletter and WWW service aimed at people interested in the fields of natural language processing, speech processing and/or logic.

Notre Dame Journal of Formal Logic - Publisher's site, access restricted.

History and Philosophy of Logic - Publisher's site.

Modern Logic - International Journal for the History of Mathematical Logic, Set Theory, and Foundations of Mathematics.

Journal of Logic and Computation - Publisher's site. Unrestricted access only for subscribers.

Annals of Pure and Applied Logic - Unrestricted access only for subscribers.

Logic Journal of the IGPL - Official publication of the Interest Group in Pure and Applied Logic.

Journal of Automated Reasoning - Published by Kluwer.

Archive for Mathematical Logic - (Springer) Tables of contents from vol.34 (1995) on. Full text to subscribers via LINK.

Journal of Philosophical Logic - Journal devoted to philosophical applications of logic, and the philosophical underpinnings of logic. Published by Kluwer, this site contains a sample copy and an archive of tables of contents.

IEEE CS MVL-TC Bulletin - Volumes 17-19 (1996-8) only.

Studia Logica - Editors' site.

Nordic Journal of Philosophical Logic - All articles available online.

Israel Journal of Mathematics - Publisher's site.

Fundamenta Mathematicae - Publisher's site.

Journal of Logic, Language and Information - Publisher's site.

Journal of Mathematical Logic - World Scientific. Contents and abstracts of all issues; full text to institutional subscribers.

Logic Journal of the IGPL - An Electronic Journal on Pure and Applied Logic. Editors' page with author information.

The Journal of Logic Programming - Elsevier. Now The Journal of Logic and Algebraic Programming.

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.

History and Philosophy of Logic - Editor's site.

Logical Analysis and History of Philosophy - Intends to provide a forum for articles in which classical philosophical texts are interpreted by drawing on the resources of modern formal logic; abstracts online.

Studia Logica - Publisher's site.

Bulletin of Symbolic Logic - All articles in postscript format.

Colloquium Mathematicum - Colloquium Mathematicum frequently publishes research articles in foundations.

Journal of Functional and Logic Programming - Electronic journal.

Reports on Mathematical Logic - (Jagiellonian University Press) Contents and abstracts from no.25 (1991).

Journal of Logic, Language and Information - Editors' site.

Journal of Symbolic Logic - Official organ of the Association of Symbolic Logic.

Journal of Applied Non-Classical Logics - Includes aims and scopes, editorial staff and contact information.

Shelah, Saharon - Personal bibliography hyperlinked.

Omega Bibliography - Almost complete bibliography of mathematical logic and related fields, goes back to Boole and Frege! Note: Name search is case-sensitive. Description in German.

xxx Math Front: LO Logic - Front for the xxx Mathematics Archive

References in Finite Model Theory - Bibliography maintained by Argimiro Arratia-Quesada.

Bibliography on Linear Logic - Indexed by author. In HTML, PS, DVI and BibTeX.

Set Theory with a Universal Set - List of publications and websites on axiomatic set theories.

Journal of Logic and Computation - Unofficial bibliography as part of Hypertext Bibliography Project.

Research Index: Computer Science: Theory: Logic - Research Index is a major project to provide access to research science in a format that benefits from the interconnectivity of the internet.

Lambda Calculus - Introduction to the lambda calculus for computer scientists. Shows how the calculus can be formalised in Scheme.

Dual Identity Combinators - Article by Katalin Bimbó presented at the 20th World Congress of Philosophy. Investigates the addition of identity combinators, in the formulae-as-types sense, to combinatory logic.

Kolmogorov Complexity in Combinatory Logic - Online article by John Tromp. Kolmogorov complexity is a recursion theoretic characterisation of randomness.

Lambda - An online introduction to the lambda calculus by Lloyd Allison, complete with a web form that will evaluate lambda expressions.

Perl Contains the Lambda-Calculus - Explains why this computer program is well suited to apply to functional application.

A presentation of the Curry-Howard Correspondence (1997) - Notes on the Curry-Howard correspondence by Chantal Berline.

Computational Content of Classical Logic (1996) - Lecture notes from a research seminar series by Thierry Coquand covering double-negation translations, game semantics of classical logic and point-free topology.

On the computational content of the Axiom of Choice (1995) - Article by S. Berardi, M. Bezem and T. Coquand presenting a possible computational content of the negative translation of classical analysis with the Axiom of Choice.

CPS Translations and Applications: the Cube and Beyond (1996) - Article by G. Barthe, J. Hatcliff, and M.H. Sørensen which presents a CPS translation to Barenderegt's `cube' of pure type systems, and applies this to provide a formulae-as-types correspondence for higher-order classical predicate logic.

A Curry-Howard Foundation for Functional Computation with Control (1997) - Article by C.-H. L. Ong and C. A. Stewart which presents a call-by-name variant of Parigot's lambda-mu calculus. The calculus is proposed as a foundation for first-class continuations and statically scoped exceptions in functional programming languages.

A Semantic View of Classical Proofs (1996) - Article by C.-H. Luke Ong presenting the semantics of classical proof theory from three prespectives: a formulae-as-types characterisation in a variant of Parigot's lambda-mu calculus, a denotational characterisation in game semantics, and a categorical semantics as a fibred CCC.

Extracting Constructive Content from Classical Logic via Control-like Reductions - Article by F. Barbanera and S. Berardi showing how computational content may be extracted from proofs in Peano Arithmetic by a variant of a method proposed by William Tait.

Computational Isomorphisms in Classical Logic - Article by V. Danos, J. B. Joinet and H. Schellinx examining the categorical semantics of classical logic from a persepctive inspired by linear logic.

A Notion of Classical Pure Type System (1997) - Article by Gilles Barthes.

On the Formulae-as-Types Correspondence for Classical Logic - Doctoral thesis of Charles Stewart, which investigates foundational aspects of the application of the formulae-as-types correspondence to classical logic, and extends the treatment to include intensional equality and induction.

A Non Functional Calculus: Linear Logic and Concurrency (2000) - (CiteSeer) This paper proposes the *-calculus as an approach that unifies Abramsky's proofs-as-processes approach with Boudol and Berry's Chemical Abstract Machine approach.

The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes (1998) - (CiteSeer) This PhD thesis proposes the fusion calculus as a simplified pi-calculus with many formal advantages.

Pi-Calculus and Linear Logic (1992) - (CiteSeer) Article by Bellin and Scott showing how classical linear logic may be interpreted in the pi calculus, thus supporting Abramksy's `Proofs as Processes' thesis.

Retracing Some Paths in Process Algebra (1996) - (CiteSeer) Discursive article by Samson Abramksy reexamining some early ideas in the theory of processes in the light of later logical parallels.

Completeness Results for Linear Logic on Petri Nets (1993) - (CiteSeer) Article by Engberg and Winskel showing that Petri nets provide a class of model for linear logic that is complete.

Automated Reasoning - Survey of automated deduction and theorem proving; from the Stanford Encyclopedia of Philosophy by Frederic Portoraro.

MetaPRL logical programming environment - The next generation of the NuPrl proof development system. The main new features of MetaPRL include: 1) Modularity. Programs and logics are developed as modules that define computational, heuristic, and mathematical properties. 2) Speed. MetaPRL is more than two orders of magnitude faster than NuPrl.

The LEGO Proof Assistant - A powerful tool for interactive proof development in the natural deduction style. It supports refinement proof as a basic operation. The system design emphasizes removing the more tedious aspects of interactive proofs.

Alfa - A successor to the proof editor Alf with a graphical user interface, being developed at the Programming Logic Group at Chalmers. Available for download.

NuPrl Proof Development System - A powerful tactic-based proof assistant, developed over the last 15 years at Cornell University. IFeatures include: very expressive logical language based on Martin-Lof type theory, extensive library of formal mathematics and automata theory, possibility of an extraction a certified program from the constructive proof of its formal specification, graphical proof editor. NuPrl was successfully used in verifying components of the Ensemble group communications system.

Proof General - Emacs based generic interface for theorem provers.

Kumo - A web-based proof assistant. It assists with proofs in first order hidden logic, using OBJ3 as a reduction engine. The most important inference rules in first order logic and hidden equational logic are implemented, including induction and coinduction, generates proof documentation for the web, supports distributed cooperative proving.

Yarrow - A proof-assistant for Pure Type Systems (PTSs), representing different logics and programming languages. A basic knowledge of Pure Type Systems and the Curry-Howard-de Bruijn isomorphism is required. (This isomorphism says how you can interpret types as propositions.)

Af2 Proof Assistant - A type system based on second order intuitionistic logic.

Isabelle - Homepage of the theorem prover environment developed by Larry Paulson at Cambridge University and Tobias Kipkow at TU Munich.

The Practice of Logical Frameworks - Comprehensive survey article by Frank Pfenning (1996) discussing the history of work on logical frameworks and their current open problems.

The HOL Theorem Proving System - The system documented originated at the Laboratory for Applied Logic of Brigham Young University and features higher-order, classical, natural deduction with tactics.

CtCoq - a working environment for the Coq theorem prover (XWindow)

The Coq proof assistant - Allows the user to handle calculus assertions, to check mechanically proofs of these assertions, helps to find formal proofs, extracts a certified program from the constructive proof of its formal specification.

Logic Programming in the LF Logical Framework (1991) - Article by Frank Pfennig describing a logic programming language which serves as a proof search engine for LF.

Non Standard Logics - A comprehensive listing of flavours of non-standard logic with brief descriptions and references, compiled by Peter Suber.

Infinitary Logic - Article in the Stanford Encyclopaedia of Philosophy by John L. Bell. Infinitary Logic is a branch of formal logic where finitary formulae are replaced by potentially infinitary mathematical entities.

Modal Logic - Originally the study of deductive behavior of the expressions `it is necessary that' and `it is possible that', now also includes logics for belief, tense, the deontic (moral) expressions. From the Stanford Encyclopedia, by James W. Garson.

Logic System Interrelationships - Shows how a number of representative logics fit together. The interrelationships usually given as something of the form: System X is system Y plus the axiom Z. By John Halleck.

Computational Tools for Modal Logic - Resources collected by Renate Schmidt.

What are Weak Arithmetics - Notes defining the subject. Available in HTML and PS formats.

Mally's Deontic Logic - Discussion of Ernst Mally's logic of obligation; from the Stanford Encyclopedia by Gert-Jan Lokhorst.

Topics in Logic and Proof Theory - Brief introductions to combinatory logic, the incompleteness theorems and independence results, by Andrew D Burbanks.

Ground Temporal Logic: A Logic for Hardware Verification - A temporal logic designed to specify properties of hardware at the register transfer level.

The Temporal Logic of Actions - A logic for specifying and reasoning about concurrent systems.

Centre for Agent Research and Development - Among other activities, this group explores topics related to temporal logic including temporal resolution methods.

Temporal Logic Case Study - A case study applying temporal logic to specify the operation of a bank of identical elevators servicing a number of floors in a building.

Kono's Temporal Logic Related Information - A collection of papers by Shinji Kono on the Interval Temporal Logic.

Time International Workshop Series - The annual International Workshop on Temporal Representation and Reasoning covers temporal representation and reasoning, including temporal logic.

Spin - A general tool for verifying the correctness of distributed software (designs) in a rigorous and mostly automated fashion. Can be used as a full linear temporal logic model checking system.

Temporal Logic - The Stanford Encyclopedia of Philosophy entry on the subject, with a detailed description, application areas and a bibliography.

TemporalRover - Provides automatic verification of protocols and reactive systems through temporal logic specifications.

Marking up Temporal Logic - First in a series of posts to the www-math mailing list on using TL operators in web pages. Clicking [Prev] will continue through the series.

Temporal Logic in Information Systems - A survey of the field by Jan Chomicki and David Toman. From the 1997 BRICS Lecture Series.

Efficient Symbolic Tools - A BDD based tool for the formal verification of concurrent systems using a propositional branching-time temporal logic: action computation tree logic (ACTL). It runs under different OS, including Linux and Windows 95/98/NT.

Interval Temporal Logic - A flexible notation for both propositional and first-order reasoning about periods of time found in descriptions of hardware and software systems. Includes table of contents, abstracts and pdf downloads.

Fuzzy Logic Jump Start - Shows some examples of how this system would work. Includes instruction on method, perception, and sets. Also, gives details on how to create a logic controller as home exercise.

Fuzzy Systems by James F. Brule' - Covers the history, main concepts, applications and peer objections. Includes bibliography and additional resources.

Fuzzy Logic - Survey of logical systems with a continuum of truth values; from the Stanford Encyclopdia by Petr Hajek .

Fuzzy Logic Sources - Maintained by Bob John, De Montfort University.

An Introduction to Substructural Logics - Website for the book `Consequenc