@UNPUBLISHED{GanzingerNivelle-99-lics,
       AUTHOR = {Ganzinger, H. and De Nivelle, H.},
       TITLE = {A Superposition Decision Procedure for the Guarded Fragment with Equality},
       YEAR = {1999},
        BOOKTITLE          = {Proc.\ 14th IEEE Symposium on Logic in Computer Science},
	PAGES		   = {295--305},
	PUBLISHER          = {IEEE Computer Society Press},
       ABSTRACT = {
   We give a decision procedure for the
   guarded fragment with equality.
   The procedure is based on resolution with superposition. 
   The relevance of the guarded fragment lies in the fact
   that many modal logics can be translated into it. 
   In this way the guarded fragment acts as a framework explaining
   some of the nice properties of these modal logics.
   By constructing an implementable decision procedure for 
   the guarded fragments we define an effective procedure
   for deciding these modal logics. 
   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.
},
       URL = {\hgURL{~hg/pca.html#99LICS.2}}
}