Featured image of post 自动推理（实验相关内容）
江西理工大学

自动推理（实验相关内容）

实验

创建日期:
最后修改:

“Work. ”

前言

进行此项内容前，请确保已经完成环境的配置。
相关网站：TPTP官网

1、实验前准备

准备条件

拷贝好dist文件夹，确保内部具有正确的文件

problems文件夹中存放问题以及Axiom公理集，测试完output中会存放生成相关文件，strategy中存放策略集合，proofStatistics.txt内存放所有问题的证明时间。
在dist文件夹内打开命令行窗口，使用ls命令，检查文件是否具有可执行权限：
cse,eprover,tptp4X,以及相关jar包。
若没有权限，使用如下命令对文件授予权限：chmod +x 文件名
使用./eprover --verson或./vampire --verson查看对应软件的版本
使用命令行版本测试时，将cse替换为自己导出的cse
替换eprover的版本时，要将eprover和mcs_eprover.jar同时替换才正确。
3.1以上的版本的Eprover会出现异常，则需要进行以下操作（重新打开一个终端，输入下述指令）：

1

ps -ef|grep eprover

然后使用kill指令将前三个icdc进程杀死
拓展(输入./vampire –ignore_missing on –mode casc -t 300 +一个问题的绝对路径，就能得到下面这样的证明搜索路径和时间，这样子只能测单个的原始时间)

带界面版本测试命令

在虚拟机内：选择⽤户args01，密码是icdc1016，若选择guest⽤户请先logout切换⽤户

  • (1)启动Terminal;
  • (2)切换⽬录：cd Desktop/dist;
  • (3) 执⾏命令：./kzprover.sh，脚本没有可执⾏权限时， sudo chmod +x kzprover.sh;
  • (4) 启动时把单组合模式改为多组合模式，其他不需要改.

命令行版本测试命令

测试CSE和Eprover融合系统命令：

1

java -jar mcs_epr.jar CSE_E problems 0 1 4 1 300 0 1 10

测试CSE和Vampire融合系统命令：

1

java -jar mcs_vampire.jar CSE_V problems 0 1 2 1 260 30 1 10

单独测试CSE系统命令：

1

java -jar mcs_scs.jar CSE problems 0 1 0 1 1 10

其中260 20 为时间参数 如果那两个数值变为300 0，意味着是原始测出来的数据， 前一个数值代表eprover测的时间，后一个数值代表CSE测的时间， 300秒减去前两个数值所剩下的时间也是eprover参与的

jar包修改相关内容

  • NetBeans 8.0.2 Mcs_epr.java 第734行
  • String combinedRunCmd = “timeout " + firstRunTime + " " + getAppPath() + File.separator + “eprover –delete-bad-limit=2000000000 –definitional-cnf=24 -s –print-statistics -R –print-version –proof-object –auto-schedule –cpu-limit=” + 300 + " " + problemPath;
  • 根据eprover官网给出的命令进行对应的修改
  • 编译后，jar包输出位置为：Desktop/2020_CASC_PROCESS/mcs_epr/dist

2、代码相关逻辑

基础代码修改项

必改项
2217Resolution.cppfor(int i=0;iuLitNum;++1i){删除1
使用776行的main函数替换原始800行的main函数
验证检查原始代码修改后，会生成run文件
Prover.cpp
319		if(1){
FileOp::delRunFiles();
}		if(0){
FileOp::delRunFiles();
}
选改项
main.cppdebug编译release
216#define newTriDebug//#define newTriDebug
755//child = fork();
if (0 == 0)		child = fork();
if (child == 0) {
生成cse文件

部分演绎框架

CSE1.3_pre文件位置方法名
较优子句TriAlg.cpp345GenerateTriByRecodePath
优化演绎路径TriAlg.cpp1832GenerateTriByRecodePathLROptimalProofSearch
充分使用子句TriAlg.cpp2983GenerateTriByRecodePathLR
单元子句排序规则SortRule.h168
候选子句排序Resolution.cpp4833
合一算法Unify.cpp320LitMgu
预处理Resolution.cpp3183

构建标准矛盾体思想

方法从左到右构建从右到左构建
思想选择了候选子句集的文字，
在决策文字集上遍历文字判断是否互补		选择了决策文字集上的文字，
在候选子句集中遍历子句，再遍历文字是否互补
代表算法充分使用子句，优化演绎路径较优子句

标准矛盾体：
决策文字及其下拉文字，但不包含对角线最后一位

文字变元输出

1
2

cout<< QLit->subTerm->ToString()<<endl;//debug输出当前文字项
cout<<QLit->subTerm->ToStringBind()<<endl;//debug输出当前文字项和变元元替换项

3、融合系统E3.1以上版本卡住解决方法

解决方法1：原始方法
新打开一个命令行窗口输入以下指令：

1

ps -ef|grep eprover

使用kill指令将前三个eprover的进程杀死。
解决方法2：自编sh脚本方法
新建一个名为kill.sh的文件，其内代码编写如下：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49

# 获取脚本文件所在的路径
SCRIPT_DIR=$(dirname "$(readlink -f "$0")")
# 日志文件路径
LOG_FILE="$SCRIPT_DIR/kill-log.txt"
# 检查并删除已存在的日志文件
if [ -f "$LOG_FILE" ]; then
    rm "$LOG_FILE"
fi
# 创建新的日志文件
touch "$LOG_FILE"
# 循环执行
echo "实验进程守护中，请勿关闭此窗口"
while true; do
    # 获取 proofStatistics.txt 的路径
    PROOF_FILE="$SCRIPT_DIR/proofStatistics.txt"
    # 如果 PROOF_FILE 为空或文件不存在，直接跳到 sleep 420
    if [ -z "$PROOF_FILE" ] || [ ! -f "$PROOF_FILE" ]; then
        echo "实验进程守护中，请勿关闭此窗口"
        sleep 350
        continue
    fi
    # 获取 proofStatistics.txt 的修改时间（单位：秒）
    FILE_MOD_TIME=$(stat -c %Y "$PROOF_FILE")
    # 获取当前系统时间（单位：秒）
    CURRENT_TIME=$(date +%s)
    # 计算时间差（单位：秒）
    TIME_DIFF=$((CURRENT_TIME - FILE_MOD_TIME))
    # 判断时间差是否超过 7 分钟 (420 秒)
    if [ "$TIME_DIFF" -le 420 ]; then
        # 如果时间差未超过 7 分钟，结束本轮循环
        echo "实验进程守护中，请勿关闭此窗口"
    else
        # 如果时间差超过 7 分钟，杀死所有名为 eprover 的进程
        PIDS=$(pgrep -f eprover)
        if [ -n "$PIDS" ]; then
            # 获取当前系统时间
            CURRENT_TIME_READABLE=$(date "+%Y-%m-%d %H:%M:%S")
            # 记录杀死进程的 PID 并写入日志文件
            for PID in $PIDS; do
                echo "$CURRENT_TIME_READABLE - 成功杀死进程, PID: $PID" >> "$LOG_FILE"
            done
            # 杀死所有名为 eprover 的进程
            pkill -f eprover
	    echo "成功杀死进程"
        fi
    fi
    # 等待 7 分钟后再次循环
    sleep 420 # 420秒 == 7分钟
done

其原理如下：

  • 脚本检测dist路径下的proofStatistics.txt文件的修改时间，若超过7分钟，则杀死名为eprover的所有进程。
  • 若proofStatistics.txt文件的修改时间，未超过7分钟则等待7分钟后进入下一轮循环
  • 若未检测到proofStatistics.txt文件，则休眠7分钟。

使用规则：

  • 将kill.sh文件置于dist文件夹内；
  • 使用chmod +x kill.sh授予权限；
  • 在命令窗口使用./kill.sh启动脚本；
  • 脚本会在dist文件夹内生成kill-log.txt日志文件。
最后更新于 2026-04-02 23:33