Logic in Computer Science (LICS 1999)

Paper: A Superposition Decision Procedure for the Guarded Fragment with Equality (at LICS 1999)

Authors: H. Ganzinger H. de Nivelle

Abstract

We give a new decision procedure for the guarded fragment with equality. The procedure is based on resolution with superposition. We argue that this method will be more useful in practice than methods based on the enumeration of certain finite structures. It is surprising to see that one does not need any sophisticated simplification and redundancy elimination method to make superposition terminate on the class of clauses that is obtained from the clausification of guarded formulas. Yet the decision procedure obtained is optimal with regard to time complexity. We also show that the method can be extended to the loosely guarded fragment with equality.

BibTeX

  @InProceedings{GanzingerNivelle-ASuperpositionDecis,
    author = 	 {H. Ganzinger and H. de Nivelle},
    title = 	 {A Superposition Decision Procedure for the Guarded Fragment with Equality},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {295--304},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }