@INPROCEEDINGS{GanzingerMeyerWeidenbach-97-cade,                  
        AUTHOR             = {Ganzinger, H. and Meyer, Chr. and Weidenbach, Chr.},
        TITLE              = {Soft typing for ordered resolution},
	BOOKTITLE          = {Automated Deduction --- CADE'14},
        PUBLISHER       = {Springer-Verlag},
        SERIES          = {Lecture Notes in Computer Science},
        ADDRESS         = {Berlin},
        VOLUME             = {1249},
        PAGES           ={321--335},
        YEAR               = {1997},
        abstract = {We propose a variant of ordered resolution with semantic restrictions
based on interpretations which are identified by the given atom ordering
and selection function. Techniques for effectively approximating validity (satisfiability)
in these interpretations are presented. They are related to methods of
soft typing for programming languages.
The framework is shown to be strictly more general than certain previously
introduced approaches.
Implementation of some of our techniques
in the SPASS prover has lead to encouraging experimental results.
},

}