Translating propositional extended conjunctions of Horn clauses into Boolean circuits