Tree-based heuristics in modal theorem proving
Carlos Areces, Rosella Gennari, J.M. Heguiabehere, Maarten de Rijke · UvA-DARE (University of Amsterdam) · 2000
. 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. 1 Introduction Modal and modal-like logics such as temporal logic, description logic, and feature logic, have had a long history in artificial intelligence, both as an area of foundational research and as a source for useful representation formalisms and reasoning methods [6, 9]. The recent advent of agent-based technologies has dramatically increased the need for efficient automated reasoning methods for modal logic [6]. Broadly speaking, there are three general strategies for modal theorem proving: (1) develop purpose-built calculi and tools; (2) translate modal problems into automata-theoretic problem...