Internet References

Philosophy
- The Internet Encyclopedia of Philosophy (http://www.utm.edu/research/iep/)
- Stanford Encyclopedia of Philosophy (http://plato.stanford.edu/)

Mathematics (foundations)
- Foundations of Mathematics (http://sakharov.net/foundation.html)

Logic
- Logical Systems (http://www.earlham.edu/~peters/courses/logsys/lshome.htm) (Peter Suber, Earlham College)
- Glossary of First Order Logic (http://www.earlham.edu/%7Epeters/courses/logsys/glossary.htm)
- Mathematical Logic (http://www.uni-bonn.de/logic/world.html) around the world
- Logic software and logic education (http://www.cs.otago.ac.nz/staffpriv/hans/logiccourseware.html)
- Mathematical Logic Seminar (http://www-logic.stanford.edu/seminars.html) (Stanford University)
- Wikipedia - Logic (http://en.wikipedia.org/wiki/Logic)
- Logic and Ontology (http://plato.stanford.edu/entries/logic-ontology)

AI, ATP, programming and computation
- Automated theorem proving (http://en.wikipedia.org/wiki/Theorem_prover)
- Automated Reasoning (http://plato.stanford.edu/entries/reasoning-automated)
- Artificial intelligence (http://en.wikipedia.org/wiki/Artificial_intelligence)
- Computer Math Proof Shows Reasoning Power (http://www.nytimes.com/library/cyber/week/1210math.html)
- Logic and Artificial Intelligence (http://plato.stanford.edu/entries/logic-ai)
- Logic and AI (http://www.rpi.edu/%7Ebrings/LOG%2BAI/lai/lai.html): What's the relationship?
- AI on the Web (http://www.cs.berkeley.edu/%7Erussell/ai.html)
- Computer Ethics (http://setis.library.usyd.edu.au/stanford/entries/ethics-computer/) What are they?
- Early History of Automated Deduction (http://cs.nyu.edu/cs/faculty/davism/early.ps) (Martin Davis article)
- An Overview of Automated Theorem Proving (http://www.math.miami.edu/%7Etptp/OverviewOfATP.html)
- The CADE ATP System Competition (http://www.cs.miami.edu/~tptp/CASC/)

Institutions, academic organizations
- Automated Deduction Systems and Groups (http://www-unix.mcs.anl.gov/AR/others.html)
- Bibliographies on Logic Programming (http://liinwww.ira.uka.de/bibliography/LogicProgramming/)
- Research Groups in Logic and Theoretical Computer Science (http://www-compsci.swan.ac.uk/%7Ecsetzer/logic-server/index.html)
- Stanford Knowledge Systems Laboratory (http://ksl.stanford.edu/)
- Stanford Formal Reasoning Group (http://www-formal.stanford.edu/)
- American Mathematical Society (http://www.ams.org/)
- Association for Symbolic Logic (http://www.aslonline.org/)
- Association for Computing Machinery (http://www.acm.org/)
- American Philosophical Association (http://www.acm.org/)
- Logic at Stanford (http://www-logic.stanford.edu/)
- The Center for the Study of Language and Information (CSLI) (http://www-csli.stanford.edu/)
- SRI (http://www.sri.com/)
- Automated Reasoning Group HOL page (http://www.cl.cam.ac.uk/Research/HVG/HOL/)

Journals, listservs, bibliographies
- Foundations of Mathematics Listserv (http://www.math.psu.edu/simpson/fom/)
- Journal of Symbolic Logic (http://theory.lcs.mit.edu/%7Edmjones/hbp/jsyml/)
- Computer Science Bibliography (http://www.informatik.uni-trier.de/%7Eley/db/index.html) (DBLP)
- CiteSeer (http://citeseer.csail.mit.edu/)
- Journal of Automated Reasoning (http://www-unix.mcs.anl.gov/JAR/)
- Association for Automated Reasoning (http://www-unix.mcs.anl.gov/AAR/)

Projects

TPTP (http://www.cs.miami.edu/%7Etptp/)

Common Logic (http://philebus.tamu.edu/cl/)

KIF
- Knowledge Interchange Format (KIF) (http://www-ksl.stanford.edu/knowledge-sharing/kif/)
- Knowledge Interchange Format, dpAns (http://logic.stanford.edu/kif/dpans.html)
- Knowledge Interchange Format (http://logic.stanford.edu/kif/specification.html)

Stanford Knowledge Systems Laboratory
- Stanford KSL Network Services (http://www-ksl-svc.stanford.edu:5915/&service=frame-editorKSL)
- JTP An Object Oriented Modular Reasoning System (http://www.ksl.stanford.edu/software/JTP/)
- JTP User Manual (http://www.stanford.edu/~gkfrank/jtp/)
- OKBC implementations and documents (http://www-ksl-svc.stanford.edu:5915/doc/release/okbc/index.html)

Cyc (http://www.cyc.com/)
OpenCyc (http://www.opencyc.org/)

Standard Upper Ontology (SUO) Working Group (http://suo.ieee.org/)

DAML/OIL/RDF
- DARPA Agent Markup Language (http://www.daml.org/)
- DAML+OIL (March 2001) (http://www.daml.org/language/)
- DAML Axiomatic Semantics (http://www.daml.org/2001/03/axiomatic-semantics.html)

W3C
- W3C Math Home Page (http://www.w3c.org/Math/)

Semantic Web (http://www.w3.org/2001/sw/)

International Standard for the Z Notation (http://web.comlab.ox.ac.uk/oucl/research/groups/zstandards/)

Theorem provers and proof assistants on the Internet
- Tau (http://hsinfosystems.com/taujay/index.html)
- ACL2 (http://www.cs.utexas.edu/users/moore/acl2/)
- Bliksem (http://www0.risc.uni-linz.ac.at/systems/documentation/AutomatedDeductionSystems/SupportedSystems/bliksem/)
- Carine (http://www.atpcarine.com/)
- Coq (http://coq.inria.fr/)
- EQP Equational Theorem Prover (http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html)
- Isabelle (http://www.cl.cam.ac.uk/Research/HVG/Isabelle/)
- Gandalf (http://www.ttu.ee/it/gandalf/)
- HOL (http://cs.anu.edu.au/student/comp8033/hol.html)
- Lego (http://www.dcs.ed.ac.uk/home/lego/)
- LCF (see HOL)
- MetaPRL (http://metaprl.org/)
- METEOR (http://www.cs.duke.edu/~ola/meteor.html)
- Mizar (http://www.cs.ualberta.ca/~mizar/)
- Models And Counter-Examples (MACE) (http://www-unix.mcs.anl.gov/AR/mace/)
- NuPrl (http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html)
- Otter (http://www-unix.mcs.anl.gov/AR/otter/)
- Nqthm (ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html)
- Paradox (http://www.math.chalmers.se/~koen/paradox/)
- PHOX (http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html)
- PROTEIN (http://www.uni-koblenz.de/ag-ki/Systems/PROTEIN/)
- Prover9 (http://www-unix.mcs.anl.gov/~mccune/prover9/)
- PTTP - Prolog Technology Theorem Prover (http://www.ai.sri.com/~stickel/pttp.html)
- PVS (http://pvs.csl.sri.com/)
- Simplify (http://citeseer.ist.psu.edu/detlefs03simplify.html)
- Spark (http://www.sparkada.com/)
- Spass (http://spass.mpi-sb.mpg.de/)
- SNARK (http://www.ai.sri.com/~stickel/snark.html) - SRI's New Automated Reasoning Kit
- The leanTAP Home Page (http://i12www.ira.uka.de/leantap/)
- The LogiCal Project (http://logical.inria.fr/)
- Theorem Prover 3TAP (http://mathforum.org/library/view/17325.html)
- Twelf (http://www.cs.cmu.edu/~twelf/)
- Vampire (http://en.wikipedia.org/wiki/Vampire_theorem_prover)
- Waldmeister (http://www.mpi-sb.mpg.de/~hillen/waldmeister/)

A selection of people of interest (and their papers on the Internet)