unit3my.cpp

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

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

#include <vcl.h>
#pragma hdrstop

#include "Unit3my.h"
//---------------------------------------------------------------------------
#pragma package(smart_init)
#pragma resource "*.dfm"
TForm3 *Form3;
//---------------------------------------------------------------------------
__fastcall TForm3::TForm3(TComponent* Owner)
        : TForm(Owner)
{
}
//---------------------------------------------------------------------------
void __fastcall TForm3::Button1Click(TObject *Sender)
{
         Form3->Close();
}
//---------------------------------------------------------------------------

void __fastcall TForm3::FormShow(TObject *Sender)
{
      PaintBox1->Canvas->Brush->Color=clBtnFace;
      PaintBox1->Canvas->Font->Color=clRed;
      PaintBox1->Canvas->Font->Size=13;
      PaintBox1->Canvas->TextOutA(115,0,"- - -RULES- - -");
      PaintBox1->Canvas->Font->Color=clBtnText;
      PaintBox1->Canvas->Font->Size=11;
      PaintBox1->Canvas->TextOutA(10,25,"(1) The word can be formed with any visual char in ASCII.");
      PaintBox1->Canvas->TextOutA(10,45,"(2) The longest word should be not more than 200.");
      PaintBox1->Canvas->TextOutA(10,65,"(3) Be sure choose the type of WFF which you input.");
      PaintBox1->Canvas->TextOutA(10,85,"(4) Clicking 'submit',it will convert the WFF into");
      PaintBox1->Canvas->TextOutA(30,105,"corresponding clause form.");
      PaintBox1->Canvas->TextOutA(10,125,"(5) Clicking 'start',it will begin to resolution.");
      PaintBox1->Canvas->Font->Color=clRed;
      PaintBox1->Canvas->Font->Size=13;
      PaintBox1->Canvas->TextOutA(105,155,"- - -PRINCIPLE- - -");
      PaintBox1->Canvas->Font->Color=clBtnText;
      PaintBox1->Canvas->Font->Size=11;
      PaintBox1->Canvas->TextOutA(10,180,"(1) Polish");
      PaintBox1->Canvas->TextOutA(30,200,"'Polish' is the first principle in our algorithm.");
      PaintBox1->Canvas->TextOutA(30,220,"We use 'Polish' to convert the WFF into ClAUSES.");
      PaintBox1->Canvas->TextOutA(10,240,"(2) Resolution");
      PaintBox1->Canvas->TextOutA(30,260,"Resolution is the second principle in ou algorithm.");
      PaintBox1->Canvas->TextOutA(30,280,"We use it to judge whether the WFF is satiable.");
      PaintBox1->Canvas->TextOutA(30,300,"a. Combine the clause from S(original clauses set) into");
      PaintBox1->Canvas->TextOutA(45,320,"a single set of clauses.");
      PaintBox1->Canvas->TextOutA(30,340,"b. Interatively apply resolution to the clauses in S and");
      PaintBox1->Canvas->TextOutA(45,360,"add the resolvent to S until either:");
      PaintBox1->Canvas->TextOutA(45,380,"No more new resolvent can be generated.");
      PaintBox1->Canvas->TextOutA(45,400,"The empty clauses has been reduced.");
}
//---------------------------------------------------------------------------