| 摘要 |
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 sub-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 sequence, 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.
|
