×

On a semantic subsumption test. (English) Zbl 1108.03307

Baader, Franz (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14–18, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25236-3/pbk). Lecture Notes in Computer Science 3452. Lecture Notes in Artificial Intelligence, 142-153 (2005).
Summary: We observe, that subsumption of clauses (in the language of first-order logic), so far understood as a syntactic notion, can also be defined by semantical means. Subsumption is NP-complete and testing subsumption takes roughly half of the running time of a typical first order resolution-based theorem prover. We also give some experimental evidence, that replacing syntactic indexing for subsumption by our semantic Monte-Carlo technique can, in some situations, significantly decrease the cost of subsumption testing.
Finally, we provide some evidence that a similar semantic idea can be probably successfully used for testing for AC matching, which is another NP-complete problem whose millions of instances are being solved by theorem provers.
For the entire collection see [Zbl 1070.68001].

MSC:

03B35 Mechanization of proofs and logical operations
68Q25 Analysis of algorithms and problem complexity
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

TPTP; OTTER; VAMPIRE; EQP
PDFBibTeX XMLCite
Full Text: DOI