Abstract
This paper focuses on some automated reasoning issues for a kind of lattice-valued logic LP(X) based on lattice-valued algebra. Firstly some extended strategies from classical logic to LP(X) are investigated in order to verify the α-satisfiability of formulae in LP(X) while the main focus is given on the role of constant formula played in LP(X) in order to simply the verification procedure in the semantic level. Then, an α-lock resolution method in LP(X) is proposed and the weak completeness of this method is proved. The work will provide a support for the more efficient resolution based automated reasoning in LP(X).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Robinson, J.P.: A machine-oriented logic based on the resolution principle. J. ACM 12, 23–41 (1965)
Liu, X.H.: Resolution-Based Automated Reasoning. Academic Press, Beijing (1994) (in Chinese)
Wos, L.: Automated Reasoning: 33 Basic Research Problems. Prentice Hall, New Jersey (1988)
Wang, G.J., Zhou, H.J.: Introduction to Mathematical Logic and Resolution Principle, 2nd edn. Science Press, Beijing (2006)
Xu, Y.: Lattice implication algebra. J. Southwest Jiaotong University 1, 20–27 (1993)
Xu, Y., Ruan, D., Qin, K.Y., Liu, J.: Lattice-Valued Logic: An Alternative Approach to Treat Fuzziness and Incomparability. Springer, Berlin (2003)
Xu, Y., Ruan, D., Kerre, E.E., Liu, J.: α-resolution principle based on lattice-valued propositional logic LP(X). Information Science 130, 195–223 (2000)
Xu, Y., Ruan, D., Kerre, E.E., Liu, J.: α-resolution principle based on first-order lattice-valued logic LF(X). Information Science 132, 221–239 (2001b)
Ma, J., Li, W.J., Ruan, D., Xu, Y.: Filter-based resolution principle for lattice-valued propositional logic LP(X). Information Sciences 177, 1046–1062 (2007)
Liu, J., Ruan, D., Xu, Y., Song, Z.M.: A resolution-like strategy based on a lattice-valued logic. IEEE Transaction on Fuzzy System 11(4), 560–567 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
He, X., Xu, Y., Li, Y., Liu, J., Martinez, L., Ruan, D. (2010). α-Satisfiability and α-Lock Resolution for a Lattice-Valued Logic LP(X). In: Corchado, E., Graña Romay, M., Manhaes Savio, A. (eds) Hybrid Artificial Intelligence Systems. HAIS 2010. Lecture Notes in Computer Science(), vol 6077. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13803-4_40
Download citation
DOI: https://doi.org/10.1007/978-3-642-13803-4_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13802-7
Online ISBN: 978-3-642-13803-4
eBook Packages: Computer ScienceComputer Science (R0)