Some results and experiments in programming techniques for propositional logic