Working within a semantic framework for sequent calculi developed in a previous paper, we propose a couple of extensions to the concepts of correct answers and correct resultants which can be applied to the full first order logic. With respect to previous proposals, this is based on proof theory rather than model theory. We motivate our choice with several examples and we show how to use correct answers to reconstruct an abstraction which is widely used in the static analysis of logic programs, namely groundness. As an example of application, we present a prototypical top-down static interpreter for properties of groundness which works for the full intuitionistic first order logic.
Correct Answers for First Order Logic
AMATO, Gianluca
2000-01-01
Abstract
Working within a semantic framework for sequent calculi developed in a previous paper, we propose a couple of extensions to the concepts of correct answers and correct resultants which can be applied to the full first order logic. With respect to previous proposals, this is based on proof theory rather than model theory. We motivate our choice with several examples and we show how to use correct answers to reconstruct an abstraction which is widely used in the static analysis of logic programs, namely groundness. As an example of application, we present a prototypical top-down static interpreter for properties of groundness which works for the full intuitionistic first order logic.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
