命题公式真值表的生成与公式类型的机械判定

Generating Algorithm of Truth Value Table and Type's Mechanical Decision to a Propositional Formula

在文[1]的基础上,给出了命题逻辑中任一命题公式的真值表的生成算法与命题公式类型的判定算法,实现了利用计算机对有限多个命题公式的真值表的直接计算和输出,以及对一个命题公式是重言式、矛盾式或可满足式的机械判定.

Based on paper [1] ,this paper gives a generating algorithm of truth value table and an algorithm to determine types of propositional formulae. Using these algorithms, we can use computer mechanically to list truth value table of a group of propositional formulae,determine that if a given propositional formula is a tautology,a contradiction,or if the formula is satisfiable.