Paper: Paramodulation without Duplication (at LICS 1995)

Authors: Christopher Lynch

Abstract

The resolution (and paramodulation) inference systems are theorem proving procedures for first-order logic (with equality), but they can run exponentially long for subclasses which have polynomial time decision procedures, as in the case of SLD resolution and the Knuth-Bendix completion procedure, both in the ground case. Specialized methods run in polynomial time, but have not been extended to the full first-order case. We show a form of Paramodulation which does not copy literals, which runs in polynomial time for the ground case of the following four subclasses: Horn Clauses with any selection rule, any set of Unit Equalities (this includes Completion), Equational Horn Clauses with a certain selection rule, and Conditional Narrowing.

BibTeX

  @InProceedings{Lynch-Paramodulationwitho,
    author = 	 {Christopher Lynch},
    title = 	 {Paramodulation without Duplication},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)},
    year =	 {1995},
    month =	 {June}, 
    pages =      {167--177},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }