A first-order language for expressing sharing and type properties of logic programs

In this paper we study a first-order language that allows to express and prove properties regarding the sharing of variables between non-ground terms and their types. The class of true formulas is proved to be decidable through a procedure of elimination of quantifiers and the language, with its proof procedure, is shown to have interesting applications in validation and debugging of logic programs. An interesting parallel is pointed out between the language of aliasing properties and the first order theories of Boolean algebras.