Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Compactness Theorem for First-...

view this post on Zulip Email Gateway (Feb 27 2025 at 07:20):

From: Tobias Nipkow <nipkow@in.tum.de>
Compactness Theorem for First-Order Logic
Sophie Tourret and Lawrence C. Paulson

This is a translation of a HOL Light formalization covering foundational results
in first-order model theory, including the compactness of first-order logic. The
original work is described in the following paper: Formalizing Basic First Order
Model Theory John Harrison Proceedings of the 11th International Conference on
Theorem Proving in Higher Order Logics, TPHOLs'98, Springer LNCS 1497, pp.
153-170. The corresponding HOL Light theories can be found on GitHub.

https://www.isa-afp.org/entries/FOL_Compactness.html

Enjoy!

smime.p7s

Last updated: Mar 09 2025 at 12:28 UTC