Normal Form of Łukasiewicz Logic Formulae and Related Counting Problems
Author:
Affiliation:

  • Article
  • | |
  • Metrics
  • |
  • Reference [14]
  • |
  • Related
  • |
  • Cited by
  • | |
  • Comments
    Abstract:

    The Shannon expansion in symbolic computation tree logic is generalized. In a n-valued Łukasiewicz logic system, Łn, the expansion of n-valued McNaughton functions which are induced by logical formulae is studied. The quasi disjunctive normal form and quasi conjunctive normal form of m-ary n-valued McNaughton functions, and the counting problems of m-ary n-valued McNaughton functions are given. In n-valued Łukasiewicz logic system Łn, the construction of formulae and counting problems of their logic equivalence class are provided.

    Reference
    [1] Baier C, Katoen JP. Principles of Model Checking. The MIT Press Cambridge, 2008.
    [2] Dasgupta P, Chakrabarti PP, Deka JK, Sankaranarayanan S. Min-Max computation tree logic. Artificial Intelligence, 2001,127(1): 137-162.
    [3] Ivan-i- F, Yang ZJ, ganai MK, Gupta A, Ashar P. Efficient SAT-based bounded model checking for software verification. Theoretical Computer Science, 2008,404(3):256-274. [doi: 10.1016/j.tcs.2008.03.013]
    [4] Basagiannis S, Katsaros P, Pombortsis A. An intruder model with message inspection for model checking security protocols. Computer & Security, 2010,29(1):16-34. [doi: 10.1016/j.cose.2009.08.003]
    [5] Burkart O, Steffen B. Model checking the full modal mu-calculus for infinite sequential processes. Theoretical Computer Science, 1999,221(1-2):251-270.
    [6] Lomuscio A, Penczek W, Wo-na B. Bounded model checking for knowledge and real time. Artificial Intelligence, 2007,171(16-17): 1011-1038. [doi: 10.1016/j.artint.2007.05.005]
    [7] Raimondi F, Lomuscio A. Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. Journal of Applied Logic, 2007,5(2):235-251. [doi: 10.1016/j.jal.2005.12.010]
    [8] Moreno-Ger P, Fuentes-Fernández R, Sierra-Rodriguez JL, Fernández-Manjón B. Model-Checking for adventure videogames. Information and Software Technology, 2009,51(3):564-580. [doi: 10.1016/j.infsof.2008.08.003]
    [9] Baresi L, Rafe V, Rahmani AT, Spoletini P. An efficient solution for model checking graph transformation systems. Electronic Notes in Theoretical Computer Science, 2008,213(1):3-21. [doi: 10.1016/j.entcs.2008.04.071]
    [10] Boucheneb H, Hadjidj R. CTL* model checking for time Petri nets. Theoretical Computer Science, 2006,353(1-3):208-227. [doi: 10.1016/j.tcs.2005.11.002]
    [11] Awedh M, Somenzi F. Termination criteria for bounded model checking: extensions and comparison. Electronic Notes in Theoretical Computer Science, 2006,144(1):51-66. [doi: 10.1016/j.entcs.2005.07.019]
    [12] Wang GJ. Introduction to Mathematical Logic and Resolution Principle. 2nd ed., Beijing: Science Press, 2006. 16-40 (in Chinese).
    [13] Cignoli RLO, D'Ottaviano IML, Mundici D. Algebraic Foundations of Many-Valued Reasoning. Dordrecht: Kluwer Academic Publishers, 2000. 7-30.
    [14] Wang GJ. Nonclassical Mathematical Logic and Approximate Reasoning. 2nd ed., Beijing: Science Press, 2008. 29-36 (in Chinese).
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

王庆平,王国俊.多值Łukasiewicz逻辑公式的范式表示和计数问题.软件学报,2013,24(3):433-453

Copy
Share
Article Metrics
  • Abstract:4131
  • PDF: 5541
  • HTML: 0
  • Cited by: 0
History
  • Received:January 05,2011
  • Revised:March 19,2012
  • Online: March 01,2013
You are the first2044671Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063