Foundations of Paraconsistent Resolution

• Autorzy: Kamide N.
• Języki publikacji: EN

Abstrakty

EN

An extended first-order predicate sequent calculus PLK with two kinds of negation is introduced as a basis of a new resolution calculus PRC (paraconsistent resolution calculus) for handling the property of paraconsistency. Herbrand theorem, completeness theorem (with respect to a classical-like semantics) and cut-elimination theorem are proved for PLK. The correspondence between PLK and PRC is shown by using a faithful embedding of PLK into the sequent calculus LK for classical logic.

Słowa kluczowe

EN

paraconsistent resolution; sequent calculus; Herbrand theorem; completeness; cut elimination

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 71, nr 4
• Strony: 419--441
• Opis fizyczny: bibliogr. 44 poz.

Twórcy

autor

Kamide N.

• Department of Philosophy, Keio University, 2-15-45 Mita, Minatoku, Tokyo, 108-8345, Japan,

Bibliografia

• [1] Akama, S.: Tableaux for logic programming with strong negation, Lecture Notes in Computer Science, 1227, 1997, 31-42.
• [2] Alcântara, J., Damásio, C. V., and Pereira, L. M.: Paraconsistent logic programs, Lecture Notes in Computer Science, 2424, 2002, 345-356.
• [3] Alcântara, J., Damásio, C. V., and Pereira, L. M.: A declarative characterisation of disjunctive paraconsistent answer sets, Proceedings of the 16-th European Conference on Artificial Intelligence, ECAI'2004, Valencia, Spain, 2004, pp. 951-952, IOS Press.
• [4] Apt, K. R., and Bol, R. N.: Logic programming and negation: a survey, Journal of Logic Programming, 19, 20, 1994, 9-71.
• [5] Arieli, O., and Avron, A.: Reasoning with logical bilattices, Journal of Logic, Language and Information, 5, 1996, 25-63.
• [6] Arieli, O.: Paraconsistent declarative semantics for extended logic programs, Annals of Mathematics and Artificial Intelligence, 36 (4), 2002, 381-417.
• [7] Béziau, J.-Y.: The future of paraconsistent logic, Logical Studies, 2, 1999, (Online available).
• [8] Béziau, J.-Y.: S5 is a paraconsistent logic and so is first-order classical logic, Logical Studies, 9, 2002, (Online available).
• [9] Béziau, J.-Y.: Paraconsistent logic from a modal viewpoint, Journal of Applied Logic (in press).
• [10] Blair, H. A., and Subrahmanian, V. S.: Paraconsistent logic programming, Theoretical Computer Science, 68, 1989, 135-154.
• [11] Buss, S. R.: An introduction to proof theory, in: Handbook of Proof Theory (S. R. Buss, Ed.), Elsevier, 1998, 1-78.
• [12] Carnielli, W. A., Coniglio, M. E., and Marcos, J.: Logics of formal inconsistency, D. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, Vol. 14, 2004, pp. 1-124, Kluwer Academic Publishers.
• [13] da Costa, N. C. A., Béziau, J.-Y., and Bueno, O. A. S.: Aspects of paraconsistent logic, Bulletin of the IGPL, 3 (4), 1995, 597-614.
• [14] Damásio, C. V., and Pereira, L. M.: A survey of paraconsistent semantics for logic programs, In D. Gabbay and P. Smets (eds.), Handbook of Defeasible Reasoning and Uncertainty Management Systems, Vol. 2, 1998, pp. 241-320, Kluwer Academic Publisheres.
• [15] Došen, K.: Negation in the light of modal logic, In What is negation? (D. M. Gabbay and H.Wansing, Eds.), Kluwer Academic Publishers, 1999, 77-86.
• [16] Dovier, A., Pontelli, E., and Rossi, G.: Constructive negation and constraint logic programming with sets, New Generation Computing 19, 2001, 209-255.
• [17] Fages, F.: Constructive negation by pruning, Journal of Logic Programming, 1997, 85-118.
• [18] Fitting, M. C.: Negation as refutation, Proceedings of the fourth IEEE Symposium on logic in Computer Science, 1989, 63-70.
• [19] Fitting, M. C.: Bilattices and semantics of logic programming, Journal of Logic Programming, 11, 1991, 91-116.
• [20] Gabbay, D. M., and Sergot, M. J.: Negation as inconsistency. I, Journal of Logic Programming, 1, 1986, 1-35.
• [21] Gargov, G.: Knowledge, uncertainty and ignorance in logic: bilattices and beyond, Journal of Applied Non-Classical Logics, 9, 1999, 195-283.
• [22] Gelfond, M., and Lifschitz, V.: Classical negation in logic programming and disjunctive databases, New Generation Computing, 9, 1991, 365-385.
• [23] Hayashi, S.: Mathematical logic (in japanease), 177 pages, Corona Publishing Co. LTD. Tokyo Japan, 1989.
• [24] Herre, H., Jaspars, J., and Wagner, G.: Partial logics with two kinds of negation as a foundation for knowledge-based reasoning, In What is negation? (D. M. Gabbay and H. Wansing, Eds.), Kluwer Academic Publishers, 1999, 121-159.
• [25] Kamide, N.: Quantized linear logic, involutive quantales and strong negation, Studia Logica, 77, 2004, 355-385.
• [26] Kamide, N.: Combining soft linear logic and spatio-temporal operators, Journal of Logic and Computation, 14 (5), 2004, 625-650.
• [27] Kunen, K.: Negation in logic programming, Journal of Logic Programming, 4, 1987, 289-308.
• [28] Marcos, J.: Nearly every normal modal logic is paranormal, Research report, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisbon, Portugal, 2004, 16 pages.
• [29] Mascellani, P.: Using paraconsistent models in logic program verification, CLE e-Prints, 2(7), 2002, 15 pages, Proceedings of the workshop on paraconsistent logic (WoPaLo).
• [30] Miller, D.: A logical analysis of modules in logic programming, Journal of Logic Programming, 1989, 79-108.
• [31] Mints, G.: Gentzen-type systems and resolution rules. Part I. propositional logic, LNCS 417, Springer-Verlag, Berlin, 1988, 198-231.
• [32] Mints, G.: Resolution calculus for the first-order linear logic, Journal of Logic, Language and Information, 2, 1993, 59-83.
• [33] Nelson, D.: Constructible falsity, Journal of Symbolic Logic, 14, 1949, 16-26.
• [34] Ono, H.: Logic for information science (in japanease), Nihon Hyouron shya, 297 pages, 1994.
• [35] Pearce. D., and Wagner, G.: Logic programming with strong negation, in: P. Schroeder-Heister, Ed., Proceedings of Workshop on Extensions of Logic Programming, Lecture Notes in Artificial Intelligence 475, Springer-Verlag, 1990, 311-326.
• [36] Priest, G. and Routly, R.: Introduction : paraconsistent logics, Studia Logica, 43, 1982, 3-16.
• [37] Pynko, Alexej P.: Functional completeness and axiomatizability within Belnap's four-valued logic and its expansions, Journal of Applied Non-Classical Logics, 9, 1999, 61-105.
• [38] Robinson, J. A.: A machine-oriented logic based on the resolution principle, Journal of the ACM, 12 (1), 1965, 23-41.
• [39] Ruet, P., and Fages, F.: Combining explicit negation and negation by failure via Belnap's logic, Theoretical Computer Science, 171, 1997, 61-75.
• [40] Sakama, C.: Extended well-founded semantics for paraconsistent logic programs, In Fifth Generation Computer Systems, ICOT, pp. 592-599, 1992.
• [41] Sakama, C., and Inoue, K.: Paraconsistent stable semantics for extended disjunctive programs, Journal of Logic and Computation, 5(3), 1995, 265-285.
• [42] Takeuti, G.: Proof theory, North-Holland Publishing Company, 1975.
• [43] Wagner, G.: Logic programming with strong negation and inexact predicates, Journal of Logic and Computation, 1 (6), 1991, 835-859.
• [44] Wansing, H.: Displaying the modal logic of consistency, Journal of Symbolic Logic, 64, 1999, 1573-1590.