Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Sort It Out with Monotonicity
Translating between Many-Sorted and Unsorted First-Order Logic
verfasst von : Koen Claessen, Ann Lillieström, Nicholas Smallbone
Erschienen in: Automated Deduction – CADE-23
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.