unit1my.cpp

基于机器学习的自动逻辑推理机。本程序用归结反演策略实现了命题逻辑系统的自动推理。把要解决的问题作为一个要证明的命题

//---------------------------------------------------------------------------
#include <vcl.h>
#pragma hdrstop

#include "Unit1my.h"
#include "Stack1.h"
#include "Unit2my.h"
#include "Unit3my.h"
//---------------------------------------------------------------------------
#pragma package(smart_init)
#pragma resource "*.dfm"

TForm1 *Form1;
//---------------------------------------------------------------------------
__fastcall TForm1::TForm1(TComponent* Owner)
        : TForm(Owner)
{
}
//---------------------------------------------------------------------------

void __fastcall TForm1::Button3Click(TObject *Sender)
{
        SendMessage(Memo1->Handle,WM_CHAR,('('),(LPARAM)0);
        ::SetFocus(Memo1->Handle);

}
//---------------------------------------------------------------------------
void __fastcall TForm1::ClearClick(TObject *Sender)
{
       Memo1->Clear();
       ::SetFocus(Memo1->Handle);
}
//---------------------------------------------------------------------------

void __fastcall TForm1::Button4Click(TObject *Sender)
{
        SendMessage(Memo1->Handle,WM_CHAR,(')'),(LPARAM)0);
        ::SetFocus(Memo1->Handle);
}
//---------------------------------------------------------------------------

void __fastcall TForm1::Button5Click(TObject *Sender)
{
        SendMessage(Memo1->Handle,WM_CHAR,('&'),(LPARAM)0);
        ::SetFocus(Memo1->Handle);
}
//---------------------------------------------------------------------------

void __fastcall TForm1::Button6Click(TObject *Sender)
{
        SendMessage(Memo1->Handle,WM_CHAR,('|'),(LPARAM)0);
        ::SetFocus(Memo1->Handle);
}
//---------------------------------------------------------------------------

void __fastcall TForm1::Button7Click(TObject *Sender)
{
        SendMessage(Memo1->Handle,WM_CHAR,('!'),(LPARAM)0);
        ::SetFocus(Memo1->Handle);
}
//---------------------------------------------------------------------------

void __fastcall TForm1::Button8Click(TObject *Sender)
{
        SendMessage(Memo1->Handle,WM_CHAR,('>'),(LPARAM)0);
        ::SetFocus(Memo1->Handle);
}
//---------------------------------------------------------------------------
void __fastcall TForm1::ExitClick(TObject *Sender)
{
     Form1->Close();
}


//---------------------------------------------------------------------------
void __fastcall TForm1::SubmitClick(TObject *Sender)
{
     T_Prepare Pre1;
     AnsiString Input;
     T_node *p;
     int i,j;

     Input=Memo1->Text;
     if(Pre1.Inspect(Input)==1)
       {

          Pre1.Polish(Input);
          p=Pre1.Semantic();
          Pre1.Plot(p);


          RichEdit1->Clear();
          for(i=0;S[i][0]!=0;i++)
          {     if(S[i][0]>0)
                {       RichEdit1->Text=RichEdit1->Text+"S["+i+"]="+V[S[i][0]];}
                else
                {       RichEdit1->Text=RichEdit1->Text+"S["+i+"]=～"+V[abs(S[i][0])];}
                for(j=1;S[i][j]!=0;j++)
                {       if(S[i][j]>0)
                        {       RichEdit1->Text=RichEdit1->Text+"∨"+V[S[i][j]];}
                        else
                        {       RichEdit1->Text=RichEdit1->Text+"∨～"+V[abs(S[i][j])];}
                }
                RichEdit1->Text=RichEdit1->Text+"\r\n";
          }


          i=1;
          Memo2->Clear();
          while(V[i]!="")
          {     Memo2->Text=Memo2->Text+"V["+i+"]="+V[i]+"\r\n";
                i++;
          }


          Pre1.Kill();
          Memo1->Clear();
          ::SetFocus(Memo1->Handle);

       }
}


//---------------------------------------------------------------------------

int T_Prepare::Inspect(AnsiString Instring)
{
        AnsiString Temp;
        int counter=0,i,j;


    // Make a filter with blankspace and binary operation
        for(i=1;i<=Instring.Length();i++)
        {

            if(Instring[i]==32)
               {Application->MessageBox("No Blank allowed","ERROR",MB_ICONSTOP);return 0;}
            else if(Instring[i]=='&'||Instring[i]=='|'||Instring[i]=='>')
                    Temp+='&';
            else
                 Temp+=Instring[i];
        }

    // Valid Inspect processing using these rules
        if(Instring=="")
           {Application->MessageBox("Input String Empty","ERROR",MB_ICONSTOP);return 0;}
        if(Instring[1]=='&'||Instring[1]=='|'||Instring[1]=='>'||Instring[1]==')')
           {Application->MessageBox("First Letter Illegal ","ERROR",MB_ICONSTOP);return 0;}

        for(int i=1;i<=Temp.Length()-1;i++)
        {
            if(Temp[i]=='(')
               counter++;
            if(Temp[i]==')')
               counter--;
            if(counter<0)
              {Application->MessageBox("Illegal Brackets Order ","ERROR",MB_ICONSTOP);return 0;}
            if(Temp[i]>=123 || Temp[i]<=31)
              {Application->MessageBox("Contain Illegal Letter ","ERROR",MB_ICONSTOP);return 0;}
            if(Temp[i]=='('&&Temp[i+1]==')')
              {Application->MessageBox("Empty Brackets","ERROR ",MB_ICONSTOP);return 0;}
            if(Temp[i]==')'&&Temp[i+1]=='(')
              {Application->MessageBox("Missing Operation Between Brackets ","ERROR",MB_ICONSTOP);return 0;}
            if((Temp[i]=='('&&Temp[i+1]=='&')||(Temp[i]=='&'&&Temp[i+1]==')')||(Temp[i]=='&'&&Temp[i+1]=='&'))
              {Application->MessageBox("Missing Expression Between Brackets and Operations ","ERROR",MB_ICONSTOP);return 0;}
            if((Temp[i]=='!'&&Temp[i+1]=='&')||(Temp[i]=='!'&&Temp[i+1]==')'))
              {Application->MessageBox("Illegal Inverse Operation ","ERROR",MB_ICONSTOP);return 0;}
            if(Temp[i]!='&'&&Temp[i]!='('&&Temp[i]!='!'&&Temp[i+1]=='!')
              {Application->MessageBox("Illegal Inverse Operation ","ERROR",MB_ICONSTOP);return 0;}
            if((Temp[i]!='!'&&Temp[i]!='&'&&Temp[i]!='('&&Temp[i+1]=='(')||(Temp[i+1]!=')'&&Temp[i+1]!='&'&&Temp[i]==')'))
              {Application->MessageBox("Missing Operation Between Letter and Operation ","ERROR",MB_ICONSTOP);return 0;}
        }

        j=Temp.Length();
        if(Temp[j]=='('||Temp[j]=='&'||Temp[j]=='!')
          {Application->MessageBox("Last Letter Illegal ","ERROR",MB_ICONSTOP);return 0;}
        if(Temp[j]==')')
           counter--;
        if(counter!=0)
          {Application->MessageBox("Missing Bracket '('or')'","ERROR",MB_ICONSTOP);return 0;}

        return 1;
}

//---------------------------------------------------------------------------


void  T_Prepare::Polish(AnsiString Instring)
{
       int i,flag=1;  // flag=1 mean last-char is Letter
       int tag,tag2;
       AnsiString Keep="";

       T_Stack s1;


       V[1]="(";V[2]=")";V[3]="!";V[4]=">";V[5]="|";V[6]="&";

       for (i=1;i<=Instring.Length();i++)
       {

           if(Instring[i]=='!'|| Instring[i]=='|'|| Instring[i]=='&'|| Instring[i]=='>'||Instring[i]=='('||Instring[i]==')')
           {     if(flag==1&&Keep!="")
                {       tag=repeat(Keep);
                        n1.Append(tag);
                        Keep="";
                        flag=0;
                }
           }

           else
           {    Keep=Keep+Instring[i];
                flag=1;
           }
           if(Instring[i]=='!')
           {    if(s1.Peek()!=3)s1.Push(3);
                else s1.Pop();
           }
           if(Instring[i]=='>')
           {    while(s1.Peek()==3||s1.Peek()==4||s1.Peek()==5||s1.Peek()==6)
                        {n1.Append(s1.Pop());}
                s1.Push(4);
           }
           if(Instring[i]=='|')
           {    while(s1.Peek()==5||s1.Peek()==6||s1.Peek()==3)
                        {n1.Append(s1.Pop());}
                s1.Push(5);
           }
           if(Instring[i]=='&')
           {    while(s1.Peek()==5||s1.Peek()==6||s1.Peek()==3)
                        {n1.Append(s1.Pop());}
                s1.Push(6);
           }
           if(Instring[i]=='(')
                   s1.Push(1);
           if(Instring[i]==')')
           {    while(s1.Peek()!=1)
                        {n1.Append(s1.Pop());}
                s1.Pop();
           }

        }

       tag=repeat(Keep);
       if(Keep!="")
                {n1.Append(tag);}
       tag2=s1.Pop();
       while(tag2!=-1)
       {        n1.Append(tag2);
                tag2=s1.Pop();
       }
       if(Form1->RadioGroup1->ItemIndex==1)
          n1.Append(3);


}
//------------------------------------------------------------------------
T_node *T_Prepare::Semantic()
{
        T_Stack s2;
        int i,t,temp,temp1,temp2;
        T_node *point,*q;

   //////////////Do Semantic Analysis with '>'//////////////
        point=n1.Head()->link;
        t=1;
            while(point->link!=NULL)
             {
                 if(abs(point->num)>=7)
                    s2.Push(t);
                 else if(point->num==3)
                    {s2.Pop();
                     s2.Push(t);
                    }
                 else if(point->num==5 ||point->num==6)
                    {s2.Pop();s2.Pop();
                     s2.Push(t);
                    }
                 else if(point->num==4)
                    {point->num=5;
                     s2.Pop();
                     temp=s2.Pop();
                     n1.Insert(temp+1,3);
                     t=t+1;
                     s2.Push(t);
                    }
                 point=point->link;
                 t++;
              }

                 if(abs(point->num)>=7)
                    s2.Push(t);
                 else if(point->num==3)
                    {s2.Pop();
                     s2.Push(t);
                    }
                 else if(point->num==5 ||point->num==6)
                    {s2.Pop();s2.Pop();
                     s2.Push(t);
                    }
                 else if(point->num==4)
                    {point->num=5;
                     s2.Pop();
                     temp=s2.Pop();
                     n1.Insert(temp+1,3);
                     t=t+1;
                     s2.Push(t);
                    }

      //////Do Semantic Analysis with '!'//////////////
        point=q=n1.Head()->link;
        t=1;
        s2.do_empty();
        while(q->link!=NULL &&point!=NULL)
             {
                 if(abs(point->num)>=7)
                    {s2.Push(t);
                     q=point;
                     point=point->link;
                     t++;
                    }
                 else if(point->num==5 ||point->num==6)
                    {temp1=s2.Pop();
                     temp2=s2.Pop();
                     s2.Push(t);
                     q=point;
                     point=point->link;
                     t++;
                    }
                 else if(point->num==3)
                    { temp=s2.Peek();
                      if(abs(n1.Read(temp))>=7)
                       {
                         n1.Inverse(temp);
                         q=point;
                         point=point->link;
                         n1.Delete(t);
                       }
                      else
                        {n1.Inverse(temp);
                         n1.Insert(temp1+1,3);
                         n1.Insert(temp2+1,3);
                         n1.Delete(t+2);
                         point=q=n1.Head()->link;
                         t=1;
                         s2.do_empty();
                        }
                    }
              }

      point=n1.Head()->link;
      return point;

}

//---------------------------------------------------------------------------

void T_Prepare::Plot(T_node *hh)  //hh=head->link;
{
        T_Stack  S3;
        int f_Letter=0,f_and=0;
        int position=1;
        int b;
        T_node *p,*q;
        S3.do_empty();
        p=hh;