Skip to main content
SpringerLink
Log in

Automatic theorem proving in paraconsistent logics: Theory and implementation

  • Conference paper
  • First Online:
10th International Conference on Automated Deduction (CADE 1990)

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

Included in the following conference series:

Abstract

Databases and knowledge bases may be inconsistent in many ways. However, a database that is inconsistent may, nonetheless, contain a great deal of useful information. Classical logic, however, would deem such a database as useless. Paraconsistent logics are a family of logics introduced by da Costa. A family of paraconsistent logics called annotated logics were proposed by Subrahmanian in [17]. Subsequently, these logics found use in reasoning about logic programs that contained inconsistent and/or erroneous information, as well as in the study of inheritance hierarchies and object oriented databases. However, no full-fledged study of automatic theorem proving in these logics has been carried out to date. In this paper, we develop a linear resolution style proof procedure for mechanical reasoning in these paraconsistent 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.

References

  1. N.D. Belnap. (1977) A Useful Four-Valued Logic, in G. Epstein and J.M. Dunn, eds. Modern Uses of Many-valued Logic, (eds. G. Epstein and J.M. Dunn), D. Reidel, pps. 8–37.

    Google Scholar 

  2. H. A. Blair and V.S. Subrahmanian. (1989) Paraconsistent Logic Programming, Theoretical Computer Science, 68, 1, pp 135–153.

    Google Scholar 

  3. H. A. Blair and V. S. Subrahmanian. (1988) Paraconsistent Foundations for Logic Programming, Journal of Non-Classical Logic, 5,2, pp 45–73.

    Google Scholar 

  4. C. L. Chang and R.C.T. Lee. (1973) Symbolic Logic and Mechanical Theorem Proving, Academic Press.

    Google Scholar 

  5. N.C.A. da Costa. (1974) On the Theory of Inconsistent Formal Systems, Notre Dame J. of Formal Logic, 15, pps 497–510.

    Google Scholar 

  6. N.C.A. da Costa and E.H. Alves. (1981) Relations between Paraconsistent logic and Many-valued logic, Bulletin of the Section of Logic, 10, pps 185–191.

    Google Scholar 

  7. N.C.A. da Costa, V.S. Subrahmanian and C. Vago. (1989) The Paraconsistent Logics PT, to appear in: Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, Vol. 37, 1991.

    Google Scholar 

  8. M. C. Fitting. (1989) Bilattices and the Theory of Truth, to appear in: Journal of Philosophical Logic.

    Google Scholar 

  9. M. C. Fitting. (1988) Logic Programming on a Topological Bilattice, Fundamenta Informatica, 11, pps 209–218.

    Google Scholar 

  10. M. C. Fitting. (1988) Bilattices and the Semantics of Logic Programming, to appear in: Journal of Logic Programming.

    Google Scholar 

  11. M. Kifer and T. Krishnaprasad. (1989) An Evidence Based Framework for a Theory of Inheritance, Proc. 11th International Joint Conf. on Artificial Intelligence, pp 1093–1098, Morgan-Kaufmann.

    Google Scholar 

  12. M. Kifer and E. Lozinskii. (1989) RI: A Logic for Reasoning with Inconsistency, LICS-89.

    Google Scholar 

  13. M. Kifer and J. Wu. (1989) A Logic for Object Oriented Logic Programming, Proc. 8th ACM Symp. on Principles of Database Systems, pp 379–393.

    Google Scholar 

  14. D. W. Loveland. (1970) A Linear Format for Resolution, Proc. IRIA Symp. on Automatic Demonstration, Lecture Notes in Mathematics, Springer, pps 147–162.

    Google Scholar 

  15. D. W. Loveland. (1972) A Unifying View of some Linear Herbrand Procedures, JACM, 19, pps 366–384.

    Google Scholar 

  16. J. Lu, V.S. Subrahmanian, and L. Henschen. (1990) An Improved Resolution Procedure for Paraconsistent Logics, submitted to AAAI-90.

    Google Scholar 

  17. V.S. Subrahmanian. (1987) On the Semantics of Quantitative Logic Programs, Proc. 4th IEEE Symposium on Logic Programming, Computer Society Press, Washington DC, pps 173–182.

    Google Scholar 

  18. V. S. Subrahmanian. (1988) Mechanical Proof Procedures for Many Valued Lattice Based Logic Programming, to appear in: Journal of Non-Classical Logic.

    Google Scholar 

  19. M.H. Van Emden. (1986) Quantitative Deduction and its Fixpoint Theory, Journal of Logic Programming, 4, 1, pps 37–53.

    Google Scholar 

  20. A. Visser. (1984) Four Valued Semantics and the Liar, J. of Philosophical Logic, 13, pps 181–212.

    Google Scholar 

  21. L. Wos, D. Carson, and G. Robinson, (1964) The Unit Preference Strategy in Theorem Proving, Proceedings of the AFIPS Conference 26, pp. 615–621.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Sao Paulo, Brazil

    Newton C. A. da Costa

  2. Northwestern University, Evanston, IL

    Lawrence J. Henschen & James J. Lu

  3. University of Maryland, College Park, MD

    V. S. Subrahmanian

Authors
  1. Newton C. A. da Costa
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lawrence J. Henschen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. James J. Lu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. V. S. Subrahmanian
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mark E. Stickel

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

da Costa, N.C.A., Henschen, L.J., Lu, J.J., Subrahmanian, V.S. (1990). Automatic theorem proving in paraconsistent logics: Theory and implementation. In: Stickel, M.E. (eds) 10th International Conference on Automated Deduction. CADE 1990. Lecture Notes in Computer Science, vol 449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52885-7_80

Download citation

  • DOI: https://doi.org/10.1007/3-540-52885-7_80

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-47171-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation