Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic. We present a novel analysis for sorted logic, which determines if a given sort is monotone. The domain of a monotone sort can always be extended with an extra element. We use this analysis to significantly improve well-known translations between unsorted and many-sorted logic, making use of the fact that it is cheaper to translate monotone sorts than non-monotone sorts. Many interesting problems are more naturally expressed in many-sorted first-order logic than in unsorted logic, but most existing highly-efficient automated theorem provers solve problems only in unsorted logic. Conversely, some reasoning tools, for example model finders, can make good use of sort-information in a problem, but most problems today are formulated in unsorted logic. This situation motivates translations in both ways between many-sorted and unsorted problems. We present the monotonicity analysis and its implementation in our tool Monotonox, and also show experimental results on the TPTP benchmark library.
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Blanchette, Jasmin Christian; Paskevich, Andrei: TFF1: the TPTP typed first-order form with rank-1 polymorphism (2013)
- Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias: Automatic proof and disproof in Isabelle/HOL (2011)
- Blanchette, Jasmin Christian; Krauss, Alexander: Monotonicity inference for higher-order formulas (2011)
- Claessen, Koen; Lillieström, Ann; Smallbone, Nicholas: Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic (2011)