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

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

基于列随机矩阵的逐次差分代换与正半定型的机械化判定

本文选择列随机平均矩阵Tn作为基本代换矩阵，建立了基于％的逐次差分代换方法．获得了腿翌上正半定型，不定型判定的充要条件．并进一步证明了：正定型的差分代换集序列正向终止．根据这些结果编写的Maple程序TSDS3，能够自动证明代数型不等式，对不成立的不等式总能输出反例．该程序虽可能不停机，但大量的应用实例证实了该方法的实用性．