请教：定理自动证明程序实现
最近在学人工智能，想用java写一个定理的自动证明程序，自动实现定理基于规则的和基于归结的演绎推理，有哪位大虾做过给小弟指点一下，不用给出完整的程序，给个思路就行，小弟在这先谢了

------解决方案--------------------
在系统中System.out.println("n=" + n);//看看n的情况
当你第一次增加时
if(list[n][0] == " ") //不知道你改成equals了没有
这次判断成功，所以最追加了一条记录，但此时n没有改变，还是3
当你第二次增加时，首先输出一次“请输入”，而此时因为n是3
所以if(list[n][0] == " ") 判断失败
程序走到
else
{ 
n++; 
add(); 
} 
又再次调用了add方法，这时又输出一次“请输入”所以就是你说的输出2次了
所以应该在追加成功后对增加n
即
if(j == 4) 
{ 
System.out.println("增加成功！"); 
display(); 
n++;//这里
} 
然后
else
{ 
n++; 
add(); 
} 
这部分不要。

而你把“请输入”放到if里，也就是
只有if(list[n][0] == " ")判断成功才会输出
所以第二次增加时，因为n是3
所以if(list[n][0] == " ") 判断失败，所以没有输出“请输入”
而程序走到
else
{ 
n++; 
add(); 
} 
又再次调用了add方法，这时n=4
if(list[n][0] == " ") 判断成功，所以这时才输出“请输入”，所以也就只有一次了

这样说明，LZ该清楚了吧，建议你在学习的时候，自己在程序中多打印一些信息，这样你自己就可以根据这些信息去追踪程序的执行顺序，然后自己再去想想为什么会这样。多动手多思考才有助于提高。