demo_pascal_theorem.htm

来自「Delphi脚本控件」· HTM 代码 · 共 626 行 · 第 1/2 页

HTM
626 行
字号
12
      C.Dump;
  <font color="blue"><b>end</b></font>;
  writeln(<font color="Red">'Contradiction: '</font>, NX, <font color="Red">' '</font>, NY);
  Clauses[HC].Dump;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>procedure</b></font> TClauseList.Dump;
<font color="blue"><b>var</b></font>
  I: Integer;
<font color="blue"><b>begin</b></font>
  <font color="blue"><b>for</b></font> I:=0 <font color="blue"><b>to</b></font> Count - 1 <font color="blue"><b>do</b></font>
    Clauses[I].Dump;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>procedure</b></font> TClauseList.AddClauses(L: TClauseList);
<font color="blue"><b>var</b></font>
  I: Integer;
<font color="blue"><b>begin</b></font>
  <font color="blue"><b>for</b></font> I:=0 <font color="blue"><b>to</b></font> L.Count - 1 <font color="blue"><b>do</b></font>
    fClauses.Add(L[I]);
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> Contradict(A, U, V: TClauseList): boolean;
<font color="blue"><b>var</b></font>
  I, J: Integer;
  UI, VJ, R: TClause;
  Name: <font color="blue"><b>String</b></font>;
<font color="blue"><b>begin</b></font>
  result := false;
  <font color="blue"><b>for</b></font> I := 0 <font color="blue"><b>to</b></font> U.Count - 1 <font color="blue"><b>do</b></font>
  <font color="blue"><b>begin</b></font>
    UI := U[I];
    Name := UI.Name(0);
    <font color="blue"><b>for</b></font> J := 0 <font color="blue"><b>to</b></font> V.Count - 1 <font color="blue"><b>do</b></font>
    <font color="blue"><b>begin</b></font>
      VJ := V[J];
      <font color="blue"><b>if</b></font> Name = VJ.Name(0) <font color="blue"><b>then</b></font>
      <font color="blue"><b>begin</b></font>
        UI.Rename(AX);
        VJ.Rename(AY);
        result := Unify(2, UI.E[0], VJ.E[0]);
        <font color="blue"><b>if</b></font> result <font color="blue"><b>then</b></font>
        <font color="blue"><b>begin</b></font>
          R := TClause.Create(<font color="blue"><b>nil</b></font>);
          R.PutResolvent(UI, VJ, 0, 0);
          writeln(<font color="Red">'Resolvent:'</font>);
          R.Rename(AX);
          R.Dump();
          
          A.Add(R);

          <font color="blue"><b>Exit</b></font>;
        <font color="blue"><b>end</b></font>;
      <font color="blue"><b>end</b></font>;
    <font color="blue"><b>end</b></font>;
  <font color="blue"><b>end</b></font>;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> STest(S: TClauseList; U: TClause): boolean;
<font color="blue"><b>var</b></font>
  Name: <font color="blue"><b>String</b></font>;
  I: Integer;
  SI: TClause;
<font color="blue"><b>begin</b></font>
  result := false;
  Name := U.Name(0);
  <font color="blue"><b>for</b></font> I := 0 <font color="blue"><b>to</b></font> S.Count - 1 <font color="blue"><b>do</b></font>
  <font color="blue"><b>begin</b></font>
    SI := S[I];
    <font color="blue"><b>if</b></font> Name = SI.Name(0) <font color="blue"><b>then</b></font>
    <font color="blue"><b>begin</b></font>
      SI.Rename(ArrConst);
      U.Rename(AX);
      result := Unify(2, SI.E[0], U.E[0]);
      <font color="blue"><b>if</b></font> result <font color="blue"><b>then</b></font>
        <font color="blue"><b>Exit</b></font>;
    <font color="blue"><b>end</b></font>;
  <font color="blue"><b>end</b></font>;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> GUnit(A, S1, S2, W: TClauseList; C: TClause): boolean;
<font color="blue"><b>var</b></font>
  P, S, POS, NEG: TList;
  I, J: Integer;
  U, R: TClause;
  Sign, Name: <font color="blue"><b>String</b></font>;
  Stack: TStack;
<font color="blue"><b>begin</b></font>
  POS := TClauseList.Create;
  NEG := TClauseList.Create;
  Stack := TStack.Create;

  <font color="blue"><b>try</b></font>
    Stack.Push(C);
    
    <font color="blue"><b>repeat</b></font>
      C := Stack.Pop;
      
      <font color="blue"><b>for</b></font> I := 0 <font color="blue"><b>to</b></font> W.Count - 1 <font color="blue"><b>do</b></font>
      <font color="blue"><b>begin</b></font>
        U := W[I];
        <font color="blue"><b>if</b></font> U.Number < C.NX <font color="blue"><b>then</b></font>
        <font color="blue"><b>begin</b></font>
          Sign := U.Sign(0);
          Name := U.Name(0);
          <font color="blue"><b>for</b></font> J:=0 <font color="blue"><b>to</b></font> C.length - 1 <font color="blue"><b>do</b></font>
            <font color="blue"><b>if</b></font> (Sign <> C.Sign(J)) <font color="blue"><b>and</b></font> (Name = C.Name(J)) <font color="blue"><b>then</b></font>
            <font color="blue"><b>begin</b></font>
              U.Rename(AX);
              C.Rename(AY);

              <font color="blue"><b>if</b></font> Unify(1, U.E[0], C.E[J]) <font color="blue"><b>then</b></font>
              <font color="blue"><b>begin</b></font>
                R := TClause.Create(<font color="blue"><b>nil</b></font>);
                R.PutResolvent(U, C, 0, J);

                writeln(<font color="Red">'Resolvent:'</font>);
                R.Rename(AX);
                R.Dump();
                
                A.Add(R);

                <font color="blue"><b>if</b></font> R.length = 1 <font color="blue"><b>then</b></font>
                <font color="blue"><b>begin</b></font>
                  <font color="blue"><b>if</b></font> R.Sign(0) = <font color="Red">'+'</font> <font color="blue"><b>then</b></font>
                  <font color="blue"><b>begin</b></font>
                    S := S1;
                    P := POS;
                  <font color="blue"><b>end</b></font>
                  <font color="blue"><b>else</b></font>
                  <font color="blue"><b>begin</b></font>
                    S := S2;
                    P := NEG;
                  <font color="blue"><b>end</b></font>;
                  <font color="blue"><b>if</b></font> (<font color="blue"><b>not</b></font> STest(S, R)) <font color="blue"><b>and</b></font> (<font color="blue"><b>not</b></font> STest(P, R)) <font color="blue"><b>then</b></font>
                    P.Add(R);
                <font color="blue"><b>end</b></font>
                <font color="blue"><b>else</b></font>
                  Stack.Push(R);
              <font color="blue"><b>end</b></font>;
            <font color="blue"><b>end</b></font>;
        <font color="blue"><b>end</b></font>;
      <font color="blue"><b>end</b></font>;
    <font color="blue"><b>until</b></font> Stack.Count = 0;

    result := Contradict(A, S1, NEG);
    <font color="blue"><b>if</b></font> <font color="blue"><b>not</b></font> result <font color="blue"><b>then</b></font>
    <font color="blue"><b>begin</b></font>
      result := Contradict(A, S2, POS);
      <font color="blue"><b>if</b></font> <font color="blue"><b>not</b></font> result <font color="blue"><b>then</b></font>
      <font color="blue"><b>begin</b></font>
        S1.AddClauses(POS);
        S2.AddClauses(NEG);
      <font color="blue"><b>end</b></font>;
    <font color="blue"><b>end</b></font>;
  <font color="blue"><b>finally</b></font>
    POS.Free;
    NEG.Free;
    Stack.Free;
  <font color="blue"><b>end</b></font>;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> TRU(A: TClauseList; SupportSet: Variant; TryNumber: Integer): boolean;
<font color="blue"><b>var</b></font>
  S, S1, S2, S3: TClauseList;
  I, J, K, L, N: Integer;
  W: TList;
  C: TClause;
<font color="blue"><b>begin</b></font>
  S1 := TClauseList.Create;
  S2 := TClauseList.Create;
  S3 := TClauseList.Create;
  W := TList.Create;

  <font color="blue"><b>try</b></font>
    <font color="blue"><b>for</b></font> I:=0 <font color="blue"><b>to</b></font> A.Count - 1 <font color="blue"><b>do</b></font>
    <font color="blue"><b>begin</b></font>
      C := A[I];
      <font color="blue"><b>if</b></font> C.length = 1 <font color="blue"><b>then</b></font>
      <font color="blue"><b>begin</b></font>
        <font color="blue"><b>if</b></font> C.Sign(0) = <font color="Red">'+'</font> <font color="blue"><b>then</b></font>
          S1.Add(C)
        <font color="blue"><b>else</b></font>
          S2.Add(C);
      <font color="blue"><b>end</b></font>
      <font color="blue"><b>else</b></font>
      <font color="blue"><b>begin</b></font>
        S3.Add(C);
        <font color="blue"><b>if</b></font> SupportSet[I] <> <font color="blue"><b>nil</b></font> <font color="blue"><b>then</b></font>
        <font color="blue"><b>begin</b></font>
          S := TClauseList.Create;
          <font color="blue"><b>for</b></font> J:=0 <font color="blue"><b>to</b></font> SupportSet[I].length - 1  <font color="blue"><b>do</b></font>
          <font color="blue"><b>begin</b></font>
            C := SupportSet[I][J];
            S.Add(C);
          <font color="blue"><b>end</b></font>;
          W.Add(S);
        <font color="blue"><b>end</b></font>;
      <font color="blue"><b>end</b></font>;
    <font color="blue"><b>end</b></font>;

    result := Contradict(A, S1, S2);

    <font color="blue"><b>if</b></font> result <font color="blue"><b>then</b></font>
      <font color="blue"><b>Exit</b></font>;

    K := 0;

    <font color="blue"><b>for</b></font> I:=0 <font color="blue"><b>to</b></font> TryNumber - 1 <font color="blue"><b>do</b></font>
    <font color="blue"><b>begin</b></font>
      N := A.Count;
      result := GUnit(A, S1, S2, W[K], S3[K]);

      <font color="blue"><b>if</b></font> result <font color="blue"><b>then</b></font>
        <font color="blue"><b>Exit</b></font>;

      <font color="blue"><b>if</b></font> A.Count > N <font color="blue"><b>then</b></font>
        <font color="blue"><b>for</b></font> J:=0 <font color="blue"><b>to</b></font> S3.Count - 1 <font color="blue"><b>do</b></font>
        <font color="blue"><b>begin</b></font>
          <font color="blue"><b>if</b></font> J = K <font color="blue"><b>then</b></font>
            W[J].Clear;

          <font color="blue"><b>for</b></font> L:=N <font color="blue"><b>to</b></font> A.Count - 1 <font color="blue"><b>do</b></font>
            <font color="blue"><b>if</b></font> A[L].length = 1 <font color="blue"><b>then</b></font>
              W[J].Add(A[L]);
        <font color="blue"><b>end</b></font>;

      Inc(K);
      <font color="blue"><b>if</b></font> K = S3.Count <font color="blue"><b>then</b></font>
        K := 0;
    <font color="blue"><b>end</b></font>;
  <font color="blue"><b>finally</b></font>
    S1.Free;
    S2.Free;
    S3.Free;
    W.Free;
  <font color="blue"><b>end</b></font>;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>const</b></font>
  A = <font color="Red">'A'</font>;
  D = <font color="Red">'D'</font>;
  F = <font color="Red">'F'</font>;
  H = <font color="Red">'H'</font>;
  L = <font color="Red">'L'</font>;
  P = <font color="Red">'P'</font>;
  X = <font color="Red">'X'</font>;
  Y = <font color="Red">'Y'</font>;
<font color="blue"><b>var</b></font>
  I, N: Integer;
  Clauses: TClauseList;
  SupportSet: TList;

<font color="blue"><b>procedure</b></font> AddClause(E);
<font color="blue"><b>begin</b></font>
  Clauses.Add(TClause.Create(E));
<font color="blue"><b>end</b></font>;

<font color="blue"><b>begin</b></font>
  Num := 0;
  Clauses := TClauseList.Create;
  SupportSet := TList.Create;

  AddClause([[<font color="Red">'+'</font>,L,X,[F,X]]                      ]);
  AddClause([[<font color="Red">'-'</font>,L,X,X]                          ]);
  AddClause([[<font color="Red">'-'</font>,L,X,Y],[<font color="Red">'-'</font>,L,Y,X]              ]);
  AddClause([[<font color="Red">'-'</font>,D,X,[F,Y]],[<font color="Red">'+'</font>,L,Y,X]          ]);
  AddClause([[<font color="Red">'+'</font>,P,X],[<font color="Red">'+'</font>,D,[H,X],X]            ]);
  AddClause([[<font color="Red">'+'</font>,P,X],[<font color="Red">'+'</font>,P,[H,X]]              ]);
  AddClause([[<font color="Red">'+'</font>,P,X],[<font color="Red">'+'</font>,L,[H,X],X]            ]);
  AddClause([[<font color="Red">'-'</font>,P,X],[<font color="Red">'-'</font>,L,A,X],[<font color="Red">'+'</font>,L,[F,A],X]]);

  <font color="blue"><b>for</b></font> I:=0 <font color="blue"><b>to</b></font> Clauses.Count - 1 <font color="blue"><b>do</b></font>
  <font color="blue"><b>begin</b></font>
    <font color="blue"><b>if</b></font> I >= 2 <font color="blue"><b>then</b></font>
      SupportSet.Add([Clauses[0], Clauses[1]])
    <font color="blue"><b>else</b></font>
      SupportSet.Add(<font color="blue"><b>nil</b></font>);
  <font color="blue"><b>end</b></font>;

  writeln(<font color="Red">'Source clauses:'</font>);
  Clauses.Dump;

  writeln(<font color="Red">'-------------------------------'</font>);
  writeln(<font color="Red">'Theorem proving'</font>);
  writeln(<font color="Red">'Unit binary resolution'</font>);
  writeln(<font color="Red">'-------------------------------'</font>);

  writeln(<font color="Red">'Theorem :'</font>);
  writeln(<font color="Red">'The set of prime numbers is infinite'</font>);

  N := Clauses.Count;
  TRU(Clauses, SupportSet, 20);

  Clauses.Output(N);
  
  <font color="blue"><b>for</b></font> I:=0 <font color="blue"><b>to</b></font> Clauses.Count - 1 <font color="blue"><b>do</b></font>
    Clauses[I].Free;
  Clauses.Free;
  SupportSet.Free;
<font color="blue"><b>end</b></font>.
</pre>
</blockquote>

<p>
<HR>
<font size = 1 color ="gray">
Copyright &copy; 1999-2005
VIRT Laboratory. All rights reserved.
</font>
</body>
</html>
12

demo_pascal_theorem.htm - 源码说明

本页面展示了「Delphi脚本控件」中的 demo_pascal_theorem.htm 源码文件，采用 HTM 编程语言编写，共 626 行代码。您可以在线阅读完整代码内容，也可以返回资源详情页下载完整源码包进行本地学习和开发。

虫虫下载站收录了大量与Delphi相关的技术资源，包括源代码、技术文档、电路图等，是电子工程师和嵌入式开发者的专业学习平台。

⌨️ 快捷键说明

复制代码Ctrl + C
搜索代码Ctrl + F
全屏模式F11
增大字号Ctrl + =
减小字号Ctrl + -
显示快捷键?