Skip to content
Permalink
Browse files

Added a compendium of old work on formalizing metatheory of first-ord…

…er logic

and proof procedures. (I've never previously made this generally available,
but have now supplied it privately several times over.) It's a combination of
stuff described here:

    Formalizing Basic First Order Model Theory
    Proceedings of the 11th International Conference on Theorem Proving
    in Higher Order Logics, TPHOLs'98, Springer LNCS 1497, pp. 153-170.

    https://www.cl.cam.ac.uk/~jrh13/papers/model.html

and later work done purely for my own satisfaction, as a correctness check
when writing my textbook on automated reasoning:

    "Handbook of Practical Logic and Automated Reasoning"
    Cambridge University Press 2009

    https://www.cl.cam.ac.uk/~jrh13/atp/index.html
  • Loading branch information...
jrh13 committed Jun 15, 2019
1 parent 3a1ec4a commit 013324af7ff715346383fb963d323138cf011732
Showing with 17,415 additions and 0 deletions.
  1. +27 −0 Logic/README
  2. +1,186 −0 Logic/birkhoff.ml
  3. +681 −0 Logic/canon.ml
  4. +1,093 −0 Logic/fol.ml
  5. +314 −0 Logic/fol_prop.ml
  6. +1,147 −0 Logic/fole.ml
  7. +2,047 −0 Logic/given.ml
  8. +998 −0 Logic/givensem.ml
  9. +175 −0 Logic/herbrand.ml
  10. +765 −0 Logic/linear.ml
  11. +851 −0 Logic/lpo.ml
  12. +51 −0 Logic/make.ml
  13. +1,382 −0 Logic/positive.ml
  14. +662 −0 Logic/prenex.ml
  15. +827 −0 Logic/prolog.ml
  16. +829 −0 Logic/resolution.ml
  17. +1,206 −0 Logic/skolem.ml
  18. +956 −0 Logic/support.ml
  19. +256 −0 Logic/trs.ml
  20. +1,962 −0 Logic/unif.ml
@@ -0,0 +1,27 @@
FORMALIZED METATHEORY OF FIRST-ORDER LOGIC

(c) John Harrison 1998-2008

This is a miscellany of results involving formalization of first-order
logic and various proof systems, particularly automated theorem proving
methods like resolution. It's a combination of work published here:

Formalizing Basic First Order Model Theory
Proceedings of the 11th International Conference on Theorem Proving
in Higher Order Logics, TPHOLs'98, Springer LNCS 1497, pp. 153-170.

https://www.cl.cam.ac.uk/~jrh13/papers/model.html

and later work done as a correctness check when writing my textbook on
automated reasoning:

"Handbook of Practical Logic and Automated Reasoning"
Cambridge University Press 2009

https://www.cl.cam.ac.uk/~jrh13/atp/index.html

There is additional formalization work connected with the material
there on limitations (Tarski, Goedel etc.). That can be found in the
"Arithmetic" subdirectory of the HOL Light repository

https://github.com/jrh13/hol-light/tree/master/Arithmetic

Large diffs are not rendered by default.

Large diffs are not rendered by default.

0 comments on commit 013324a

Please sign in to comment.
You can’t perform that action at this time.