首页>
外国专利>
DETERMINING PROPOSITIONAL LOGIC THEOREMS BY APPLYING VALUES AND RULES TO TRIPLETS THAT ARE GENERATED FROM A BOOLEAN FORMULA
DETERMINING PROPOSITIONAL LOGIC THEOREMS BY APPLYING VALUES AND RULES TO TRIPLETS THAT ARE GENERATED FROM A BOOLEAN FORMULA
展开▼
机译：通过应用值和规则来确定提议的逻辑定理，这些值和规则是根据布尔公式生成的三元组
展开▼
页面导航
摘要
著录项
相似文献
摘要
The invention relates to a method and apparatus for theoremchecking with the intention in so-called tautology checks ofestablishing whether or not all possible attributions of thetruth values (0 and 1) to variables in a boolean formularender the formula true. The problem of known techniques isthat checking of the truth content is effected against allvariables in an original formula, which requires manycalculations to be made and which is highly time-consuming.According to the invention, an original formula is dividedinto part-expressions, so-called triplets, eachcorresponding to a part-formula of the original formula,whereafter logic 0:s and 1:s are instantiated (allotted) tovariables in the triplets for the purpose of checking thetruth content. The check is thus made against tripletsinstead of against all variables in the original formula,therewith greatly reducing the number of calculationsnecessary and providing a considerable saving in time.Apparatus for carrying out the method includes a sequenceunit for controlling the calculation sequency, a generator Gfor generating sequences of ordered variables, a permanentunit P for storing triplets, a plurality of arithmeticalunits, evaluators (E), and an analyzer A operative toanalyze the result obtain from all calculations
展开▼
