Use of logical models for proving operational termination in general logics





Publicado en

Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017)

Licencia Creative Commons


A declarative programming language is based on some logic L and its operational semantics is given by a proof calculus which is often presented in a natural deduction style by means of inference rules. Declarative programs are theories S of L and executing a program is proving goals G in the inference system I(S) associated to S as a particularization of the inference system of the logic. The usual soundness assumption for L implies that every model M of S also satisfies G. In this setting, the operational termination of a declarative program is quite naturally defined as the absence of infinite proof trees in the inference system I(S). Proving operational termination of declarative programs often involves two main ingredients: (i) the generation of logical models M to abstract the program execution (i.e., the provability of specific goals in I(S)), and (ii) the use of well-founded relations to guarantee the absence of infinite branches in proof trees and hence of infinite proof trees, possibly taking into account the information about provability encoded by M. In this paper we show how to deal with (i) and (ii) in a uniform way. The main point is the synthesis of logical models where well-foundedness is a side requirement for some specific predicate symbols.


Acerca de Lucas, Salvador

Palabras clave

Abstraction, Logical Models, Operational Termination
Página completa del ítem
Notificar un error en este resumen
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX