unit2my.h

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

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

#ifndef Unit2myH
#define Unit2myH
//---------------------------------------------------------------------------
#include <Classes.hpp>
#include <Controls.hpp>
#include <StdCtrls.hpp>
#include <Forms.hpp>
#include <ComCtrls.hpp>
#include <ExtCtrls.hpp>
#include <Dialogs.hpp>
//---------------------------------------------------------------------------
class TForm2 : public TForm
{
__published:	// IDE-managed Components
        TButton *Closer;
        TButton *Save;
        TMemo *Memo1;
        TBevel *Bevel1;
        TSaveDialog *SaveDialog1;
        void __fastcall CloserClick(TObject *Sender);
        void __fastcall FormShow(TObject *Sender);
        void __fastcall SaveClick(TObject *Sender);
private:	 
public:



        __fastcall TForm2(TComponent* Owner);
        void D_single(int);
        void D_alltrue(int);
        void D_contain(int);
        void D_same(int);
        void Display(int);
        void D_del(int);
        int  Resolute(int);
};
extern      int  P[500][2];
extern      AnsiString V[200];
extern      int S[500][200];
extern      int h[200];

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

void TForm2::D_single(int step)
{
     int i,j,begin;
     int ti,tj,f;
     if(step==0)  begin=0;                 
     else
        begin=h[step-1]+1;
     for(i=begin;i<=h[step];i++)
     {
         for(ti=0;S[i][ti]!=0&&ti<200;ti++)
         {
               f=0;
               for(j=begin;j<=h[step]&&f!=1;j++)
               {
                   if(j==i)  continue;
                   for(tj=0;S[j][tj]!=0&&tj<200&&f!=1;tj++)
                       if(S[j][tj]==S[i][ti]*(-1))
                          f=1;
               }
               if(f!=1)
               {
                   P[i][0]=-1;
                   break;
               }
         }
     }
}
//---------------------------------------------------------------------------
void TForm2::D_alltrue(int step)
{
     int i,j,k,ik,j0,flag,begin;
     if(step==0)  begin=0;
     else
        begin=h[step-1]+1;
     for(ik=begin;ik<=h[step];ik++)
     {
         j0=0; flag=0;
         while(S[ik][j0]!=0&&j0<200)
               j0++;
         for(i=0;i<j0&&flag!=1;i++)           //all ture
         {
             for(j=i+1;j<j0&&flag!=1;j++)
             {
                 if(S[ik][i]==S[ik][j]*(-1))
                 {
                    P[ik][0]=-1;
                    flag=1;
                 }
             }
         }
         if(flag==1)
            continue;
 ////////////////////////////////////
         for(i=0;i<j0;i++)
         {
             for(j=i+1;j<j0;j++)
             {
                 if(S[ik][j]==S[ik][i])
                    S[ik][j]=0;
             }
         }
         for(i=0;i<j0;i++)
         {
             if(S[ik][i]==0)
             {
                for(j=i;j<j0;j++)
                    S[ik][j]=S[ik][j+1];
                j0--;i--;
             }
         }                                                  
     }
}
//---------------------------------------------------------------------------
void TForm2::D_contain(int step)
{
     int i,ik,jk,flag,begin,k;
     if(step==0)  begin=0;
     else
        begin=h[step-1]+1;
     for(ik=begin;ik<=h[step];ik++)
     {
         for(jk=begin;jk<=h[step];jk++)
         {
             k=0;
             if(jk==ik)  continue;
             for(i=0;S[jk][i]!=0&&i<200;i++)     //inclued
             {
                 flag=0;
                 if(S[ik][k]==S[jk][i])
                 {   k++;  flag=1; }
                 if(flag==1)
                 {   i=-1; continue; }
             }
             if(S[ik][k]==0)
             {
                if(k==i)
                   if(ik<jk) continue;
                P[ik][0]=-1;
                break;
             }
         }
     }
}
//---------------------------------------------------------------------------
void TForm2::D_same(int step)
{
    int i,ik,jk,k,flag,begin;
    if(step==0)
       begin=0;
    else
       begin=h[step-1]+1;
    for(ik=begin;ik<=h[step];ik++)
     {
         for(jk=0;jk<=h[step-1];jk++)
         {
             k=0;
             for(i=0;S[jk][i]!=0&&i<200;i++)
             {
                 flag=0;
                 if(S[ik][k]==S[jk][i])
                 {   k++;  flag=1; }
                 if(flag==1)
                 {   i=-1; continue; }
             }
             if(S[ik][k]==0&&k==i&&ik>jk)
             {   P[ik][0]=-1; break; }
         }
     }
}


//---------------------------------------------------------------------------
void TForm2::D_del(int step)
{
                int k,m,t,begin,i=0,temp,temp0,temp1;
                if(step==0)  begin=0;
                else
                    begin=h[step-1]+1;
                i=begin;                              
                for(k=begin;k<=h[step];k++)
                    if(P[k][0]==-1)
                    {
                       for(m=0;S[k][m]!=0&&m<200;m++)
                           S[k][m]=0;
                       P[k][0]=0;
                       P[k][1]=0;       
                    }
                for(k=begin;k<=h[step];k++)
                {
                    if(S[k][0]==0) continue;
                    else
                    {
                       for(t=0;S[k][t]!=0&&t<200;t++)
                       { temp=S[k][t];S[k][t]=0; S[i][t]=temp;}
                         temp0=P[k][0];P[k][0]=0;P[i][0]=temp0;
                         temp1=P[k][1];P[k][1]=0;P[i][1]=temp1; 
                       i++;
                     }
                }
                h[step]=i-1;
}



//---------------------------------------------------------------------------
extern PACKAGE TForm2 *Form2;
//---------------------------------------------------------------------------
#endif