摘要
连接法是自动定理证明中一种较新的证明方法,本文讨论了任意矩阵的连接法,给出了一条用于任意矩阵的一般的简化规则及其正确性的证明,并给出了相应的算法。
As a new method in automated theorem proving,the connection method for an arbitrary matrix is discussed in this paper where a general reduction rule and its proof of correctness are given.The corresponding algorithm is alsointroduced.
出处
《计算机应用与软件》
CSCD
1992年第5期29-34,共6页
Computer Applications and Software
关键词
人工智能
连接法
自动定理证明
Automated theorem proving
connection mothod
arbitrnry matrix
reduction rule.
