Sound and Complete Sort Encodings for First-Order Logic.
Jasmin Christian Blanchette, Andrei Popescu · 2013
This is a formalization of the soundness and completeness proper- ties for various efficient encodings of sorts in unsorted first-order logic used by Isabelle’s Sledgehammer tool. The results are reported in [1, §2,3] and the formalization itself is presented in [2, §3–5]. 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 proofs rely on monotonicity criteria recently introduced by Claessen, Lilliestrom and Smallbone [3]. 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. References [1] J. C. Blanchette, S. Bohme, A. Popescu, and N. Smallbone. Encoding monomorphic and polymorphic types. In N. Piterman and S. Smolka, editors, TACAS 2013, volume 7795 of LNCS, pages 493–507. Springer, 2013. [2] J. C. Blanchette and A. Popescu. Mechanizing the metatheory of sledge- hammer. To be presented at FroCoS 2013. [3] K. Claessen, A. Lilliestrom, and N. Smallbone. Sort it out with monotonicity—Translating between many-sorted and unsorted first- order logic. In N. Bjorner and V. Sofronie-Stokkermans, editors, CADE- 23, volume 6803 of LNAI, pages 207–221. Springer, 2011.