###
DOI:
Journal of Software:1997.8(4):271-277

基于配对方法的自动定理证明
陈玉泉,陆汝占,余皓
(上海交通大学计算机科学与工程系,上海,200030)
AUTOMATIC THEOREM PROVING BASED ON MATINGS
CHEN Yuquan,LU Ruzhan,YU Hao
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 2976   Download 2975
    Revised:April 05, 1996
> 中文摘要: PeterB.Andrews提出了自动定理证明的配对方法的理论和算法.本文针对该算法的缺点,给出了一个无需回溯的实现算法,并得到一个高阶逻辑的自动定理证明系统.
中文关键词: 自动定理证明  配对  归结  关联  高阶逻辑
Abstract: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.
文章编号:     中图分类号:    文献标志码:
基金项目:本文研究得到国家自然科学基金资助. 本文研究得到国家自然科学基金资助.
Foundation items:
Reference text:

陈玉泉,陆汝占,余皓.基于配对方法的自动定理证明.软件学报,1997,8(4):271-277

CHEN Yuquan,LU Ruzhan,YU Hao.AUTOMATIC THEOREM PROVING BASED ON MATINGS.Journal of Software,1997,8(4):271-277