CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Sort it out with monotonicity: translating between many-sorted and unsorted first-order logic

Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Ann Lillieström (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Nicholas Smallbone (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Lecture Notes in Computer Science, CADE'11 Proceedings of the 23rd international conference on Automated deduction (03029743). p. 207-221. (2011)
[Konferensbidrag, refereegranskat]

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.

Nyckelord: Automated theorem proving, First-order logic, Automated reasoning

Denna post skapades 2012-01-13. Senast ändrad 2013-09-28.
CPL Pubid: 152862


Läs direkt!

Lokal fulltext (fritt tillgänglig)

Länk till annan sajt (kan kräva inloggning)