Skip to main content
SpringerLink
Log in
Book cover

International Conference on Logic for Programming Artificial Intelligence and Reasoning

LPAR 2010: Logic for Programming, Artificial Intelligence, and Reasoning pp 202–216Cite as

Magically Constraining the Inverse Method Using Dynamic Polarity Assignment

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6397))

Abstract

Given a logic program that is terminating and mode-correct in an idealised 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 characterise 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 characterise 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 generalised to larger fragments of logic.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. of Logic and Computation 2(3), 297–347 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  2. Apt, K.R., Marchiori, E.: Reasoning about prolog programs from modes through types to assertions. Formal Aspects of Computing 6(A), 743–764 (1994)

    Article  MATH  Google Scholar 

  3. Beeri, C., Ramakrishnan, R.: On the power of magic. J. of Logic Programming 10(1/2/3&4), 255–299 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  4. Chaudhuri, K.: The Focused Inverse Method for Linear Logic. PhD thesis, Carnegie Mellon University, Technical report CMU-CS-06-162 (2006)

    Google Scholar 

  5. Chaudhuri, K.: Focusing strategies in the sequent calculus of synthetic connectives. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 467–481. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Chaudhuri, K.: Classical and intuitionistic subexponential logics are equally expressive. In: Veith, H. (ed.) CSL 2010. LNCS, vol. 6247, pp. 185–199. Springer, Heidelberg (2010)

    Google Scholar 

  7. Chaudhuri, K., Pfenning, F.: A focusing inverse method theorem prover for first-order linear logic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 69–83. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  8. Chaudhuri, K., Pfenning, F., Price, G.: A logical characterization of forward and backward chaining in the inverse method. J. of Automated Reasoning 40(2-3), 133–177 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  9. Degtyarev, A., Voronkov, A.: The inverse method. In: Handbook of Automated Reasoning, pp. 179–272. Elsevier and MIT Press (2001)

    Google Scholar 

  10. Donnelly, K., Gibson, T., Krishnaswami, N., Magill, S., Park, S.: The inverse method for the logic of bunched implications. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 466–480. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Heilala, S., Pientka, B.: Bidirectional decision procedures for the intuitionistic propositional modal logic IS4. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 116–131. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. Howe, J.M.: Proof Search Issues in Some Non-Classical Logics. PhD thesis, U. of St Andrews, Research Report CS/99/1 (1998)

    Google Scholar 

  13. Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science 410(46), 4747–4768 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  14. Liang, C., Miller, D.: A unified sequent calculus for focused proofs. In: LICS 24, pp. 355–364 (2009)

    Google Scholar 

  15. Mascellani, P., Pedreschi, D.: The declarative side of magic. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond. LNCS (LNAI), vol. 2408, pp. 83–108. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  16. McLaughlin, S., Pfenning, F.: Imogen: Focusing the polarized focused inverse method for intuitionistic propositional logic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 174–181. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Miller, D., Nigam, V.: Incorporating tables into proofs. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 466–480. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Miller, D., Saurin, A.: From proofs to focused proofs: a modular proof of focalization in linear logic. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 405–419. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  19. Ullman, J.D.: Principles of Database and Knowledge-base Systems, Volume II: The New Techniques. In: Principles of Computer Science. Computer Science Press, Rockville (1989)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Saclay, France

    Kaustuv Chaudhuri

Authors
  1. Kaustuv Chaudhuri
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Computersprachen 185.2, Theory and Logic Group, TU Wien, Favoritenstraße 9-11, A-1040, Vienna, Austria

    Christian G. Fermüller

  2. School of Computer Science, University of Manchester, Oxford Road, Kilburn Building, M13 9PL, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chaudhuri, K. (2010). Magically Constraining the Inverse Method Using Dynamic Polarity Assignment. In: Fermüller, C.G., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science, vol 6397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16242-8_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16242-8_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16241-1

  • Online ISBN: 978-3-642-16242-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation