Chang C-L and Lee R C-T, (1973). Symbolic Logic and Mechanical Theorem Proving, Academic Press.