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

Handling common transitive relations in first-order automated reasoning

Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Ann Lillieström (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
CEUR Workshop Proceedings (1613-0073). Vol. 1635 (2016), p. 11-23.
[Konferensbidrag, refereegranskat]

We present a number of alternative ways of handling transitive binary relations that commonly occur in first-order problems, in particular equivalence relations, total orders, and reflexive, transitive relations. We show how such relations can be discovered syntactically in an input theory. We experimentally evaluate different treatments on problems from the TPTP, using resolution-based reasoning tools as well as instance-based tools. Our conclusions are that (1) it is beneficial to consider different treatments of binary relations as a user, and that (2) reasoning tools could benefit from using a preprocessor or even built-in support for certain binary relations.

Nyckelord: Based reasonings, Built-in-support, Different treatments, Equivalence relations, First order problems, Transitive binary relations, Transitive relation



Denna post skapades 2016-12-20. Senast ändrad 2017-02-21.
CPL Pubid: 246382