Logic and Foundations Math

[Find on this page]

- Classical Logic
- Computability Logic Homepage
- Introduction to Mathematical Logic
- Mathematical Logic and Foundations
- Mathematical Logic around the World
- Mind Versus Goedel by Damjan Bojadziev


Computability
- Bibliographic Database for Computa...
- Church-Turing Thesis
- Computability and Complexity
- Computability and Complexity in An...
- Computability Logic - Wictionary
- Computability Theory
- Hypercomputation Research Network
- Interactive Computation
- Introduction to Logic and Recursio...
- Open Questions in Recursion Theory
- Problem Solving Environments Home Page

Computational Logic
- CiteSeer Index: Computer Science: ...

Computational Logic Automated Reasoning
- Automated Reasoning

Computational Logic Classical Logic
- A Curry-Howard Foundation for Func...
- A Notion of Classical Pure Type Sy...
- A Semantic View of Classical Proof...
- Computational Content of Classical...
- Computational Isomorphisms in Clas...
- CPS Translations and Applications:...
- Extracting Constructive Content fr...
- On the computational content of th...
- On the Formulae-as-Types Correspon...

Computational Logic Combinatory Logic and Lambda Calculus
- Dual Identity Combinators
- Kolmogorov Complexity in Combinato...
- Lambda

Computational Logic Coq
- CtCoq
- The Coq proof assistant

Computational Logic Formulae-as-Types Correspondence
- A presentation of the Curry-Howard...

Computational Logic LF Logical Framework
- Logic Programming in the LF Logica...

Computational Logic Logical Frameworks
- Af2 Proof Assistant
- Alfa
- Isabelle
- Kumo
- MetaPRL logical programming enviro...
- NuPrl Proof Development System
- Proof General
- The HOL Theorem Proving System
- The LEGO Proof Assistant
- The Practice of Logical Frameworks
- Yarrow

Computational Logic Proofs as Processes
- A Non Functional Calculus: Linear ...
- Completeness Results for Linear Lo...
- Pi-Calculus and Linear Logic (1992)
- The Fusion Calculus: Expressivenes...

Directories
- ASL members
- Computability Theory
- Description Logics
- Knowledge Representation
- Logic and Set Theory
- Logic and Set Theory
- Logic Links
- Logic Page
- Logic Programming
- Mathematical Logic and Foundations
- Mathematical Logic around the world
- Research groups in Logic and Theor...

Education
- A Problem Course in Mathematical L...
- Around Gödels Theorem
- ASL Committee on Logic Education
- Course on Description Logics
- Disjunction
- Formal Methods Educational Materials
- Gödels Theorem and Information
- Games Mathematicians Play
- Infinity
- Logic Software from CSLI
- Logic Tutorial
- Logical Laws
- Mission: Critical
- The Daily Translation
- The Logic Cafe
- The Logic Classroom
- The Logic Daemon
- University of Alberta Logic Course

Foundations
- A Century of Controversy over the ...
- Arché
- FOM
- Foundations of Mathematics
- Hilbert II - Mathematical Foundati...
- Mizar Project
- Practical Foundations of Mathematics
- QED Project

Game Semantics
- Game Semantics
- Game Semantics or Linear Logic?
- Game Theory
- Game_Semantics
- Is Game Semantics Necessary?
- Logic and Games

Game Semantics People
- Abramsky, Samson
- Blass, Andreas
- Hyland, J.M.E.
- Japaridze, Giorgi
- Ong, Luke
- Parikh, Rohit
- Van Benthem, Johan

History
- Aristotles Logic
- Aristotles Reform of Paideia
- Earliest Uses of Symbols of Set Th...
- Logic
- Mediaeval Logic and Philosophy
- Medieval Theories of Analogy
- Medieval Theories of Modality
- On Dialectic
- On Dialectic
- Peter of Spain (Petrus Hispanus)
- Scholastic Logic
- Scholasticism
- Square of Opposition
- Syllogistic logic online
- The Summulae of John Buridan

History Ancient and Modern Logic
- Aristotelian and Modern Logic
- Aristotles Singular Negative Syllo...
- Modern Interpretation of Ancient L...
- Old Directions in Free Logic
- The Modernity of Aristotles Logica...

History Bernays, Paul
- Bernays, Paul
- The Bernays Project

History Boole, George
- George Boole
- George Boole - the Lincoln Genius
- George Boole (1815 - 1864)
- Papers of George Boole
- The Calculus of Logic


History Cantor, Georg
- Georg Cantor
- Georg Cantor
- Georg Cantor
- Georg Ferdinand Ludwig Philipp Cantor

History Church, Alonzo
- Alonzo Church
- Church-Turing Thesis
- The Bulletin of Symbolic Logic, De...
- The Need for Abstract Entities

History Frege, Gottlob
- A Slice of Philosophy: Gottlob Fre...
- Frege
- Frege: Two Theses, Two Senses
- Freges Logic, Theorem, and Foundat...
- Gottlob Frege
- Gottlob Frege
- Gottlob Frege
- Gottlob Frege
- Gottlob Frege
- On Sense and Reference
- Philosophy Professor

History Gödel, Kurt
- Gödel
- Gödel: A Life of Logic
- Gödels Ontological Argument
- Godels Theorems
- Kennys Overview of Hofstadters Exp...
- Kurt Gödel
- Kurt Gödel
- Kurt Gödel
- Kurt Gödel in Blue Hill
- Kurt Gödel Society

History Hilbert, David
- David Hilbert
- David Hilbert
- Hilbert Edition
- Hilberts Problems
- Hilberts Program
- Mathematical Problems of David Hilbert

History Lukasiewicz, Jan
- A note on Lukasiewiczs three-valu...
- Jan Lukasiewicz
- Jan Lukasiewicz
- Jan Lukasiewicz
- Logic and determinism in Jan Lukas...
- Lukasiewicz and Lesniewski on Cont...
- Lukasiewicz in Dublin

History Peirce, Charles Sanders
- Charles S. Peirce
- Charles S. Peirce Studies
- Charles Sanders Peirce
- Charles Sanders Peirce
- Institute for Studies in Pragmaticism
- Peirce Edition Project (IUPUI)
- Peirces Logic
- Philosophy Professor
- Transactions of the Charles S. Pei...

History People
- Who are Boole, Fitch, and Tarski?

History Post, Emil L.
- E.L. Post Manuscript Guide
- Emil Post
- PCP@HOME Contest
- Posts Correspondence Problem
- Posts Problem of Creativity

History Skolem, Thoralf
- Skolem Issue of the Nordic Journal...
- Thoralf Skolem (1887-1963)

History Tarski, Alfred
- Alfred Tarski
- The Bulletin of Symbolic Logic, Ju...
- The Semantic Conception of Truth

History Turing, Alan Mathison
- Alan M. Turing
- Alan Mathison Turing
- Alan Mathison Turing (1912-1954)
- Alan Turing
- Alan Turing
- Alan Turing
- Alan Turing Archive
- Alan Turing Papers
- Alan Turing: The Biography Project
- Alan Turing: Thinking Up Computers
- On Computable Numbers with an Appl...
- The Church-Turing Thesis
- Turing Machine
- Wired Archive: Alan Turing

History Zermelo, Ernst
- Ernst Friedrich Ferdinand Zermelo
- Ernst Zermelo

Institutions
- (Australia) Canberra
- (Colombia) Bogotá
- (Israel) Ben Gurion University of ...
- (Israel) Haifa
- (Japan) Kobe
- Linear Naming and Computation
- Logic at Leeds Homepage

Institutions Europe
- (Austria) Linz - Hagenberg
- (Austria) University of Vienna
- (Austria) Vienna University of Tec...
- (Belgium) Ghent
- (Belgium) University of Mons-Hainault
- (Czech Republic) Charles University
- (Czech Republic) Ostrava
- (Czech Republic) Prague
- (Czech Republic) Prague
- (Finland) Helsinki
- (France) Paris 1
- (France) Paris 7
- (Hungary) Budapest
- (Italy) Istituto di Elaborazione d...
- (Italy) LADSEB-CNR - Ontological F...
- (Netherlands) Amsterdam
- (Netherlands) Amsterdam
- (Russia) Moscow
- (Russia) St. Petersburg
- (Spain) Barcelona
- (Spain) Universidad Politécnica de...
- (Sweden) Uppsala
- Compulog Net
- ECOR: European centre for ontologi...
- ERCIM Working Group on Constraints
- Interest Group in Pure and Applied...

Institutions Germany
- Aachen
- Bonn
- Freiburg
- Heidelberg
- Munich

Institutions North America
- Berkeley, University of California
- Brigham Young University
- Carnegie Mellon University
- Florida, University of
- Indiana University
- Las Cruces, New Mexico
- Michigan, University of
- Minnesota, University of
- New York, City University
- Pennsylvania State
- Pennsylvania, University of
- SRI International
- Stanford

Institutions North America (part 2)
- University of Calgary
- University of Maryland at College Park
- Urbana-Champaign, University of Il...

Institutions United Kingdom
- Manchester Metropolitan University
- University of Leeds
- University of Manchester
- University of Manchester
- University of Oxford
- University of St. Andrews
- University of St. Andrews
- University of St. Andrews

Knowledge Representation and Planning
- Knowledge Representation
- Texas Action Group

Meetings
- Deon06 homepage
- Logic and Algorithms


Meetings BLC
- British Logic Colloquium
- British Logic Colloquium 1996
- British Logic Colloquium 1998
- British Logic Colloquium 1999
- British Logic Colloquium 2000
- British Logic Colloquium 2001
- British Logic Colloquium 2002
- British Logic Colloquium 2004

Meetings Calendars
- Association of Logic Programming
- British Colloquium for Theoretical...
- LJ-IGPL, Related Conferences and E...
- Logic-Related Conferences

Meetings ESSLLI
- ESSLLI 2001
- ESSLLI 2003
- ESSLLI 2004
- ESSLLI97
- ESSLLI98
- ESSLLI99
- European Summer School in Logic, L...

Meetings ISMVL
- ISMVL 2000
- ISMVL 2001
- ISMVL 2002
- ISMVL 2003

Meetings Logic Colloquium
- Logic Colloquium 2000
- Logic Colloquium 2002
- Logic Colloquium 2004
- Logic Colloquium 96
- Logic Colloquium 98
- Logic Colloquium 99

Meetings Past Conferences
- 2001 Greater Boston Logic Meeting
- 21st Days of Weak Arithmetics
- 6BLM
- 9th Annual Logic Summer School
- AC2001
- ACL2-2002
- ADD2002
- ADMW01
- Algebra and Discrete Mathematics
- BI-DIALOG 2001
- CADE-17
- CADE-18
- CCF99
- CICLOPS 2001
- CiE 2005
- CL 2000
- CLIMA02 - Computational Logic in M...
- Computation Prospects of Infinity
- Computer-Supported Mathematical Th...
- Conference and Workshop in Honor o...
- Conference in Honor of D. A. Marti...
- Coordination and Action
- CSL 2000
- CSL01
- CSL02
- DEON02
- Description Logics Workshops
- DL2001
- FICS2001 Fixed Points in Computer ...
- FLA 2001
- FLoC 02 - Federated Logic Conference
- FLoC 1999
- FOSSACS 2000
- FOTFS III
- Fourth International Tbilisi Sympo...
- FroCoS96
- GÖDEL96
- GETCO 2001
- ICALP96
- ICC01
- ICLP01
- ICLP02
- ICLP99
- Infinite Games
- International Workshop on Computab...
- ISMVL 2000
- ISWC 2002
- ITRS00
- JELIA 2000
- JELIA 2004
- JoLL2000
- KR2002
- LACL 2001
- LCCS 2001
- LICS 2001
- LICS 2002
- LLL 2001
- LOFT4
- Logic and Mathematics: Connections...
- Logic of Soft Computing
- Logic, Algebra and Geometry
- Logical Methods
- LP-01.
- LPAR 2000
- LPAR 2001
- LPNMR01
- LPNMR97
- MFCS 2001
- MFCS98
- MFCSIT2002
- Model Theory and Applications to A...
- Neutrosophy, Neutrosophic Logic, S...
- NMR-2000
- NMR2002
- NS2002
- OntoLex2000
- PLI 2001
- PLI00
- PLS-1
- Proof and Computation
- Proof and System Reliability
- RTA 2003
- RTA02
- Set Theory and Analysis
- Set Theory and its Neighbours 9
- SPbDLC99
- SPR03
- TABLEAUX 2000
- TABLEAUX 2002
- TABLEAUX99
- TARK VIII
- The Continuum Hypothesis
- The Logic Programming Paradigm: Cu...
- TLCA - 5th International Conferenc...
- TPHOLs 2000
- TPTS
- Turing 2004: A Celebration of his ...
- Types Summer School 99
- WCP 2000
- Weighted Automata: Theory and Appl...
- WFLP 2001
- WILF 2005
- WoPaLo
- Workshop on Logical Foundations of...
- Workshop on Model Theory
- World Congress on Paraconsistency
- World Congress on Universal Logic

Meetings Series
- Boise Extravaganza in Set Theory C...
- CADE
- FMOODS08
- Formal Methods
- LICS
- LOPSTR
- MFPS
- NMRW
- Set Theory and its Neighbours
- TABLEAUX
- TARK - Theoretical Aspects of Rati...

Meetings WoLLIC
- WoLLIC - Vision
- WoLLIC 97
- WoLLIC 99
- WoLLIC2000
- WoLLIC2001
- WoLLIC2002

Model Theory
- Finite Model Theory Homepage
- Introduction to Model Theory
- Model Theory of Fields: Suggested ...
- Model Theory. Skolems Paradox. Ram...

Nonstandard Logics and Extensions
- Computability Logic
- Infinitary Logic
- Logic System Interrelationships
- Non Standard Logics
- What are Weak Arithmetics

Nonstandard Logics and Extensions Fuzzy Logic
- Fuzzy Logic
- Fuzzy Logic
- Fuzzy Logic
- Fuzzy Logic Archive
- Fuzzy Logic Jump Start
- Fuzzy Logic Sources
- Fuzzy Systems by James F. Brule

Nonstandard Logics and Extensions Intuitionistic Logic
- A Bibliography of Constructive Mat...
- Confessions of a Formalist, Platon...
- Constructive Mathematics
- Intuitionistic logic
- Intuitionistic Logic
- Intuitionistic Logic
- Intuitionistic Logic
- Intuitionistic Topology and Founda...
- Porgi

Nonstandard Logics and Extensions Linear Logic
- A New Deconstructive Logic: Linear...
- Applications of Linear Logic to Co...
- Articles by Jean-Yves Girard
- Bibliography on Linear Logic
- Chu Spaces
- Chu Spaces from the Representation...
- Flow Analysis in the Geometry of I...
- Game Semantics or Linear Logic?
- Introduction to Linear Logic
- Linear Logic as a Good Logical Fou...
- Linear Logic Papers by Andreas Blass
- Linear Logic Primer
- Linear Logic Semantics
- Phil Wadlers Linear Logic Publications
- Seminar on Linear Logic and Applic...
- The Linear Logic Pages

Nonstandard Logics and Extensions Many-valued Logic
- MacColl and Many-Valued Logic: An ...
- Many-Valued Logic
- Multi-valued Logic Home Page
- Multiple-valued Logic: A Tutorial
- Polyvalued Logic
- Resources for Many-Valued Logic
- The Logic of More

Nonstandard Logics and Extensions Martin-Löfs Type Theory
- Extensional Concepts in Intensiona...
- Implementing Mathematics Using NuPrl
- Inductive Definitions in Type Theory
- Martin-Löf Type Theory: Semantics ...
- Nuprl Project Related Web Sites
- Research Profile of Anton Setzer

Nonstandard Logics and Extensions Modal Logic
- Computational Tools for Modal Logic
- Mallys Deontic Logic
- Modal epistemic logic
- Modal Logic
- Modal Logic
- Modal Logic
- Modal Logic
- Modal Logic
- Modal Logics
- Modality, Si! Modal Logic, No!
- The Calculus of Structures - Modal...

Nonstandard Logics and Extensions People
- Abbasbandy, Saeid
- Afzalian, Ali
- Beg, Ismat
- Cornelis, Chris
- De Cock, Martine
- De Cock, Martine
- Fukuda, Toshio
- Joslyn, Cliff
- Kruse, Rudolf
- Mendel, Jerry
- Zadeh, Lofti

Nonstandard Logics and Extensions People
- Artemov, Sergei
- Beklemishev, Lev
- Boolos, George
- Dosen, Kosta
- Guglielmi, Alessio
- Japaridze, Giorgi
- Muravitsky, Alexei
- Van Benthem, Johan
- Verbrugge, Rineke
- Zambella, Domenico

Nonstandard Logics and Extensions People
- Abramsky, Samson
- Asperti, Andrea
- Benton, Nick
- Braüner, Torben
- Cervesato, Lliano
- Danos, Vincent
- De Paiva, Valeria
- Delzanno, Giorgio
- Dosen, Kosta
- Fages, Francois
- Gallier, Jean
- Galmiche, Didier
- Gardner, Philippa
- Harland, James
- Hodas, Joseph
- Honsell, Furio
- Hyland, Martin
- Japaridze, Giorgi
- Lincoln, Patrick
- Miller, Dale
- Ong, Luke
- Perrier, Guy
- Pfenning, Frank
- Pitts, Andrew
- Shankar, Natarajan
- Tammet, Tanel
- Tamura, Naoyuki
- Wadler, Philip
- Winikoff, Michael
- Winskel, Glynn

Nonstandard Logics and Extensions Provability and Interpretabili
- Cointerpretability
- Cotolerance
- Giorgi Japaridzes Publications
- Interpretability
- Interpretability Logic

Nonstandard Logics and Extensions Provability and Interpretabili (part 2)
- Interpretability Logic
- Provability Logic
- Provability Logic
- Tolerance

Nonstandard Logics and Extensions Relevance Logic
- Relevance Logic
- Relevance Logic and Concurrent Com...

Nonstandard Logics and Extensions Substructural Logics
- Substructural and Paraconsistent L...
- Substructural Logics

Nonstandard Logics and Extensions Temporal Logic
- Efficient Symbolic Tools
- Interval Temporal Logic
- JMCA - Java ModelChecking Application
- Marking up Temporal Logic
- Temporal Logic
- Temporal Logic Case Study
- Temporal Logic in Information Systems
- TemporalRover
- The Temporal Logic of Actions
- Time International Workshop Series

Online Discussion Groups
- Frogs
- Jon Cohens That Logic Blog
- Richard Zachs Logic and Philosophy...

Organizations
- ALP
- ASL
- British Logic Colloquium
- COMPULOG Americas
- Computability in Europe Homepage
- CSHPM
- DVMLG
- EACSL
- FoLLI
- IGPL
- KR, Inc.
- Kurt Gödel Society
- UP Eulogica. Asias First Student L...

People
- Aczel, Peter
- Andrews, Peter B.
- Artemov, Sergei
- Avigad, Jeremy
- Awodey, Steve
- Baldwin, John T.
- Barendregt, Henk
- Bartoszynski, Tomek
- Beklemishev, Lev
- Blass, Andreas R.
- Bouscaren, Elisabeth
- Buechler, Steven
- Burris, Stanley
- Buss, Samuel R.
- Carlstrom, Jesper
- Carnielli, Walter A.
- Chaitin, Gregory J.
- Chatzidakis, Zoé
- Cholak, Peter
- Cummings, James
- Danos, Vincent
- Darničre, Luck
- Dosen, Kosta
- Ebbinghaus, Heinz-Dieter
- Enderton, Herbert B.
- Etchemendy, John
- Feferman, Solomon
- Fitting, Melvin
- Flum, Jörg
- Foreman, Matthew
- Forster, T. E.
- Friedman, Sy D.
- Gehrke, Mai
- Gerla, Giangiacomo
- Goldstern, Martin
- Grossberg, Rami
- Guglielmi, Alessio
- Hähnle, Reiner
- Herwig, Bernhard
- Hindley, J. R.
- Hjorth, Greg
- Hodges, Wilfrid
- Holmes, Randall
- Howard, Paul
- Hustadt, Ullrich
- Hyland, J. Martin E.
- Japaridze, Giorgi
- Jech, Thomas
- Jockusch, Carl G.
- Junker, Markus
- Kaiser, Klaus
- Kanamori, Akihiro
- Kastermans, Bart
- Kaye, Richard
- Kechris, Alexander S.
- Knight, Julia F.
- Kunen, Kenneth
- Lafont, Yves
- Lakemeyer, Gerhard
- Larson, Jean A.
- Lascar, Daniel
- Leivant, Daniel
- Lempp, Steffen
- Lessmann, Olivier
- Levesque, Hector
- Lindell, Steven
- Luo, Zhaohui
- Maddy, Penelope
- Makowsky, Johann (Janos) A.
- Marcos, Joăo
- Marker, David
- Matiyasevich, Yuri
- McKenzie, Ralph
- Miller, Dale
- Mitchell, William
- Monk, Donald
- Moreno, Javier
- Moschovakis, Yiannis N.
- Moss, Lawrence
- Nelson, Edward
- Nerode, Anil
- Ong, C.-H. Luke
- Ono, Hiroakira
- Parikh, Rohit
- Pedicini, Marco
- Pfenning, Frank
- Pitts, Andrew
- Plotkin, Gordon
- Pollett, Chris
- Pratt, Vaughan
- Prest, Mike
- Pym, David J.
- Quigley, Peter
- Rathjen, Michael
- Regnier, Laurent
- Robinson, Edmund
- Rubin, Jean E.
- Scedrov, Andre
- Schmidt, Renate
- Scott, Dana
- Setzer, Anton
- Shore, Richard A.
- Sieg, Wilfried
- Simpson, George
- Sipser, Michael
- Slaman, Theodore A.
- Soare, Robert I.
- Solovay, Robert M.
- Statman, Richard
- Stewart, Charles
- Taylor, Paul
- Van Benthem, Johan
- Van Dalen, Dirk
- Vereshchagin, Nikolai
- Vickers, Steven
- Vlad, Serban E.
- Wansing, Heinrich
- Wehmeier, Kai
- Welch, Philip
- White, Graham
- Wilkie, Alex
- Zach, Richard
- Ziegler, Martin
- Zilber, Boris

People Students and Independent Scholars
- Anand, Bhupinder Singh
- Costa-Leite, Alexandre
- Flannery, Ryan

Proof Theory
- G. Japaridzes Papers
- Linear Network
- Logic of programming
- Mathematical Reasoning Group
- Proof Theory
- Proof Theory as an Alternative to ...
- Proof Theory on the Eve of Year 2000
- ProofTheory.ORG
- The Calculus of Structures
- The Epsilon Calculus
- Topics in Logic and Proof Theory

Proof Theory People
- Artemov, Sergei
- Beklemishev, Lev
- Buss, Samuel
- Guglielmi, Alessio
- Japaridze, Giorgi

Publications
- Colibri Home Page

Publications Bibliographies
- Journal of Logic and Computation
- Set Theory with a Universal Set
- Shelah, Saharon

Publications Books
- Practical Foundations of Mathematics
- Proofs and Types

Publications Journals
- Annals of Pure and Applied Logic
- Archive for Mathematical Logic
- Bulletin of Symbolic Logic
- Fundamenta Mathematicae
- History and Philosophy of Logic
- Israel Journal of Mathematics
- Journal of Automated Reasoning
- Journal of Functional and Logic Pr...
- Journal of Logic and Computation
- Journal of Logic, Language and Inf...
- Journal of Mathematical Logic
- Journal of Philosophical Logic
- Journal of Symbolic Logic
- Logic Journal of the IGPL
- Mathematical Logic Quarterly
- Nordic Journal of Philosophical Logic
- Notre Dame Journal of Formal Logic
- Reports on Mathematical Logic
- Studia Logica
- Transactions on Computational Logic

Set Theory
- A Crash Course in the Mathematics ...
- A New System of Axioms Instead of ZF
- Axiom of Choice and Continuum Hypo...
- Bounded Set Theory
- Cantors Theorem
- Consequences of the Axiom of Choic...
- Equivalence Relation
- Extending Set Theory
- Infinite Ink: The Continuum Hypoth...
- Metamath Proof Explorer
- New Foundations
- Operational Set Theory
- Programming with Sets
- Set Theoretic Analysis.
- Set Theorists
- Set Theory
- Set Theory
- Set Theory
- Set Theory for the Working Mathema...
- Set Theory Page
- Shelahs Archive
- The Axiom of Choice
- The Beginnings of Set Theory
- The Future of Set Theory by S. Shelah

Set Theory People
- Abraham, Uri
- Aharoni, Ron
- Andréka, Hajnal
- Apter, Arthur
- Bagaria, Joan
- Bankston, Paul
- Barbanel, Julius
- Bartoszynski, Tomek
- Bilaniuk, Stefan
- Blass, Andreas
- Brendle, Joerg
- Brown, Elizabeth Theta
- Burke, Dennis
- Burke, Douglas
- Burke, Maxim
- Cameron, Peter
- Cenzer, Douglas
- Cherlin, Gregory
- Ciesielski, Krzysztof
- Clemens, John D.
- Corazza, Paul
- Csirmaz, László
- Cummings, James
- Dehornoy, Patrick
- Devlin, Keith
- Di Nasso, Mauro
- Dobrinen, Natasha
- Donder, Dieter
- Dordal, Peter Lars
- Dzamonja, Mirna
- Eklof, Paul
- Enderton, Herbert B.
- Farah, Ilijas
- Fleissner, William
- Foreman, Matthew
- Forster, T.E.
- Friedman, Sy D.
- Galvin, Fred
- Gao, Su
- Gitik, Moti
- Goldstern, Martin
- Grossberg, Rami
- Larson, Jean A.

Software
- ACL2 Version 2.7
- Automated Reasoning Project
- Bertrand
- Church
- CrocoPat: Simple and Efficient Rel...
- Database of Existing Mechanized Re...
- DC Proof Online
- DELORES
- Gateway to Logic
- Isabelle
- JImp Theorem Prover
- Llprover
- Logic Software from CSLI
- LOOM
- LWB
- ModLeanTAP: Lean Tableau-based Ded...
- MUltlog
- MUltseq
- Paradox
- Proof General
- ProofPower
- PROTEIN
- PVS
- Spreadsheet Logic
- The Coq Project
- Tree Proof Generator
- VeriFun
- Visual Turing
- WinKE