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.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten