IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Tenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1995)

Paper: Paramodulation without Duplication (at LICS 1995)

Authors: Christopher Lynch


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.


    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}

Last modified: 2017-04-0512:37
Andrzej Murawski