MARKED MODAL RESOLUTION
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    To overcome the notation redundancy in the modaI resolution systems estab-lished bv P.Enjalbert and L.Farinas del Cerro,the authors propose marked modal resolu-tion.whose soundness and completeness are proved.In marked modal resolution,they mark possible operators in modal clauses,and add a rule for computing resolvent of two formulas which are bound by possible operator respectively.This new method has the fol-lowing feature:a resolvent may not be a logical consequence of its parents,it is only a log-ical consequence of the input set of clauses,that iS the soundness.At the same time,they design and implement system RD based on modal resolution of Enjalbert and Farinas del Cerro.and system MRD based on marked modal resolution in C-PROLOG,and then run on SUN workstation.The experimental results show:the MRD method iS almostly 10 times faster than RD.

    Reference
    Related
    Cited by
Get Citation

孙吉贵,刘叙华.标记模态归结推理*.软件学报,1996,7(zk):156-162

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:March 06,1995
  • Revised:
  • Adopted:
  • Online:
  • Published:
You are the firstVisitors
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