Abstract
The inference rule ℧-resolution for regular multiple-valued logics is developed. One advantage of ℧-resolution is that linear, regular proofs are possible. That is, unlike existing deduction techniques, ℧-resolution admits input deductions (for Horn sets) while maintaining regular signs. More importantly, ℧-resolution proofs are at least as short as proofs for definite clauses generated by the standard inference techniques—annotated resolution and reduction—and pruning of the search space occurs automatically.
This research was supported in part by the National Science Foundation under grants CCR-9731893, CCR-9404338 and CCR-9504349.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baaz, M., and Fermüller, C.G., Resolution-based theorem proving for many-valued logics, J. of Symbolic Computation, 19(4):353–391, 1995.
Blair, H.A. and Subrahmanian, V.S., Paraconsistent Logic Programming, Theoretical Computer Science, 68:135–154, 1989.
Carnielli, W.A., Systematization of finite many-valued logics through the method of tableaux. J. of Symbolic Logic 52(2):473–493, 1987.
Davey, B.A., and Priestley, H.A., Introduction to Lattices and Order, Cambridge Mathematical Textbooks, (1990)
Doherty, P., NML3 — A Non-Monotonic Formalism with Explicit Defaults. Linköping Studies in Science and Technology. Dissertations No. 258. Department of Computer and Information Science, Linköping University, 1991.
Fitting, M., First-order modal tableaux, J. Automated Reasoning 4:191–213, 1988.
Ginsberg, M.L., Multivalued Logics, Readings in Non-Monotonic Reasoning, 251–255, 1987.
Hähnle, R., Automated Deduction in Multiple-Valued Logics, International Series of Monographs on Computer Science, vol. 10. Oxford University Press, 1994.
Hähnle, R., Short conjunctive normal forms in finitely-valued logics, J. of Logic and Computation, 4(6): 905–927, 1994.
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. To appear.
Hähnle, R. and Escalada-Imaz, G., Deduction in many-valued logics: a survey, Mathware & Soft Computing, IV(2), 69–97, 1997.
Kifer, M., and Li, A., On the Semantics of Rule-based Expert Systems with Uncertainty, Proceedings of the 2nd International Conference on Database Theory, 102–117, 1988.
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.
Kifer, M., and Subrahmanian, V.S., Theory of generalized annotated logic programming and its applications, the J. of Logic Programming 12, 335–367, 1992.
Kifer, M., and Lozinskii, E., A logic for reasoning with inconsistency, J. of Automated Reasoning 9, 179–215, 1992.
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.
Lu, J.J., Nerode, A. and Subrahmanian, V.S. Hybrid Knowledge Bases, IEEE Transactions on Knowledge and Data Engineering, 8(5):773–785, 1996.
Lu, J.J., Murray, N.V., and Rosenthal, E., A Framework for Automated Reasoning in Multiple-Valued Logics, J. of Automated Reasoning 21:39–67, 1998. To appear.
Lu, J.J., Logic programming with signs and annotations, J. of Logic and Computation, 6(6):755–778, 1996.
Murray, N.V., and Rosenthal, E., Adapting classical inference techniques to multiple-valued logics using signed formulas, Fundamenta Informaticae 21:237–253, 1994.
Subrahmanian, V.S., On the Semantics of Quantitative Logic Programs, in: Proceedings of the 4th IEEE Symposium on Logic Programming, Computer Society Press, 1987.
Subrahmanian, V.S., Paraconsistent Disjunctive Databases, Theoretical Computer Science, 93, 115–141, 1992.
Thirunarayan, K., and Kifer, M., A Theory of Nomonotonic Inheritance Based on Annotated Logic, Artificial Intelligence, 60(1):23–50, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leach, S.M., Lu, J.J., Murray, N.V., Rosenthal, E. (1998). ℧-Resolution: An Inference Rule for Regular Multiple-Valued Logics. In: Dix, J., del Cerro, L.F., Furbach, U. (eds) Logics in Artificial Intelligence. JELIA 1998. Lecture Notes in Computer Science(), vol 1489. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49545-2_11
Download citation
DOI: https://doi.org/10.1007/3-540-49545-2_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65141-3
Online ISBN: 978-3-540-49545-1
eBook Packages: Springer Book Archive