×

zbMATH — the first resource for mathematics

Translating propositional extended conjunctions of Horn clauses into Boolean circuits. (English) Zbl 1191.68148
Summary: Horn\(^{\supset}\) 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 way of structuring programs in logic programming. We are interested in finding correct and efficient translations from Horn\(^{\supset}\) 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\(^{\supset}\) 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.
MSC:
68N17 Logic programming
68N15 Theory of programming languages
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Arruabarrena, R.; Lucio, P.; Navarro, M., A strong logic programming view for static embedded implications, (), 56-72 · Zbl 0948.68031
[2] Baldoni, M.; Giordano, L.; Martelli, A., Translating a modal language with embedded implication into Horn clause logic, ()
[3] Bugliesi, M.; Lamma, E.; Mello, P., Modularity in logic programming, Journal of logic programming, 19-20, 443-502, (1994)
[4] Gabbay, D.M., N-prolog: an extension of prolog with hypothetical implications. II. logical foundations and negation as failure, Journal of logic programming, 2, 4, 251-283, (1985) · Zbl 0595.68004
[5] Gaintzarain, J.; Hermo, M.; Navarro, M., Goals in the propositional Horn\({}^\supset\) language are monotone Boolean circuits, (), 376-386 · Zbl 1156.68326
[6] Giordano, L.; Martelli, A., Structuring logic programs: A modal approach, Journal of logic programming, 21, 59-94, (1994) · Zbl 0812.68065
[7] Giordano, L.; Martelli, A.; Rossi, G., Extending Horn clause logic with implication goals, Theoretical computer science, 95, 43-74, (1992) · Zbl 0754.68109
[8] Lucio, P., Structured sequent calculi for combining intuitionistic and classical first-order logic, (), 88-104 · Zbl 0961.03008
[9] Meseguer, J., Multiparadigm logic programming, (), 158-200
[10] Miller, D., A logical analysis of modules in logic programming, Journal of logic programming, 6, 79-108, (1989) · Zbl 0681.68022
[11] Miller, D.; Nadathur, G.; Pfenning, F.; Scedrov, A., Uniform proofs as a foundation for logic programming, Annals of pure and appl. logic, 51, 125-157, (1991) · Zbl 0721.03037
[12] L. Monteiro, A. Porto, Contextual logic programming, in: Proc. 6th International Conf. on Logic Programming, 1989, pp. 284-299.
[13] Y. Moscowitz, E. Shapiro, Lexical logic programs, in: Proc. 8th International Conf. on Logic Programming, 1991, pp. 349-363.
[14] M. Navarro, From modular horn programs to flat ones: a formal proof for the propositional case, in: Proc. of ISIICT 2004, Int. Symp. on Innovation in Information and Communication Technology, Amman, Jordan. April 2004. Technical Report UPV-EHU/ LSI/ TR 01-2004.
[15] Papadimitriou, Christos H., Computational complexity, (1995), Addison-Wesley Publishing Company, Inc. · Zbl 0833.68049
[16] Pasarella, E.; Orejas, F.; Pino, E.; Navarro, M., A transformational semantics of static embedded implications, (), 113-146 · Zbl 1156.68329
[17] Wegener, I., Relating monotone formula size and monotone depth of Boolean functions, Information processing letters, 16, 41-42, (1983) · Zbl 0504.94035
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.