unit2my.cpp

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

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

#include <vcl.h>
#pragma hdrstop

#include "Unit2my.h"
//---------------------------------------------------------------------------
#pragma package(smart_init)
#pragma resource "*.dfm"
TForm2 *Form2;
//---------------------------------------------------------------------------
__fastcall TForm2::TForm2(TComponent* Owner)
        : TForm(Owner)
{
}

void __fastcall TForm2::FormShow(TObject *Sender)
{
       int i,up,down;
       int flag;



       for(i=0;i<500;i++)
       {        P[i][0]=0;P[i][1]=0;
       }
       i=0;
       while(S[i][0]!=0&&i<500)
       {        i++;}
       h[0]=i-1;

       Form2->D_single(0);
       Form2->D_del(0);
       Form2->D_alltrue(0);
       Form2->D_same(0);
       Form2->D_del(0);
       Form2->Display(0);

       if(h[0]<=0)
       {       Form2->Memo1->Text=Form2->Memo1->Text+"No Empty-Clause exist ,Input WFF can be Satisfied\r\n";
               return;
       }
       for(up=0;up<200&&h[up]<500;up++)
       {

                flag=Form2->Resolute(up);
                down=up+1;
                if(flag!=0)
                {       Form2->Display(down);
                        Form2->Memo1->Text=Form2->Memo1->Text+"S["+h[down]+"]=S["+P[h[down]][0]+"]+S["+P[h[down]][1]+"]=NULL\r\n";
                        Form2->Memo1->Text=Form2->Memo1->Text+"EMPTY CLAUSE ARE GENERATED ,INPUT WFF DISSATISFIED\r\n";
                        return;
                }


                if(h[down]==h[up])
                {
                        Form2->Display(up);
                        Form2->Memo1->Text=Form2->Memo1->Text+"NO MORE APODOSIS GENERATED ,INPUT WFF CAN BE SATISFIED\r\n";
                        return;
                }
                else
                {
                        Form2->D_alltrue(down);
                        Form2->D_contain(down);
                        Form2->D_same(down);
                        Form2->D_del(down);
                        Form2->Display(down);
                }
       }
       Form2->Memo1->Text=Form2->Memo1->Text+"Out of The Iterative Range,Illation Abort\r\n";
       Form2->Closer->SetFocus();

}
//---------------------------------------------------------------------------



//---------------------------------------------------------------------------
void __fastcall TForm2::CloserClick(TObject *Sender)
{
        Form2->Close();
}

//---------------------------------------------------------------------------
int TForm2::Resolute(int step)
{
        int i,j,ki,kj,p,pnew;
        int down;
        down=step+1;
        h[down]=h[step];
        if(step==0)
        {       for(i=0;i<=h[0];i++)
                        for(j=i+1;j<=h[0];j++)
                                for(ki=0;S[i][ki]!=0&&ki<200;ki++)
                                        for(kj=0;S[j][kj]!=0&&kj<200;kj++)
                                        {       if(S[i][ki]==S[j][kj]*(-1))
                                                {       h[1]=h[1]+1;
                                                        P[h[1]][0]=i;
                                                        P[h[1]][1]=j;
                                                        pnew=0;
                                                        S[h[1]][0]=0;
                                                        for(p=0;S[i][p]!=0&&p<200;p++)
                                                                if(p!=ki)
                                                                {       S[h[1]][pnew]=S[i][p];
                                                                        pnew++;
                                                                }
                                                        for(p=0;S[j][p]!=0&&p<200;p++)
                                                                if(p!=kj)
                                                                {       S[h[1]][pnew]=S[j][p];
                                                                        pnew++;
                                                                }
                                                        if(S[h[1]][0]==0)return 1;
                                                }
                                        }
        }
        else
        {       for(i=0;i<=h[step-1];i++)
                        for(j=h[step-1]+1;j<=h[step];j++)
                                for(ki=0;S[i][ki]!=0&&ki<200;ki++)
                                        for(kj=0;S[j][kj]!=0&&kj<200;kj++)
                                        {       if(S[i][ki]==S[j][kj]*(-1))
                                                {       h[down]=h[down]+1;
                                                        P[h[down]][0]=i;
                                                        P[h[down]][1]=j;
                                                        pnew=0;
                                                        S[h[down]][0]=0;
                                                        for(p=0;S[i][p]!=0&&p<200;p++)
                                                                if(p!=ki)
                                                                {       S[h[down]][pnew]=S[i][p];
                                                                        pnew++;
                                                                }
                                                        for(p=0;S[j][p]!=0&&p<200;p++)
                                                            if(p!=kj)
                                                                {       S[h[down]][pnew]=S[j][p];
                                                                        pnew++;
                                                                }
                                                        if(S[h[down]][0]==0)return 1;
                                                }
                                        }
        }

        return 0;
}

//---------------------------------------------------------------------------
void TForm2::Display(int step)
{
        int i,j;

        if(step==0)
        {       Form2->Memo1->Clear();
                for(i=0;S[i][0]!=0&i<500;i++)
                {
                        if(S[i][0]>=0)
                        {       Form2->Memo1->Text=Form2->Memo1->Text+"S["+i+"]="+V[S[i][0]];}
                        else
                        {       Form2->Memo1->Text=Form2->Memo1->Text+"S["+i+"]=～"+V[abs(S[i][0])];}
                        for(j=1;S[i][j]!=0&&j<200;j++)
                        {       if(S[i][j]>=0)
                                {       Form2->Memo1->Text=Form2->Memo1->Text+"∨"+V[S[i][j]];}
                                else
                                {       Form2->Memo1->Text=Form2->Memo1->Text+"∨～"+V[abs(S[i][j])];}
                        }
                        Form2->Memo1->Text=Form2->Memo1->Text+"\r\n";

                }
         }
         else
         {      for(i=h[step-1]+1;i<=h[step];i++)
                {
                        if(S[i][0]>=0)
                        {       Form2->Memo1->Text=Form2->Memo1->Text+"S["+i+"]=S["+P[i][0]+"]+S["+P[i][1]+"]="+V[S[i][0]];}
                        else
                        {       Form2->Memo1->Text=Form2->Memo1->Text+"S["+i+"]=S["+P[i][0]+"]+S["+P[i][1]+"]=～"+V[abs(S[i][0])];}
                        for(j=1;S[i][j]!=0&&j<200;j++)
                                if(S[i][j]>=0)
                                {       Form2->Memo1->Text=Form2->Memo1->Text+"∨"+V[S[i][j]];}
                                else
                                {       Form2->Memo1->Text=Form2->Memo1->Text+"∨～"+V[abs(S[i][j])];}
                        Form2->Memo1->Text=Form2->Memo1->Text+"\r\n";
                }
         }
   
         Form2->Memo1->Text=Form2->Memo1->Text+"\r\n*************************************************************************************\r\n";

}



void __fastcall TForm2::SaveClick(TObject *Sender)
{
      if(SaveDialog1->Execute())
      {         Memo1->Lines->SaveToFile(SaveDialog1->FileName);
      }
      

}
//---------------------------------------------------------------------------