Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria.

Leo Bachmair, Harald Ganzinger

Browse the full LPAR paper archive.