guijiefanyan.java

用Java编的人工智能的归结反演算法

import java.util.*;
import java.awt.*;
import java.awt.event.*;
import javax.swing.*;

public class Guijiefanyan extends JFrame 
{
	private JLabel zijuLabel,jielunLabel;
	private JButton  qiujieButton,exitButton;
	private JTextField zijuField,jielunField;	
	private JTextArea outputArea;
    String zijuString;
    String jielunString;
    
  public  Guijiefanyan()
  {
  	super("归结反演过程");
   
      
    Container container=getContentPane();
    container.setLayout(new FlowLayout());
    
    zijuLabel=new JLabel("输入前提子句集(如 !R(x) H(w)V!D(w)  L(A) )，按Enter");
    container.add(zijuLabel);
    zijuField=new JTextField(30);
    container.add(zijuField);
    
    jielunLabel=new JLabel("输入结论子句集(如 R(x)  !H(w)VD(w)  !L(A) )，按Enter");
    container.add(jielunLabel);
    jielunField=new JTextField(30);
    container.add(jielunField);
    
    qiujieButton=new JButton("归结反演求解");
    container.add(qiujieButton);
    outputArea=new JTextArea(10,20);
    outputArea.setEditable(false);
    container.add(new JScrollPane(outputArea));
    
    exitButton=new JButton("Exit");
    container.add(exitButton);
    
    ActionEventHandler handler=new ActionEventHandler();
    zijuField.addActionListener(handler);
    jielunField.addActionListener(handler);
    qiujieButton.addActionListener(handler);
    exitButton.addActionListener(handler);
    
    setSize(380,360);
    setVisible(true);
    show();
  }
    
    private class ActionEventHandler implements ActionListener
    {
    	public void actionPerformed (ActionEvent event)
    	{
    		if(event.getSource()==exitButton)
    		System.exit(0);
    		
    		 if(event.getSource()==zijuField)
    		{ 
    			 zijuString=event.getActionCommand();
    			 
    	     }
    	     
    	     
    	    if(event.getSource()==jielunField)
    		{ 
    		     jielunString=event.getActionCommand();
    		 }
    	     
    	     if(event.getSource()==qiujieButton)
    	     { 
    	       outputArea.setText("");
    	        String str=Resolution(zijuString,jielunString);
    	      	if(str.equals("NIL"))
    	      	str+="\n"+"成功";
    	      	else
    	      	 str+="\n"+"失败";
    	      	outputArea.setText(str);
    	     	     
    	     }
    	 }
    }
    
   public String GuijieResult(String P,String S)
   {
   	
   	if(P.equals("NIL")) return "NIL";
   	
   	StringTokenizer tokensP1=new StringTokenizer(P,"V");
   	StringTokenizer tokensS1=new StringTokenizer(S,"V");
    int countP1=tokensP1.countTokens();
    int countS1=tokensS1.countTokens();
   	if(countP1==1&&countS1==1)
   	{
   		String ff=tokensP1.nextToken();
   		String hh=tokensS1.nextToken();
   	    String d="";
   	    d+=ff.charAt(1);
   	    String g="";
   	    g+=hh.charAt(0);
   	    if(d.equals(g))return "NIL";
   	   
   
   	     String dd="";
   	     dd+=ff.charAt(0);
   	     String gg="";
   	     gg+=hh.charAt(1);
   	     if(dd.equals(gg))return "NIL";
   	     
   	     return P;
   	  }
   	
    String Clauses1="";
   	String Clauses2="";
   	String Clauses3="";
   	
   	StringTokenizer tokensP=new StringTokenizer(P,"V");
   	while(tokensP.hasMoreTokens())
   	  Clauses1+=tokensP.nextToken()+" ";
   	  
   	StringTokenizer tokensS=new StringTokenizer(S,"V");
   	while(tokensS.hasMoreTokens())
   	  Clauses1+=tokensS.nextToken()+" ";
   	  
   	StringTokenizer tokensClauses1=new StringTokenizer(Clauses1);
   	int numberClauses1=tokensClauses1.countTokens();
   	
   	String string[]=new String[30];
   	int tag[]=new int[30];
   	
   	int i=0;
   	
   	while(tokensClauses1.hasMoreTokens())
   	{
   		string[i]=tokensClauses1.nextToken();
   		i++;
   	}
   	
   	for(int a=0;a<i;a++)
   	{
   		String first="";
   		first+=string[a].charAt(0);
   		if(first.equals("!"))
   		{    
   	        first="";
   			first+=string[a].charAt(1);
   			for(int b=a+1;b<i;b++)
   			{
   				String match="";
   				match+=string[b].charAt(0);
   				if(match.equals(first))
   				   {
   				   	
   				    Clauses3+=string[a]+" "+string[b]+" ";
   				    tag[a]=1;
   				    tag[b]=1;
   				   }
   			}
   		  
   	     }
   	     
   	     else 
   	     {
   	     	for(int bb=a+1;bb<i;bb++)
   			{
   				String last="";
   				String tt="";
   				tt+=string[bb].charAt(0);
   				if(string[bb].length()!=1)
   				{
   					last+=string[bb].charAt(1);
                   if(tt.equals("!")&&last.equals(first))
   				   {
   				   	
   				    Clauses3+=string[a]+" "+string[bb]+" ";
   				    tag[a]=1;
   				    tag[bb]=1;
   				   }
   				 } 
   			}
   		     
   		   }
   	}
   	
   	String tempString[]=new String[30];
   	int yy=0;
   	for(int h=0;h<i-1;h++)
   	{
   		if(tag[h]==0)
   		{
   			tempString[yy]=string[h];
   		    yy++;
   		 }
   	}
   	for(int k=0;k<yy-1;k++)
   	Clauses2+=tempString[k]+"V";
   	Clauses2+=tempString[yy-1];
   
   	
   	 StringTokenizer tokensClauses3=new StringTokenizer(Clauses3);
   	int numberClauses3=tokensClauses3.countTokens();
   	if(numberClauses1==numberClauses3)
   	   Clauses2="NIL";
   
   	return Clauses2;
   }

public String Resolution(String P,String S)
{
	
	StringTokenizer tokensP11=new StringTokenizer(P);
   	StringTokenizer tokensS11=new StringTokenizer(S);
    int countP11=tokensP11.countTokens();
    int countS11=tokensS11.countTokens();
   	if(countP11==1&&countS11==1)
   	{
   		return ResolutionChange(P,S);
   	  }
   	    
	StringTokenizer tokensP1=new StringTokenizer(P,"V");
   	StringTokenizer tokensS1=new StringTokenizer(S,"V");
    int countP1=tokensP1.countTokens();
    int countS1=tokensS1.countTokens();
   	if(countP1==1&&countS1==1)
   	{
   		String ff=tokensP1.nextToken();
   		String hh=tokensS1.nextToken();
   	    String d="";
   	    d+=ff.charAt(1);
   	    String g="";
   	    g+=hh.charAt(0);
   	    if(d.equals(g))return "NIL";
   	   
   
   	     String dd="";
   	     dd+=ff.charAt(0);
   	     String gg="";
   	     gg+=hh.charAt(1);
   	     if(dd.equals(gg))return "NIL";
   	     
   	     return "FAIL";
   	  }
	
	int  np=0,ns=0;
    String TP[]=new String[30];
    StringTokenizer tokensP=new StringTokenizer(P);
    int numberP=tokensP.countTokens();
     while(tokensP.hasMoreTokens())
   	  {
   	  	TP[np]=tokensP.nextToken();
   	    np++;
     }

   String TS[]=new String[30];
   StringTokenizer tokensS=new StringTokenizer(S);
   int numberS=tokensS.countTokens();
    while(tokensS.hasMoreTokens())
   	  {
   	  	TS[ns]=tokensS.nextToken();
   	    ns++;
   	  }

   String Duo="";
   String Danyi="";
   for(int i=0;i<np;i++)
   {
	StringTokenizer tokensTemp=new StringTokenizer(TP[i],"V");
	if(tokensTemp.countTokens()!=1)
	Duo+=TP[i]+" ";
	else
	Danyi+=TP[i]+" ";
   }

   for(int i=0;i<ns;i++)
   { 
	StringTokenizer tokensTemp=new StringTokenizer(TS[i],"V");
	if(tokensTemp.countTokens()!=1)
	Duo+=TS[i]+" ";
	else
	Danyi+=TS[i]+" ";
   }
   
   
   if(Duo.equals(""))
    {
    	return ResolutionChange(P,S);	
    }
    
    int numberDanyi;
    int numberDuo;
    int jj;
    int jjg;
    int count=5;
    String tempP,tempS;
    tempP=P;
    tempS=S;
    
while(count>=0)
{
	
   //if(Duo.equals(""))
    	//return ResolutionChange(tempP,tempS);	
    if(Duo.equals(""))
    {
    	return ResolutionChange(P,S);	
    }
 
     	String stringDuo[]=new String[30];
        String stringDanyi[]=new String[30];
    
     jj=0;
     StringTokenizer t=new StringTokenizer(Duo);
     numberDuo=t.countTokens();
     while(t.hasMoreTokens())
   	  {stringDuo[jj]=t.nextToken();
   	    jj++;
   	 }
   	 
     jjg=0;
     StringTokenizer tttt=new StringTokenizer(Danyi);
     numberDanyi=tttt.countTokens();
     while(tttt.hasMoreTokens())
   	 {
   	  	stringDanyi[jjg]=tttt.nextToken();
   	    jjg++;
   	  }

 int duan[]=new int[30];
for(int aa=0;aa<jjg;aa++)
        for(int bb=0;bb<jj;bb++)
   {
   	StringTokenizer before=new StringTokenizer(stringDuo[bb]);
      stringDuo[bb]=GuijieResult(stringDuo[bb],stringDanyi[aa]);   	
      StringTokenizer after=new StringTokenizer(stringDuo[bb]);
      if(after.countTokens()<before.countTokens())
        duan[aa]=1;
   }


  tempP=Duo;
  tempS=Danyi;
  
  Duo="";
  Danyi="";
  for(int cq=0;cq<jjg;cq++)
    {
    	if(duan[cq]==0)
    	    Danyi+=stringDanyi[cq]+" ";
    }
  
  for(int r=0;r<jj;r++)
    { if(stringDuo[r].equals("NIL")) 
       	return "NIL";
     StringTokenizer pt=new StringTokenizer(stringDuo[r],"V");
     if(pt.countTokens()==1)
        Danyi+=stringDuo[r];
     else
        Duo+=stringDuo[r];
        
    }
  count--;
  }

 return  "FAIL";
 
}
   
  
  public String ResolutionChange(String P,String S)
   {
   	String Clauses1="";
   	String Clauses2="";
   	String Clauses3="";
   	
   	StringTokenizer tokensP=new StringTokenizer(P,"V");
   	while(tokensP.hasMoreTokens())
   	  Clauses1+=tokensP.nextToken()+" ";
   	  
   	StringTokenizer tokensS=new StringTokenizer(S,"V");
   	while(tokensS.hasMoreTokens())
   	  Clauses1+=tokensS.nextToken()+" ";
   	  
   	StringTokenizer tokensClauses1=new StringTokenizer(Clauses1);
   	int numberClauses1=tokensClauses1.countTokens();
   	
   	String string[]=new String[30];
   	int tag[]=new int[30];
   	
   	int i=0;
   	
   	while(tokensClauses1.hasMoreTokens())
   	{
   		string[i]=tokensClauses1.nextToken();
   		i++;
   	}
   	
   	for(int a=0;a<i;a++)
   	{
   		String first="";
   		first+=string[a].charAt(0);
   		if(first.equals("!"))
   		{    
   	        first="";
   			first+=string[a].charAt(1);
   			for(int b=a+1;b<i;b++)
   			{
   				String match="";
   				match+=string[b].charAt(0);
   				if(match.equals(first))
   				   {
   				   	
   				    Clauses3+=string[a]+" "+string[b]+" ";
   				    tag[a]=1;
   				    tag[b]=1;
   				   }
   			}
   		  
   	     }
   	     
   	     else 
   	     {
   	     	for(int bb=a+1;bb<i;bb++)
   			{
   				String last="";
   				String tt="";
   				tt+=string[bb].charAt(0);
   				if(string[bb].length()!=1)
   				{
   					last+=string[bb].charAt(1);
                   if(tt.equals("!")&&last.equals(first))
   				   {
   				   	
   				    Clauses3+=string[a]+" "+string[bb]+" ";
   				    tag[a]=1;
   				    tag[bb]=1;
   				   }
   				 }
   				 else 
   				 {
   				 	last+=string[bb].charAt(0);
   		            if(last.equals(first))
   				   {
   				   	
   				    Clauses3+=string[a]+" "+string[bb]+" ";
   				    tag[a]=1;
   				    tag[bb]=1;
   				   }
   				 }
   				 
   			}
   		     
   		   }
   	}
   	
   	
   	 StringTokenizer tokensClauses3=new StringTokenizer(Clauses3);
   	int numberClauses3=tokensClauses3.countTokens();
   	if(numberClauses1==numberClauses3)
   	Clauses2="NIL";
   	else if(numberClauses1!=numberClauses3)
   	 Clauses2+="FAIL";
   	
   	return Clauses2;
   }
  

    public static void main(String args[])
    {
    	Guijiefanyan application=new Guijiefanyan();
    	application.setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE);
    }
}