Data processing: artificial intelligence – Knowledge processing system – Knowledge representation and reasoning technique
Patent
1997-06-24
1999-05-18
Black, Thomas G.
Data processing: artificial intelligence
Knowledge processing system
Knowledge representation and reasoning technique
G06F15/18
Patent
active
059059770
ABSTRACT:
The invention relates to a method for automatic proving theorems describing physical systems in first order logic. This method is used to produce complex systems and is implemented with the aid of 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 T, symbolizing truth, by a substitution, by constructing and exploring a search tree of possible substitutions. The tree is constructed by minimizing the branching factor and is explored by maximizing in accordance with the Shannon theory, the information gain obtained at each node of the search tree.
REFERENCES:
patent: 5243538 (1993-09-01), Okuzawa et al.
patent: 5331568 (1994-07-01), Pixley
patent: 5434794 (1995-07-01), Coudert et al.
patent: 5493504 (1996-02-01), Minato
patent: 5574893 (1996-11-01), Southgate et al.
Schneider et al., Hardware-Verification using first order BDDs, Proceedings of the 11th IFIP, pp. 45-62, Apr. 26, 1993.
Coudert et al., Fault tree analysis: 10/sup20/prime implicants and beyond, Annual Reliability and Maintainability Symposium 1993, pp. 240-245, Jan. 28, 1993.
Minato et al., Shared binary decision diagram with attributed edges for efficient Boolean function manipulation, 27th ACM/IEEE Design Automation Conference, Proceedings 1990, pp. 52-57, Jun. 28, 1990.
Stanion et al., Tsunami: a path oriented scheme for algebraic test generation, Fault tolerant computing, 21st intl. symposium, pp. 36-43, Jun. 27, 1991.
Takahashi et al., Fault simulation for multiple faults using shared BDD representation of fault sets, 1991 IEEE International conference on computer-aided design, pp. 550-553, Nov. 14, 1991.
Proceedings of the 11th IFIP WG10.2 International Conference on Computer Hardware Description Languages and Their Applications, Apr. 26, 1993, Ottawa Ontario Canada pp. 45-62 Schneider et al "Hardware verification using first oder bdds" see entire document.
GWAI-92: Advance in Artificial Intelligence 16th German Conference on Artificial Intelligence Proceedings, Aug. 31, 1992, Bonn Allemagne pp. 67-76 Posegga et al "Towards First-Order Deduction Based on Shannon Graphs" see entire document.
Chang et al., Technology mapping via transformations of function graphs, IEEE 1992 International Conference on Computer Design, pp. 159-162, Oct. 14, 1992.
Jacobi et al., Incremental reduction of binary decision diagrams, 1991 IEEE International Symposium on circuits and systems, pp. 3174-3177, Jun. 14, 1991.
Black Thomas G.
Bull S.A.
Kondracki Edward J.
Shah Sanjiv
LandOfFree
Method for automatic demonstration does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Method for automatic demonstration, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method for automatic demonstration will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-1769049