The semantics of first-order logic (FOL) can be described in the meta-language of higher-order logic (HOL). Using HOL one can prove key properties of FOL such as soundness and completeness. Furthermore, one can prove sentences in FOL valid using the formalized FOL semantics. To aid in the construction of the proof an interactive proof assistant like Isabelle can be used. The proof assistant can even automate simple proofs using the formalized FOL semantics.
|Number of pages||1|
|Publication status||Published - 2015|
|Event||LOGICA 2015 - 29th Annual International Symposia Devoted to Logic - Hejnice Monastery, Hejnice, Czech Republic|
Duration: 15 Jun 2015 → 19 Jun 2015
Conference number: 29
|Conference||LOGICA 2015 - 29th Annual International Symposia Devoted to Logic|
|Period||15/06/2015 → 19/06/2015|