A Strong Logic Programming View for Static Embedded Implications

Abstract. A strong (L) logic programming language ([14, 15]) is given by two subclasses of formulas (programs and goals) of the underlying logic L, provided that: firstly, any program P (viewed as a L-theory) has a canonical model MP which is initial in the category of all its L-models; secondly, the L-satisfaction of a goal G in MP is equivalent to the L-derivability of G from P, and finally, there exists an effective (computable) proof-subcalculus of the L-calculus which works out for derivation of goals from programs. In this sense, Horn clauses constitute a strong (first-order) logic programming language. Following the methodology suggested in [15] for designing logic programming languages, an extension of Horn clauses should be made by extending its underlying first-order logic to a richer logic which supports a strong axiomatization of the extended logic programming language. A well-known approach for extending Horn clauses with embedded implications is the static scope prog...

• Type: Conference
• Year: 1999
• Where: FOSSACS
• Authors: R. Arruabarrena, Paqui Lucio, Marisa Navarro
• Keywords: FOSSACS 1999, Horn Clauses, Logic Programming Language, Software Engineering, first-order Logic