Tree-Based Heuristics in Modal Theorem Proving (abstract)

C. Areces, R. Gennari, J. Heguiabehere, and M. de Rijke. Tree-Based Heuristics in Modal Theorem Proving (abstract). In Proceedings BNAIC'01, pp. 31–32, 2001.

Download

[pdf] 

Abstract

We describe a new relational translation of modal formulas into first-order formulas. The key idea underlying the improvement is to encode a very strong form of the tree model property in the translation. Using our tree- based heuristics, we have consistently seen improvements, both in terms of the number of clauses generated and in terms of CPU time used. Our ongoing work is aimed at exploring the behavior of our heuristics in larger parts of the problem space, and at encoding weaker forms of the tree model property to boost the performance of resolution provers on input from different modal logics, such as K4, S4, and temporal logic.

BibTeX

@InProceedings{Areces2001g,
  author =       "C. Areces and R. Gennari and J. Heguiabehere and M. de
                 Rijke",
  booktitle =    "Proceedings BNAIC'01",
  title =        "Tree-Based Heuristics in Modal Theorem Proving
                 (abstract)",
  year =         "2001",
  abstract =     "We describe a new relational translation of modal
                 formulas into first-order formulas. The key idea
                 underlying the improvement is to encode a very strong
                 form of the tree model property in the translation.
                 Using our tree- based heuristics, we have consistently
                 seen improvements, both in terms of the number of
                 clauses generated and in terms of CPU time used. Our
                 ongoing work is aimed at exploring the behavior of our
                 heuristics in larger parts of the problem space, and at
                 encoding weaker forms of the tree model property to
                 boost the performance of resolution provers on input
                 from different modal logics, such as K4, S4, and
                 temporal logic.",
  pages =        "31--32",
}