Búsqueda avanzada

Directions of Operational Termination (Trabajo original)


A theory S in a logic supplied with an inference system is operationally terminating if no goal has an infinite well-formed proof tree. Well-formed proof trees are those which an interpreter would incrementally build when trying to solve a condition at a time from left to right. For this reason, infinite well-formed proof trees have a unique infinite branch which is called the spine. This paper introduces the notion of a directed proof tree for S and a set of formulas Δ, which we call a direction. Intuitively, a direction Δ is intended to collect formulas that are infinitely often used in the spine of an infinite well-formed proof tree (which is then called Δ-directed) due to the repeated use of some specific inference rules. Then we introduce the notion of Δ-directed operational termination of a theory as the absence of Δ-directed proof trees. This new notion permits the definition of different termination properties which can be useful to distinguish different computational behaviors. It also gives a new characterization of operational termination of a (finite) theory S as the conjunction of the Δ-directed operational termination of S for each direction Δ in a (finite) set of directions.

Palabras Clave:

General Logics - Operational Termination - Program Termination





Este artículo tiene una licencia de uso CreativeCommons - Reconocimiento (by)

Descarga el artículo haciendo click aquí.

Ver la referencia en formato Bibtex