Magically Constraining the Inverse Method Using Dynamic Polarity Assignment

Kaustuv Chaudhuri 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : Given a logic program that is terminating and mode-correct in an idealized Prolog interpreter (i.e., in a top-down logic programming engine), a bottom-up logic programming engine can be used to compute exactly the same set of answers as the top-down engine for a given mode-correct query by rewriting the program and the query using the Magic Sets Transformation (MST). In previous work, we have shown that focusing can logically characterize the standard notion of bottom-up logic programming if atomic formulas are statically given a certain polarity assignment. In an analogous manner, dynamically assigning polarities can characterize the effect of MST without needing to transform the program or the query. This gives us a new proof of the completeness of MST in purely logical terms, by using the general completeness theorem for focusing. As the dynamic assignment is done in a general logic, the essence of MST can potentially be generalized to larger fragments of logic.
Type de document :
Communication dans un congrès
Christian Fermueller and Andrei Voronkov. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Oct 2010, Yogyakarta, Indonesia. Springer, 6397, pp.202--216, 2010, LNCS. 〈10.1007/978-3-642-16242-8_15〉
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00535948
Contributeur : Kaustuv Chaudhuri <>
Soumis le : dimanche 14 novembre 2010 - 14:36:49
Dernière modification le : jeudi 10 mai 2018 - 02:06:58
Document(s) archivé(s) le : mardi 15 février 2011 - 02:37:36

Fichiers

magassign.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Kaustuv Chaudhuri. Magically Constraining the Inverse Method Using Dynamic Polarity Assignment. Christian Fermueller and Andrei Voronkov. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Oct 2010, Yogyakarta, Indonesia. Springer, 6397, pp.202--216, 2010, LNCS. 〈10.1007/978-3-642-16242-8_15〉. 〈inria-00535948〉

Partager

Métriques

Consultations de la notice

282

Téléchargements de fichiers

178