Goals in the prepositional Horn⊃ language are monotone Boolean circuits

Abstract

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. Restricted to the propositional setting of this language, we prove that any goal in Horn⊃ can be translated into a monotone Boolean circuit which is linear in the size of the goal. © Springer-Verlag Berlin Heidelberg 2005.