Feasible computational methods in the propositional calculus by Martin Davis, Hilary Putnam | Lex | Lex