zbMATH — the first resource for mathematics

The study of efficient algorithm for determining tautologicability of disjunctive normal form. (Chinese. English summary) Zbl 0773.03009
Summary: This paper is based on the work of B. Dunham and H. Wang [Ann. Math. Logic 10, 117-154 (1976; Zbl 0349.02006)]. It gives the theoretical foundations for finding efficient algorithms. A divide-and- conquer algorithm is also constructed.
03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX Cite