发明名称 |
Verfahren und Vorrichtung zum automatischen Beweisen von Theoremen für Informationsverarbeitung |
摘要 |
A method of automated theorem proving for information processing which can be highly efficient irrespective of a set of clauses to be dealt with. The method includes the steps of: transforming the statement and the set of knowledge into expressions in terms of elements of a module; constructing a linear equation with the elements of the module as coefficients and elements of a ring of scalars of the module as unknowns; checking the existence of non-negative solution to the linear equation; and determining that the statement is provable when the non-negative solution exist, and not provable otherwise. The apparatus for performing this method is also disclosed. |
申请公布号 |
DE68927143(T2) |
申请公布日期 |
1997.02.20 |
申请号 |
DE1989627143T |
申请日期 |
1989.07.20 |
申请人 |
KABUSHIKI KAISHA TOSHIBA, KAWASAKI, KANAGAWA, JP |
发明人 |
YAMAZAKI, ISAMU, KAWASAKI-SHI KANAGAWA-KEN, JP |
分类号 |
G06F9/44;G06F17/10;G06F17/30;G06F19/00;G06N5/00 |
主分类号 |
G06F9/44 |
代理机构 |
|
代理人 |
|
主权项 |
|
地址 |
|