prover:命题逻辑的分解定理证明者

证明者 命题逻辑的分解定理证明者 免责声明 此存储库仅用于历史保存。 该代码已被冻结，处于打开状态。 用法 输入 输入是一个文本文件，每行一个CNF语句，格式如下： x1 x2 x3 ... 意思是 x1 OR x2 OR x3 OR ... 您可以使用代字号否定变量： penguin ~cat ~dolphin 示例文件： skyIsBlue skyIsOrange ~skyIsOrange irrelevantVar ~skyIsBlue 确保您包括要证明的结论的否定词。 ### output每个语句都有编号，对于派生语句，将列出其父级。 如果发现矛盾（证明成功），则False将是最后一个陈述。 笔记 这是2013年我的人工智能班的一个项目。