[isabelle] New AFP entry: Sound and Complete Sort Encodings for First-Order Logic

Sound and Complete Sort Encodings for First-Order Logic
Jasmin Christian Blanchette and Andrei Popescu

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.