一种基于代表模型的命题逻辑修正方法

摘要

一种基于代表模型的命题逻辑修正演算方法：(1)初始化结果集合Lambda，接受集合Sigma，系统集合Gamma和新代表模型列表NewModelList；(2)用Sigma的所有代表模型初始化代表模型列表ModelList；(3)如果系统集合Gamma为空集，则转到(8)；(4)从Gamma中取出一个命题A，并将其从Gamma删除；(5)利用A，Sigma和ModelList构造A的备选代表模型集合PropModel；(6)将PropModel中所有备选代表模型逐个对A验证：如果备选代表模型M使得A为真，则将M存入NewModelList；(7)如果NewModelList不是空集，用NewModelList赋值ModelList，并将NewModelList重置成空集，将A分别存入Lambda和Sigma，转(3)；否则直接转(3)；(8)输出结果Lambda。本发明根据系统集合中每个命题情况构造代表模型，以只验证相关模型的方法减少模型检查的次数，从而提高修正演算的效率。