Lettmann, Theodor, and Hans Kleine Büning. Propositional Logicf: Deduction and Algorithms. Cambridge Tracts in Theoretical Computer Science. Cambridge Univ. Press, 1999.