Conference paper
Meta-Logical Reasoning in Higher-Order Logic
Department of Applied Mathematics and Computer Science, Technical University of Denmark1
Algorithms and Logic, Department of Applied Mathematics and Computer Science, Technical University of Denmark2
Language-Based Technology, Department of Applied Mathematics and Computer Science, Technical University of Denmark3
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.
Language: | English |
---|---|
Year: | 2015 |
Proceedings: | LOGICA 2015 - 29th Annual International Symposia Devoted to Logic |
Types: | Conference paper |
ORCIDs: | Villadsen, Jørgen , Schlichtkrull, Anders and Hess, Andreas Viktor |