基于否证蕴含的极小一阶不可满足子式求解算法*张建民+,沈胜宇,李思昆(国防科技大学计算机学院,湖南长沙410073)AnAlgorithmforExtractingMinimalUnsatisfiableSubformulaeinFirst-orderLogicBasedonRefutationImplication*ZHANGJian-Min+,SHENSheng-Yu,LISi-Kun(SchoolofComputer,NationalUniversityofDefenseTechnology,Changsha410073,China)Abstract:Explainingthecausesofinfeasibilityofformulaehastheoreticalandpractical...
