## Monotonox

swMATH ID: | 10406 |

Software Authors: | Claessen, Koen; Lillieström, Ann; Smallbone, Nicholas |

Description: | 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. |

Homepage: | http://link.springer.com/chapter/10.1007%2F978-3-642-22438-6_17 |

Related Software: | HOL Light; TPTP; HOL; Kodkod; Isabelle/HOL; ML; Nitpick; Isabelle; SPASS+T; Why3; Hotel Key Card; ETPS; SystemOnTPTP; E Theorem Prover; SmallCheck; QuickCheck; Sledgehammer; Isabelle/jEdit; Isabelle/ZF; z3 |

Referenced in: | 4 Publications |

all
top 5

### Referenced by 8 Authors

3 | Blanchette, Jasmin Christian |

1 | Bulwahn, Lukas |

1 | Claessen, Koen |

1 | Krauss, Alexander |

1 | Lillieström, Ann |

1 | Nipkow, Tobias |

1 | Paskevich, Andrei |

1 | Smallbone, Nicholas |

### Referenced in 1 Serial

1 | Journal of Automated Reasoning |

### Referenced in 2 Fields

4 | Computer science (68-XX) |

2 | Mathematical logic and foundations (03-XX) |