Meta-Logical Reasoning in Higher-Order Logic

Jørgen Villadsen, Anders Schlichtkrull, Andreas Viktor Hess

Research output: Contribution to conferencePosterResearchpeer-review

643 Downloads (Pure)


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.
Original languageEnglish
Publication date2015
Number of pages1
Publication statusPublished - 2015
EventLOGICA 2015 - 29th Annual International Symposia Devoted to Logic - Hejnice Monastery, Hejnice, Czech Republic
Duration: 15 Jun 201519 Jun 2015
Conference number: 29


ConferenceLOGICA 2015 - 29th Annual International Symposia Devoted to Logic
LocationHejnice Monastery
Country/TerritoryCzech Republic
Internet address


Dive into the research topics of 'Meta-Logical Reasoning in Higher-Order Logic'. Together they form a unique fingerprint.

Cite this