Applied logic for computer scientists : Computational deduction and formal proofs.