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

Authors: Harald Ganzinger Hans 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{GanzingerdeNivelle-ASuperpositionDecis,
    author = 	 {Harald Ganzinger and Hans de Nivelle},
    title = 	 {A Superposition Decision Procedure for the Guarded Fragment with Equality},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999)},
    year =	 {1999},
    month =	 {July}, 
    pages =      {295--303},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }