公开(公告)号：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.