请教：定理自动证明程序实现

Question

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

Answer 1

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

Answer 2

对于人工智能没什么研究
以前好像听说过一种prolog语言，专门用于逻辑推理的，搜索一下该语言的相关资料，然后自己参考改成java程序看看。