Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas. - Atsushi Moritomo; Kiyoharu Hamaguchi; Toshinobu Kashiwabara (ATVA, 2004)