Translating propositional extended conjunctions of Horn clauses into Boolean circuits

Abstract

Horn⊃ is a logic programming language that extends usual Horn clauses by adding intuitionistic implication in goals and clause bodies. This extension can be seen as a way of structuring programs in logic programming. We are interested in finding correct and efficient translations from Horn⊃ programs into some representation type that, preserving the signature, allows us suitable implementations of these kinds of programs. In this paper we restrict to the propositional setting of Horn⊃ and we study correct translations into Boolean circuits, i.e. graphs; into Boolean formulas, i.e. trees; and into conjunctions of propositional Horn clauses. Different results for the efficiencies of the transformations are obtained in the three cases.