[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

Hales08
  1. Thomas Hales
  2. Formal Proof
  3. Notices of the American Mathematical Society V55n11 (Dec 2008) [ tx081101370p.pdf ]
  4. =EXAMPLES HOL Light FORMAL PROOFS MATHEMATICS ZFC TYPES
  5. Good discussion of the philosophy of formal proofs and HOL Light in particular.
  6. Difficult theorems can have 1728 pages for an informal proof and take decades to write.
  7. Provide formalizations can take years.
  8. DeBruijn_factor::=Length of a formal proof/Length of a conventional proof.
  9. List of 12 "real" theorems that have got formal proofs.
  10. Description of HOL_light.
  11. Discussion of full automation and automated discovery of theorems.
  12. Coq::proof_assistant= See http://coq.inria.fr/.
  13. HOL_light::proof_assistant= See http://www.cl.cam.ac.uk/~jrh13/hol-light/.
  14. Isabelle::proof_assistant= See http://isabelle.in.tum.de/.
  15. Mizar::proof_assistant= See http://mizar.org/.
  16. ProofWeb::proof_assistant= See http://prover.cs.ru.nl/login.php.
  17. QED::manifesto= See http://www.cs.ru.nl/~freek/qed/qed.html.

Search for bibliographic items containing a matching string.


(Search uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.



To see the complete bibliography (1Mb+) select:[Bibliography]