[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

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:

  • 672 Accesses

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

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

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

  1. Department of Mathematics and Computer Science, Emory University Atlanta, GA, 30322, USA

    James J. Lu

  2. Department of Computer Science, State University of New York, Albany, NY, 12222, USA

    Neil V. Murray

  3. Department of Mathematics, Dalhousie University Halifax, Nova Scotia, B3H 3J5, Canada

    Heydar Radjavi

  4. Department of Mathematics, University of New Haven, West Haven, CT, 06516, USA

    Erik Rosenthal

  5. Department of Mathematics, University of Toronto, Toronto, Ontario, M5S 3G3, Canada

    Peter Rosenthal

Authors
  1. James J. Lu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Neil V. Murray
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Heydar Radjavi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Erik Rosenthal
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Peter Rosenthal
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. UFR d’Informatique, Université Claude Bernard Lyon I, 8, boulevard Niels Bohr, 69622, Villeurbanne Cedex, France

    Mohand-Saïd Hacid

  2. Dept. of Computer Science College of IT, University of North Carolina, Charlotte, NC, 28223, USA

    Zbigniew W. Raś

  3. Băt. L. Equipe de Recherche en Ingénierie des Connaissances, Université Lumière Lyon 2, 5, avenue Pierre Mendes-France, 69676, Bron Cedex, France

    Djamel A. Zighed

  4. LRI, Université Paris Sud, Băt. 490, 91405, Orsay Cedex, France

    Yves Kodratoff

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