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 language | English |
|---|---|
| Publication date | 2015 |
| 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 http://logika.flu.cas.cz/en/logica-2015/logica-20152 |
Conference
| Conference | LOGICA 2015 - 29th Annual International Symposia Devoted to Logic |
|---|---|
| Number | 29 |
| Location | Hejnice Monastery |
| Country/Territory | Czech Republic |
| City | Hejnice |
| Period | 15/06/2015 → 19/06/2015 |
| Internet address |