@INPROCEEDINGS{MPB-JH:ACAMC1991:simp, AUTHOR = "Maria Paola Bonacina and Jieh Hsiang", TITLE = "High performance simplification-based automated deduction", BOOKTITLE = "Transactions of the 9th U.S. Army Conference on Applied Mathematics and Computing", PUBLISHER = "Army Research Office", PAGES = "321--335", NUMBER = "92-1", MONTH = "June", YEAR = 1991}