定理证明和高阶逻辑

Proof Theory as an Alternative to Model Theory

http://www-lp.doc.ic.ac.uk/UserPages/staff/ft/alp/comment/proof.html

FTP'2000

http://www.uni-koblenz.de/ftp00/

Mathematical Reasoning Group

http://dream.dai.ed.ac.uk/

Description of the HOL Theorem Proving System

http://lal.cs.byu.edu/lal/hol-desc.html

Isabelle

http://www.cl.cam.ac.uk/Research/HVG/Isabelle/

Software, Theorem Provers

http://www.tcs.informatik.uni-muenchen.de/~matthes/logikserver/software.html

Inductive Theorem Prover INKA 4.0

http://www.dfki.de/vse/systems/inka/

TABLEAUX

http://i12www.ira.uka.de/TABLEAUX/

/**/