Abstract: |
This is a formalization of the soundness and completeness properties
for various efficient encodings of sorts in unsorted first-order logic
used by Isabelle's Sledgehammer tool.
Essentially, the encodings proceed as follows:
a many-sorted problem is decorated with (as few as possible) tags or
guards that make the problem monotonic; then sorts can be soundly
erased.
The development employs a formalization of many-sorted first-order logic
in clausal form (clauses, structures and the basic properties
of the satisfaction relation), which could be of interest as the starting
point for other formalizations of first-order logic metatheory. |
BibTeX: |
@article{Sort_Encodings-AFP,
author = {Jasmin Christian Blanchette and Andrei Popescu},
title = {Sound and Complete Sort Encodings for First-Order Logic},
journal = {Archive of Formal Proofs},
month = jun,
year = 2013,
note = {\url{https://isa-afp.org/entries/Sort_Encodings.html},
Formal proof development},
ISSN = {2150-914x},
}
|