Higher-Order Logic Theorem Provers < Formal Methods in the Yahoo! Directory

WWW Virtual Library: HOL Theroem Prover
Document contains some pointers leading to information on the HOL mechanical theorem proving system, based on Higher Order Logic.
www.comlab.ox.ac.uk/archive/formal-methods/hol.html
HOL: The Higher Order Logic Theorem Prover
Paper detailing the HOL, a tool used for assisting in the specification and verification of digital hardware.
cs.anu.edu.au/student/comp8033/hol.html
Application Specific Higher Order Logic Theroem Proving (PDF)
Academic paper, the aim of which is to provide experimental results that compare the performance of the tool discussed on large scale hardware exmaples. PDF file.
www.kroening.com/papers/verify2002.pdf
Interactive Theorem Proving in Higher-Order Logic (PDF)
Outlines the associated paradoxes, functions, and tactics.
www.cs.nott.ac.uk/~lad/MR/lcf_handout.pdf
First-Order Proof Tactics in Higher-Order Logic Theorem Provers
Paper evaluating the effectiveness of first-order proof procedures when used as tactics for proving subgoals in a higher-order logic interactive theorem prover.
www.cl.cam.ac.uk/users/jeh1004/research/papers/metis.html

Formal Methods > Higher-Order Logic Theorem Provers