DESTRUCTIVE EXTENSION RULE IN PROPOSITION MODAL LOGIC K

Wu, X.; Sun, J.G.

doi:10.1007/978-1-4020-3953-9_12

X. Wu⁴ &
J.G. Sun⁴

1669 Accesses
2 Citations

Abstract

Modal logics are good candidates for a formal theory of agents, the efficiency of reasoning method in modal logics is very important, because it determines whether or not the reasoning method can be used widely in the systems based on agent. Theorem proving based on the extension rule we presented is a new method. Firstly, this paper gives the version of non-clausal extension rule algorithm. Next, we present the extension rule in proposition modal logic K, namely we provide a new proof method for modal logics. And then we give the proof of its soundness and completeness.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Chapter: USD 29.95; Price excludes VAT (USA)

eBook: USD 259.00; Price excludes VAT (USA)

Softcover Book: USD 329.99; Price excludes VAT (USA)

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

REFERENCES

H. Lin, J.G. Sun and Y.M. Zhang (2003), Theorem proving based on extension rule. Journal of Automated Reasoning, 31, pp. 11–21.
Article MATH MathSciNet Google Scholar
H.J. Ohlbach (1988), A Resolution Calculus for Modal Logics, CADE’88, pp. 23–26.
Google Scholar
M.C. Fitting (1990), Destructive modal resolution. Journal of Logic and computation, 1, pp. 11–21, 83–97.
Article MathSciNet Google Scholar
M. Fisher, C. Dixon and M. Peim (2001), Clausal temporal resolution. ACM Transactions on Computational Logic, 2, pp. 1–44.
Article MathSciNet Google Scholar
A. Artale and E. Franconi (1998), A temporal description logic for reasoning about action and plans. Journal of Artificial Intelligence Research, 9, pp. 463–506.
MATH MathSciNet Google Scholar
U. Hustadt, C. Dixson, R.A. Schmidt and M. Fisher (2000), Normal Forms and Proofs in Combined Modal and Temporal Logics, FroCoS’2000, France, pp. 73–87.
Google Scholar
R.S. Liu, J.G. Sun and X.H. Liu (1998), Epistemic Logic (3): on semantic tableau proof procedure. Chinese Journal of Computers, 21, Suppl., pp. 1–8.
Google Scholar
J.G. Sun, R.S. Liu, and R. Chen (1999), An extension on marked modal resolution. Chinese Journal of Computers, 2, pp. 113–119.
MathSciNet Google Scholar
R.A. Schmidt and U. Hustadt (2003), A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae, CADE’2003, USA, pp. 412–426.
Google Scholar

Download references

Author information

Authors and Affiliations

College of Computer Science and Technology, Jilin University, Key Laboratory of Symbolic Computation and Knowledge Engineer of Ministry of Education, ChangChun, 130012, P. R. China
X. Wu & J.G. Sun

Authors

X. Wu
View author publications
You can also search for this author in PubMed Google Scholar
J.G. Sun
View author publications
You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

National University of Singapore, Singapore
G.R. LIU
National University of Singapore, Singapore
V.B.C. TAN
Hunan University, P.R. China
X. HAN

Rights and permissions

Reprints and permissions

Copyright information

About this paper

Cite this paper

Wu, X., Sun, J. (2006). DESTRUCTIVE EXTENSION RULE IN PROPOSITION MODAL LOGIC K. In: LIU, G., TAN, V., HAN, X. (eds) Computational Methods. Springer, Dordrecht. https://doi.org/10.1007/978-1-4020-3953-9_12

Download citation

DOI: https://doi.org/10.1007/978-1-4020-3953-9_12
Publisher Name: Springer, Dordrecht
Print ISBN: 978-1-4020-3952-2
Online ISBN: 978-1-4020-3953-9
eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics