G - Physics – 06 – F
Patent
G - Physics
06
F
354/166
G06F 7/00 (2006.01) G06F 17/10 (2006.01) G06F 17/50 (2006.01) G06N 5/00 (2006.01)
Patent
CA 2018828
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 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
L'invention est constituée par une méthode et un appareil de vérification de théorèmes utilisés dans la détection des tautologies pour déterminer si toutes les attributions possibles de valeurs de vérité (0 et 1) aux variables d'une formule booléenne rendent cette dernière vraie. Dans les méthodes actuelles, cette vérification est effectuée sur toutes les variables de la formule, ce qui nécessite un grand nombre de calculs et prend beaucoup de temps. Dans la présente invention, la formule est divisée en expressions partielles appelées triplets qui correspondent chacune à une partie de la formule de départ, puis des valeurs logiques 0 et 1 sont affectées aux variables des triplets aux fins de la vérification. Celle-ci est donc effectuée sur les triplets plutôt que sur l'ensemble des variables de la formule de départ, ce qui réduit considérablement le nombre des calculs nécessaires et réalise une économie de temps considérable. L'appareil utilisant cette méthode comprend une unité de séquencement utilisée pour contrôler la séquence de calcul, un générateur de séquences de variables ordonnées G, une unité permanente de stockage de triplets P, une pluralité d'unités arithmétiques, des évaluateurs E et un analyseur A qui sert à analyser les résultats des calculs.
Marks & Clerk
Prover Technology Ab
LandOfFree
Determining propositional logic theorems by applying values... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Determining propositional logic theorems by applying values..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Determining propositional logic theorems by applying values... will most certainly appreciate the feedback.
Profile ID: LFCA-PAI-O-1498899