Annotated Hyperresolution for Non-horn Regular Multiple-Valued Logics | SpringerLink
Skip to main content
Springer Nature Link
Log in

Annotated Hyperresolution for Non-horn Regular Multiple-Valued Logics

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

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

Included in the following conference series:

Abstract

This paper focuses on non-Horn formulas for the class of regular signed logics, also known as annotated logics. Resolution-based inference systems for these logics are not new, but most earlier work has concentrated on Horn formulas, to which the logic programming paradigm applies. Here a restriction of annotated resolution and reduction called annotated hyperresolution is introduced. The new rule is developed for arbitrary CNF formulas of regular signed logics and is shown to be complete.

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

Hähnle, R. and Escalada-Imaz, G. [7] have an excellent survey encompassing deduc- tive techniques for a wide class of MVL’s, including (properly) signed logics.

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. Anderson, R. and Bledsoe, W. A linear format for resolution with merging and a new technique for establishing completeness, J. ACM 17(3) (1970), 525–534.

    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. Davey, B.A., and Priestley, H.A., Introduction to Lattices and Order, Cambridge Mathematical Textbooks, (1990)

    Google Scholar 

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

    Google Scholar 

  5. Hähnle, R., Exploiting data dependencies in many-valued logics, Journal of Applied Non-Classical Logics 6(1): 49–69, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  6. Hähnle, R., Transformation between signed and classical clause logic, Proceedings of ISMVL-99, 248–255, 1999.

    Google Scholar 

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

    Google Scholar 

  8. Hähnle, R., Murray, N.V. and Rosenthal E., Some Remarks on Completeness, Connection Graph Resolution and Link Deletion, In Proceedings of the International Conference TABLEAUX’98-Analytic Tableaux and Related Methods, Oisterwijk, The Netherlands, May 1998. In Lecture Notes in Artificial Intelligence (H. de Swart, Ed.), Springer-Verlag, Vol. 1397, 172–186.

    Google Scholar 

  9. Kifer, M., and Lozinskii, E., A logic for reasoning with inconsistency, J. of Automated Reasoning 9, 179–215, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  10. 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 

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

    Article  MathSciNet  Google Scholar 

  12. Leach, S.M., Lu, J.J., Murray, N.V., and Rosenthal, E., 0-resolution: an inference for regular multiple-valued logics. Proceedings of JELIA’98. IBFI Schloss Dagstuhl (International Conference and Research Center for Computer Science), October 1998. In Lecture Notes in Artificial Intelligence, Springer-Verlag, Vol. 1489, 154–168.

    Google Scholar 

  13. 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 

  14. Murray, N.V., and Rosenthal, E., Improving tableaux deductions in multiple-valued logic, Proceedings of the 21st International Symposium on Multiple-Valued Logic, Victoria, B.C., Canada, May 26–29, 1991, 230–237.

    Google Scholar 

  15. 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 

  16. Robinson, J.A., Automatic deduction with hyper-resolution, International Journal of Computer Mathematics, 1 (1965), 227–234.

    MATH  Google Scholar 

  17. Sofronie-Stokkermans, V., On translation of finitely-valued logics to classical first-order logic, Proceedings of the 13th ECAI, 1998.

    Google Scholar 

  18. Sofronie-Stokkermans, V., Automated theorem proving by resolution for finitely-valued logics based on distributive lattices with operators, Multiple Valued Logic Journal, to appear.

    Google Scholar 

  19. 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 

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

    Article  MATH  MathSciNet  Google Scholar 

  21. 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 Computer Science, Bucknell University, Lewisburg, PA 17837, U.S.A.

    James J. Lu

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

    Neil V. Murray

  3. Department of Mathematics, University of New Haven, West Haven, 06516, CT

    Erik 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. Erik Rosenthal
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Computer Science, Polish Academy of Sciences, 01-237, Warsaw, Poland

    Zbigniew W. Raś

  2. Department of Computer Science, University of North Carolina, NC 28223, Charlotte, USA

    Zbigniew W. Raś

  3. Department of Science and Technology, Waseda University, 61-414, 3-4-1, Ohkubo, Shinjuku-ku, 169-8555, Tokyo, Japan

    Setsuo Ohsuga

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lu, J.J., Murray, N.V., Rosenthal, E. (2000). Annotated Hyperresolution for Non-horn Regular Multiple-Valued Logics. In: Raś, Z.W., Ohsuga, S. (eds) Foundations of Intelligent Systems. ISMIS 2000. Lecture Notes in Computer Science(), vol 1932. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-39963-1_32

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41094-2

  • Online ISBN: 978-3-540-39963-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation