Meta-Logical Reasoning in Higher-Order Logic

Research output: Contribution to conferencePosterResearchpeer-review

495 Downloads (Pure)

Abstract

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
http://logika.flu.cas.cz/en/logica-2015/logica-20152

Conference

ConferenceLOGICA 2015 - 29th Annual International Symposia Devoted to Logic
Number29
LocationHejnice Monastery
Country/TerritoryCzech Republic
CityHejnice
Period15/06/201519/06/2015
Internet address

Fingerprint

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

Cite this