%0 Journal Article
%T AUTOMATIC THEOREM PROVING BASED ON MATINGS<br>基于配对方法的自动定理证明
%A CHEN Yuquan
%A LU Ruzhan
%A YU Hao
%A <br>陈玉泉
%A 陆汝占
%A 余皓
%J 软件学报
%D 1997
%I 
%X This paper first introduces the theory and algorithm of mating method in automatic theorem proving advanced by Peter B. Andrews, and then gives an implementation algorithm without backtracking, finally obtains a theorem proving system for higher order logic.
%K Automatic theorem proving
%K mating
%K resolution
%K connection
%K higher order logic<br>自动定理证明
%K 配对
%K 归结
%K 关联
%K 高阶逻辑
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=79342D007EC95C55C785E4F304F06BEE&yid=5370399DC954B911&vid=5D311CA918CA9A03&iid=E158A972A605785F&sid=273ADA1BCEFE8C00&eid=CAA7BAE04CB631A1&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=7