# Monotonox

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.

Sorted by year (- 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)