Translating propositional extended conjunctions of Horn clauses into Boolean circuits

Horn⊃ is a logic programming language which extends usual Horn clauses by adding intuitionistic implication in goals and clause bodies. This extension can be seen as a form 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, allow us suitable implementations of these kind 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 about the efficiency of the transformations are obtained in the three cases. Key words: Boolean circuits, Boolean formulas, Horn clauses, Horn⊃ clauses

• Type: Journal
• Year: 2010
• Where: TCS
• Authors: Joxe Gaintzarain, Montserrat Hermo, Paqui Lucio, Marisa Navarro
• Keywords: Boolean Formulas, Horn Clauses, TCS 2010, Theoretical Computer Science, Usual Horn Clauses