Carlos Areces, Rosella Gennari, Juan Heguiabehere, Maarten de Rijke
We use a strong form of the tree model property to boost the performance of resolution-based first-order theorem provers on the so-called relational translations of modal formulas. We provide both the mathematical underpinnings and experimental results concerning our improved translation method.
Keywords: automated reasoning, theorem proving, modal reasoning, tree model property
Citation: Carlos Areces, Rosella Gennari, Juan Heguiabehere, Maarten de Rijke: Tree-based Heuristics in Modal Theorem Proving. In W.Horn (ed.): ECAI2000, Proceedings of the 14th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2000, pp.199-203.