Skip to main content

Inference for Annotated Logics over Distributive Lattices

  • Conference paper
  • First Online:
Foundations of Intelligent Systems (ISMIS 2002)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2366))

Included in the following conference series:

Abstract

The inference rule ℧-resolution was introduced in [18] as a technique for developing an SLD-style query answering procedure for the logic programming subset of annotated logic. This paper explores the properties of ℧-resolution in the general theorem proving setting. In that setting, it is shown to be complete and to admit a linear restriction. Thus ℧-resolution is amenable to depth-first control strategies that require little memory. An ordering restriction is also described and shown to be complete, providing a promising saturation-based procedure for annotated logic. The inference rule essentially requires that the lattice of truth values be ordinary. Earlier investigations left open the question of whether all distributive lattices are ordinary; this is answered in the affirmative here.

This research was supported in part by the National Science Foundation under grant CCR-9731893.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bachmair, L. and Ganzinger, H., Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  2. Blair, H.A. and Subrahmanian, V.S., Paraconsistent logic programming, Theoretical Computer Science 68, 135–154, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  3. Calmet, J., Jekutsch, S., Kullmann, P., and Schü, J., A system for the integration of heterogeneous information sources, Proc. ISMIS, 1997.

    Google Scholar 

  4. Calmet, J. and Kullmann, P., Meta web search with KOMET, Proceedings of the IJCAI-99 Workshop on Intelligent Information Integration, Stockholm, July, 1999.

    Google Scholar 

  5. Carnielli, W.A., Systematization of finite many-valued logics through the method of tableaux. J. of Symbolic Logic 52(2):473–493, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  6. Davey, B.A. and Priestley, H.A., Introduction to Lattices and Order, Cambridge Math, 1990.

    Google Scholar 

  7. Doherty, P., NML3 —A Non-Monotonic Formalism with Explicit Defaults, Linköping Studies in Sci. and Tech., Diss. 258, Dept. of CIS, Linköping University, 1991.

    Google Scholar 

  8. Fitting, M., First-order modal tableaux, J. Automated Reasoning 4:191–213, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  9. Hähnle, R., Automated Deduction in Multiple-Valued Logics, International Series of Monographs on Computer Science, vol. 10. Oxford University Press, 1994.

    Google Scholar 

  10. Hähnle, R., Tableaux methods for many-valued logics, Handbook of Tableau Methods (M. d’Agostino, D. Gabbay, R. Hähnle and J. Posegga eds.), Kluwer, Dordrecht, 1999.

    Google Scholar 

  11. Hähnle, R. and Escalada-Imaz, G., Deduction in many-valued logics: a survey, Mathware & Soft Computing, IV(2), 69–97, 1997.

    Google Scholar 

  12. Joyner, W.H., Resolution strategies as decision procedures, JACM 23(1), 398–417, 1976.

    Article  MATH  MathSciNet  Google Scholar 

  13. Kifer, M. and Li, A., On the semantics of rule-based expert systems with uncertainty, Proc. the 2nd Int. Conf. on Database Theory, 102–117, 1988.

    Google Scholar 

  14. Kifer, M. and Lozinskii, E.L., RI: a logic for reasoning in inconsistency, Proceedings of the Fourth Symposium of Logic in Computer Science, Asilomar, 253–262, 1989.

    Google Scholar 

  15. Kifer, M. and Lozinskii, E., A logic for reasoning with inconsistency, JAR 9, 179–215, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  16. Kifer, M. and Subrahmanian, V.S., Theory of generalized annotated logic programming and its applications, J. of Logic Programming 12, 335–367, 1992.

    Article  MathSciNet  Google Scholar 

  17. Kowalski, R. and Hayes, P.J. Semantic trees in automatic theorem proving. In Machine Intelligence 4, 87–101, Edinburgh University Press, 1969. Reprinted in [29].

    MathSciNet  MATH  Google Scholar 

  18. Leach, S.M., Lu, J.J., Murray, N.V., and Rosenthal, E., ℧-resolution: an inference for regular multiple-valued logics,. Proc. JELIA’98, IBFI Schloss Dagstuhl, Lecture Notes in Artificial Intelligence 1489, Springer-Verlag, 154–168, 1998.

    Google Scholar 

  19. Leach, S.M., Lu, J.J., Murray, N.V., and Rosenthal, E., ℧-resolution and hybrid knowledge bases, Journal of The Franklin Institute (Special issue on AI), 338(5), 583–600, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  20. Lu, J.J., Henschen, L.J., Subrahmanian, V.S., and da Costa, N.C.A., Reasoning in paraconsistent logics, Automated Reasoning: Essays in Honor of Woody Bledsoe (R. Boyer ed.), Kluwer Academic, 181–210, 1991.

    Google Scholar 

  21. Lu, J.J., Nerode, A., and Subrahmanian, V.S. Hybrid Knowledge Bases, IEEE Transactions on Knowledge and Data Engineering, 8(5):773–785, 1996.

    Article  Google Scholar 

  22. Lu, J.J., Murray, N.V., and Rosenthal, E., A Framework for Automated Reasoning in Multiple-Valued Logics, J. of Automated Reasoning 21,1 39–67, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  23. Lu, J.J., Murray, N.V., and Rosenthal, E., A foundation for hybrid knowledge bases, Proc. 19 th Int. Conf. on Foundations of Software Technology & Theoretical Computer Science, Chennai, India, Lecture Notes in Computer Science 1738, Springer-Verlag, 155–167, 1999.

    Chapter  Google Scholar 

  24. Lu, J.J., Murray, N.V., and Rosenthal, E., Annotated hyperresolution for non-Horn regular multiple-valued logics, Proc. ISMIS-2000, Lecture Notes in Artificial Intelligence 1932, Springer-Verlag, 301–310.

    Google Scholar 

  25. Lu, J.J., Murray, N.V., and Rosenthal, E., Non-Horn clause annotated logic deduction over distributive lattice truth domains, Tech. Report TR 01-3, SUNY at Albany, 2001.

    Google Scholar 

  26. Lu, J.J., Murray, N.V., Radjavi, H., Rosenthal, E., and Rosenthal, P. Search strategies for annotated logics over distributive lattices, Tech. Report TR 02-1, SUNY at Albany, 2002.

    Google Scholar 

  27. Murray, N.V. and Rosenthal, E., Adapting classical inference techniques to multiple-valued logics using signed formulas, Fundamenta Informaticae 21:237–253, 1994.

    MATH  MathSciNet  Google Scholar 

  28. Reynolds, J. Unpublished seminar notes, Stanford University, Palo Alto, CA, 1966.

    Google Scholar 

  29. Siekmann, J. and Wrightson, G., editors. Automation of Reasoning: Classical Papers in Computational Logic 1967-1970, volume 2. Springer-Verlag, 1983.

    Google Scholar 

  30. Subrahmanian, V.S., On the Semantics of Quantitative Logic Programs, in: Proceedings of the 4th IEEE Symposium on Logic Programming, Computer Society Press, 1987.

    Google Scholar 

  31. Subrahmanian, V.S., Paraconsistent Disjunctive Databases, Theoretical Computer Science, 93, 115–141, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  32. Thirunarayan, K. and Kifer, M., A Theory of Nonmonotonic Inheritance Based on Annotated Logic, Artificial Intelligence, 60(1):23–50, 1993.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lu, J.J., Murray, N.V., Radjavi, H., Rosenthal, E., Rosenthal, P. (2002). Inference for Annotated Logics over Distributive Lattices. In: Hacid, MS., Raś, Z.W., Zighed, D.A., Kodratoff, Y. (eds) Foundations of Intelligent Systems. ISMIS 2002. Lecture Notes in Computer Science(), vol 2366. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48050-1_32

Download citation

  • DOI: https://doi.org/10.1007/3-540-48050-1_32

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43785-7

  • Online ISBN: 978-3-540-48050-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics