A first order logic for logic programming

Moreno Navarro J J; Rodriguez Artalejo M

Repository | Book | Chapter

(1987) Mathematical logic and its applications, Dordrecht, Springer.

A first order logic for logic programming

J J Moreno Navarro, M Rodriguez Artalejo

pp. 303-314

Clark and Tärnlud⁴ have proposed a methodology for the specification, desing and verification of logic programs in the framework of first order logic. Their main idea is to derive the correctness of a logic program from its own clauses and suitable induction axioma on the data. This approach has been also advocated by Cartwright³ for the case of recursive, functional programs. He has contributed some theoretical results about the semantics of programs in nonstandard structures, using the notion of least definable fixpoint of the operator naturally associated to a given recursive program: This idea is also implicit in the independent work of Andréka, Németi and Sain¹ and Hajék⁷ about nonstandard dynamic logic for flowchart-like programs and regular programs; see also Sain¹⁰.

Publication details

DOI: 10.1007/978-1-4613-0897-3_22

Full citation:

Moreno Navarro, J.J. , Rodriguez Artalejo, M. (1987)., A first order logic for logic programming, in D. G. Skordev (ed.), Mathematical logic and its applications, Dordrecht, Springer, pp. 303-314.

This document is unfortunately not available for download at the moment.