公开(公告)号：EP0351842A2

公开(公告)日：1990-01-24

申请号：EP89113337.3

申请日：1989-07-20

申请人： KABUSHIKI KAISHA TOSHIBA

发明人： Yamazaki, Isamu

IPC分类号： G06F9/44

CPC分类号： G06N5/006

摘要： 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.

摘要翻译： 一种用于信息处理的自动化定理的方法，无论要处理的一组条款如何，都可以高效地进行。 该方法包括以下步骤：根据模块的元素将语句和知识集合变换成表达式; 用模块的元素构建线性方程作为模块的标量环的系数和元素作为未知数; 检查线性方程的非负解的存在; 并确定在非消极解决方案存在的情况下证明该陈述，否则不可证明。 还公开了用于执行该方法的装置。

公开(公告)号：EP0403454B1

公开(公告)日：1995-06-28

申请号：EP90850184.4

申请日：1990-05-17

申请人： Stalmarck, Gunnar Martin Natanael

发明人： Stalmarck, Gunnar Martin Natanael

IPC分类号： G06F17/27

CPC分类号： G06F17/10 ,  G06F17/504 ,  G06N5/006

公开(公告)号：EP0670069B1

公开(公告)日：2001-09-26

申请号：EP94927697.6

申请日：1994-09-19

申请人： BULL S.A.

发明人： GOUBAULT, Jean

IPC分类号： G06F17/50 ,  G06F9/44

CPC分类号： G06F17/504 ,  G06N5/006

公开(公告)号：EP0670069A1

公开(公告)日：1995-09-06

申请号：EP94927697.0

申请日：1994-09-19

申请人： BULL S.A.

发明人： GOUBAULT, Jean

IPC分类号： G06F9 ,  G06F17 ,  G06N5

CPC分类号： G06F17/504 ,  G06N5/006

摘要： Method for proving theorems describing physical systems in first order logic. The method is used to produce complex systems, and is implemented using a computer, in whose memory a theorem to be proved is represented by at least one binary decision diagram (BDD). The method seeks to reduce the BDD to a constant V, symbolizing the real value, by a substitution, a search tree of possible substitutions being constructed and explored. The tree is constructed by minimizing the branching factor and is explored by maximizing, in accordance with Shannon theory, the information gain obtained at each search tree node.

公开(公告)号：EP0403454A1

公开(公告)日：1990-12-19

申请号：EP90850184.4

申请日：1990-05-17

申请人： Stalmarck, Gunnar Martin Natanael

发明人： Stalmarck, Gunnar Martin Natanael

IPC分类号： G06F17/27

CPC分类号： G06F17/10 ,  G06F17/504 ,  G06N5/006

摘要： The invention relates to a method and apparatus for theorem checking with the intention in so-called tautology checks of establishing whether or not all possible attributions of the truth values (0 and 1) to variables in a boolean formula render the formula true. The problem of known techniques is that checking of the truth content is effected against all variables in an original formula, which requires many calculations to be made and which is highly time-consuming.
According to the invention, an original formula is divided into part-expressions, so-called triplets, each corresponding to a part-formula of the original formula, whereafter logic 0:s and 1:s are instantiated (allotted) to variables in the triplets for the purpose of checking the truth content. The check is thus made against triplets instead of against all variables in the original formula, therewith greatly reducing the number of calculations necessary and providing a considerable saving in time. Apparatus, called a theorem checker, for carrying out the method includes a sequence unit for controlling the calculation sequency, a generator G for generating sequences of ordered variables, a permanent unit P for storing triplets, a plurality of arithmetical units, evaluators (E) and an analyzer A operative to analyze the result obtain from all calculations.

摘要翻译： 本发明涉及一种用于定理检查的方法和装置，其意图在所谓的重复检查中确定真值（0和1）对于布尔公式中的变量的所有可能归属是否使公式为真。 已知技术的问题是检查真实内容是针对原始公式中的所有变量进行的，这需要进行许多计算并且是非常耗时的。 根据本发明，原始公式被分为部分表达式，即所谓的三元组，每个对应于原始公式的部分公式，之后逻辑0：s和1：s被实例化（分配）到 三重组，用于检查真相内容。 因此，检查是针对三元组，而不是原始公式中的所有变量，从而大大减少了必要的计算数量，并大大节省了时间。 称为定理检验器的装置，用于执行该方法，包括用于控制计算顺序的序列单元，用于产生有序变量序列的发生器G，用于存储三元组的永久单元P，多个算术单元，评估器（E） 以及分析器A，用于分析从所有计算获得的结果。

公开(公告)号：EP2608119A1

公开(公告)日：2013-06-26

申请号：EP11194466.6

申请日：2011-12-20

申请人： Mitsubishi Electric R&D Centre Europe B.V. ,  Mitsubishi Electric Corporation

发明人： Mentre, David

IPC分类号： G06N5/00 ,  G06F11/36

CPC分类号： G06F11/3608 ,  G06N5/006

摘要： For automatically proving the correctness of a software program model, said software program model involving a set of proof obligations to be proved by a first automatic prover and at least one second automatic prover, each proof obligation being described in a format compliant with the first automatic prover, a device: obtains, for each proof obligation to be proved, an abstract syntax tree representing said obligation to be proved, each abstract syntax tree comprising interconnected nodes and leaves representing each operator and operand of said obligation to be proved; associates a type with each node and leaf in the obtained abstract syntax trees, a type for an operator being at least defined on the basis of the type of the result of the operation performed by the operator; and converts the abstract syntax trees with associated types into at least one proof obligations description matching a format compliant with the at least one second automatic prover, each node or leaf of the abstract syntax trees being converted in a corresponding symbol in said format compliant with the at least one second automatic prover taking into account the type associated with said node or leaf.

摘要翻译： 用于自动证明的软件程序模型的正确性，所述软件程序模型涉及一组证明义务由第一自动证明者和至少一个第二自动证明方证明，每个密封义务所描述的格式符合第一自动 证明者，一个装置：取得，对于要证明各证明义务，表示所述义务抽象语法树来加以证明，每个抽象语法树，其包括相互连接的节点和叶子表示所述义务的每个操作符和操作数来加以证明; 关联与每个节点和叶在所获得抽象语法树，一个类型在操作者是通过操作者进行的外科手术的结果的类型的基础上，至少定义的类型; 和具有相关联的类型的成至少一个证明义务描述匹配符合所述至少一个第二自动证明者，所述抽象语法树中的每个节点或叶的格式抽象语法树转换被转换成所述格式符合的一个相应码元 至少一个第二自动证明者考虑到与所述节点或叶相关联的类型。

公开(公告)号：EP0351842B1

公开(公告)日：1996-09-11

申请号：EP89113337.3

申请日：1989-07-20

申请人： KABUSHIKI KAISHA TOSHIBA

发明人： Yamazaki, Isamu

IPC分类号： G06F9/44

CPC分类号： G06N5/006

公开(公告)号：EP0351842A3

公开(公告)日：1992-07-08

申请号：EP89113337.3

申请日：1989-07-20

申请人： KABUSHIKI KAISHA TOSHIBA

发明人： Yamazaki, Isamu

IPC分类号： G06F9/44

CPC分类号： G06N5/006

摘要： 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.