Logic for computer science foundations of automatic theorem proving - Gallier, Jean H. (Wiley, 1987)