Automation of reasoning : classical papers on computational logic - Siekmann, Jorg H.; Wrightson, Graham (Symbolic computation, 1983)