Tree-based Heuristics in Modal Theorem Proving

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.

• Type: Conference
• Year: 2000
• Where: ECAI
• Authors: Carlos Areces, Rosella Gennari, Juan Heguiabehere, Maarten de Rijke
• Keywords: Artificial Intelligence, ECAI 2000, Resolution-based first-order Theorem, So-called Relational Translations, Tree Model Property