Author name cluster

M. Martelli

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

I&C Journal 1995 Journal Article

Negation as Instantiation

A. Dipierro
M. Martelli
C. Palamidessi

We propose a new negation rule for logic programming which derives existentially closed negative literals, and we define a version of completion for which this rule is sound and complete. The rule is called "Negation As Instantiation" (NAI). According to it, a negated atom succeeds whenever all the branches of the SLD-tree for the atom either fail or instantiate the atom. The set of the atoms whose negation is inferred by the NAI rule is proved equivalent to the complement of Tc ↓ ω, where Tc is the immediate consequence operator extended to non-ground atoms (M. Falaschi et al. , 1989, Theoret. Comput, Sci. 69(3), 289-318). The NAI rule subsumes negation as failure on ground atoms, it excludes floundering, and can be efficiently implemented, We formalize this way of handling negation in terms of SLDNI-resolution (SLD-resolution with Negation as Instantiation). Finally, we amalgamate SLDNI-resolution and SLDNF-resolution, thus obtaining a new resolution procedure which is able to treat negative literals with both existentially quantified variables and free variables, and we prove its correctness.

Details DOI

I&C Journal 1993 Journal Article

A Model-Theoretic Reconstruction of the Operational Semantics of Logic Programs

M. Falaschi
G. Levi
M. Martelli
C. Palamidessi

In this paper we define a new notion or truth on Herbrand interpretations extended with variables which allows us to capture, by means of suitable models, various observable properties, such as the ground success set, the set of atomic consequences, and the computed answer substitutions. The notion of truth extends the classical one to account for non-ground formulas in the interpretations. The various operational semantics are all models. An ordering on interpretations is defined to overcome the problem that the intersection of a set of models is not necessarily a model. The set of interpretations with this partial order is shown to be a complete lattice, and the greatest lower bound of any set of models is shown to be a model. Thus there exists a least model, which is the least Herbrand model and therefore the ground success set semantics. Richer operational semantics are non-least models, which can, however, be effectively defined by fixpoint constructions. The model corresponding to the computed answer substitutions operational semantics is the most primitive one (the others can easily be obtained from it).

Details DOI

TCS Journal 1989 Journal Article

Declarative modeling of the operational behavior of logic languages

M. Falaschi
G. Levi
C. Palamidessi
M. Martelli

The paper defines a new declarative semantics for logic programs, which is based on interpretations containing (possibly) non-ground atoms. Two different interpretations are introduced and the corresponding models are defined and compared. The classical results on the Herbrand model semantics of logic programs are shown to hold in the new models too (i. e. existence of a minimal model, fixpoint characterization, etc.). With the new models, we have a stronger soundness and completeness result for SLD-resolution. In particular, one of the two models allows the set of computed answer substitutions to be characterized precisely.

Details DOI