A way of introducing simple (finite) set designations and operations as firstclass objects of an (unrestricted) logic programming language is discussed from both the declarative and the operational semantics viewpoint First, special set terms are added to definite Horn clause logic and an extended Herbrand Universe based on an axiomatic characterization of the kind of sets we are dealing with is defined accordingly. Moreover, distinguished predicates representing set membership and equality are added to the base language along with their negative counterparts (≠ and ∉). A new unification algorithm which can cope with set terms is developed and proved to terminate. Usual SLD resolution is modified so as to incorporate the new unification algorithm and to properly manage the distinguished predicates for set operations (in particular, conjunctions of atoms containing ≠ and ∉ are dealt with as constraints, first reduced to a canonical form through a suitable canonization algorithm). Finally, the application of the resulting language to the definition of Restricted Universal Quantifiers is discussed.

Embedding Finite Sets in a Logic Programming Language

DOVIER, Agostino;
1992

Abstract

A way of introducing simple (finite) set designations and operations as firstclass objects of an (unrestricted) logic programming language is discussed from both the declarative and the operational semantics viewpoint First, special set terms are added to definite Horn clause logic and an extended Herbrand Universe based on an axiomatic characterization of the kind of sets we are dealing with is defined accordingly. Moreover, distinguished predicates representing set membership and equality are added to the base language along with their negative counterparts (≠ and ∉). A new unification algorithm which can cope with set terms is developed and proved to terminate. Usual SLD resolution is modified so as to incorporate the new unification algorithm and to properly manage the distinguished predicates for set operations (in particular, conjunctions of atoms containing ≠ and ∉ are dealt with as constraints, first reduced to a canonical form through a suitable canonization algorithm). Finally, the application of the resulting language to the definition of Restricted Universal Quantifiers is discussed.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11390/687879
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? ND
social impact