%0 Journal Article
%T A AUTOMATIC THEOREM PROVING SYSTEM BASED ON GENERALIZED RESOLUTION<br>基于广义归结的定理机器证明系统
%A Cheng Xiaochun
%A Sun Jigui
%A Liu Xuhua
%A <br>程晓春
%A 孙吉贵
%A 刘叙华
%J 软件学报
%D 1995
%I 
%X The authors prove 350 theorems of "Principia Mathematica" by a theorem proving system based on generalized resolution. Compared it with traditional resolution,they complement new strategy, avoid self-resolution, and discuss its time and space complexity.
%K Generalized resolution
%K NC resolution
%K OCCUR check
%K schedule strategy<br>广义归结，NC归结，OCCUR检查，调度策略
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=8D77CA688D536450FD96B0846FC3FF74&yid=BBCD5003575B2B5F&vid=B31275AF3241DB2D&iid=DF92D298D3FF1E6E&sid=F10601728A1E9BEA&eid=B7ACE2F11789CAE0&journal_id=1000-9825&journal_name=软件学报&referenced_num=5&reference_num=9