Journal of Logic and Computation Advance Access published online on January 8, 2008
Journal of Logic and Computation, doi:10.1093/logcom/exm077
Original papers |
General Models and Completeness of First-Order Modal µ-calculus
Department of Mathematical and Computing Sciences, Tokyo Institute of Technology. Ookayama, Meguro, Tokyo 152-8552, Japan. E-mail: kashima{at}is.titech.ac.jp
Research Center for Verification and Semantics, National Institute of Advanced Industrial Science and Technology, 1-2-14 Shin-Senri Nishi, Toyonaka, Osaka 560-0083, Japan. E-mail: keishi-okamoto{at}aist.go.jp
Received 16 April 2007.
| Abstract |
|---|
There is no recursive axiomatization of first-order modal µ-calculus that is complete with respect to usual Kripke models. Then we introduce `general' models, and we prove that the natural axiom system of first-order modal µ-calculus is complete with respect to general models.
Keywords: First-order modal µ-calculus; modal logic; Kripke model; general model; completeness