demo_pascal_theorem.htm

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

HTM
626 行
字号
12
<html>
<head>
<link rel=stylesheet type="text/css" href="styles.css">
</head>

<body>

<h3>
LISPPA: Mechanical theorem proving (paxPascal).
</h3>
<hr>

// Compare with Appendix A in "Chang C.L and Lee R.C. Symbolic Logic and Mechanical Theorem Proving", Academic Press, New York, 1973. 


<blockquote>
<pre>
<font color="blue"><b>program</b></font> TheoremProving;
<font color="blue"><b>uses</b></font>
  SysUtils, Classes, Contnrs;

<font color="blue"><b>const</b></font>
  ArrConst = [<font color="Red">'$1'</font>, <font color="Red">'$2'</font>, <font color="Red">'$3'</font>, <font color="Red">'$4'</font>, <font color="Red">'$5'</font>, <font color="Red">'$6'</font>, <font color="Red">'$7'</font>, <font color="Red">'$8'</font>];
  AX       = [<font color="Red">'X1'</font>, <font color="Red">'X2'</font>, <font color="Red">'X3'</font>, <font color="Red">'X4'</font>, <font color="Red">'X5'</font>, <font color="Red">'X6'</font>, <font color="Red">'X7'</font>, <font color="Red">'X8'</font>];
  AY       = [<font color="Red">'Y1'</font>, <font color="Red">'Y2'</font>, <font color="Red">'Y3'</font>, <font color="Red">'Y4'</font>, <font color="Red">'Y5'</font>, <font color="Red">'Y6'</font>, <font color="Red">'Y7'</font>, <font color="Red">'Y8'</font>];
<font color="blue"><b>type</b></font>
  TClause = <font color="blue"><b>class</b></font>(TObject)
  <font color="blue"><b>private</b></font>
    E, Params: Variant;
    Number, NParam, NX, NY, ND: Integer;
    InProof: Boolean;
    <font color="blue"><b>procedure</b></font> CreateParams(P: Variant);
  <font color="blue"><b>public</b></font>
    <font color="blue"><b>constructor</b></font> Create(A: Variant);
    <font color="blue"><b>procedure</b></font> PutResolvent(<font color="blue"><b>const</b></font> A, B: TClause; LA, LB: Integer);
    <font color="blue"><b>procedure</b></font> Rename(L: Variant);
    <font color="blue"><b>function</b></font> Length: Integer;
    <font color="blue"><b>function</b></font> Sign(I: Integer): <font color="blue"><b>String</b></font>;
    <font color="blue"><b>function</b></font> Name(I: Integer): <font color="blue"><b>String</b></font>;
    <font color="blue"><b>procedure</b></font> Dump;
  <font color="blue"><b>end</b></font>;

  TClauseList = <font color="blue"><b>class</b></font>(TObject)
  <font color="blue"><b>private</b></font>
    fClauses: TList;
    <font color="blue"><b>function</b></font> GetClause(I: Integer): TClause;
    <font color="blue"><b>procedure</b></font> SetClause(I: Integer; Value: TClause);
  <font color="blue"><b>public</b></font>
    <font color="blue"><b>constructor</b></font> Create;
    <font color="blue"><b>destructor</b></font> Destroy; override;
    <font color="blue"><b>function</b></font> Add(C: TClause): Integer;
    <font color="blue"><b>procedure</b></font> Clear;
    <font color="blue"><b>procedure</b></font> AddClauses(L: TClauseList);
    <font color="blue"><b>function</b></font> Count: Integer;
    <font color="blue"><b>procedure</b></font> MarkTree(I, N: Integer);
    <font color="blue"><b>procedure</b></font> Output(N: Integer);
    <font color="blue"><b>procedure</b></font> Dump;
    <font color="blue"><b>property</b></font> Clauses[I: Integer]: TClause read GetClause write SetClause; <font color="blue"><b>default</b></font>;
  <font color="blue"><b>end</b></font>;
  
<font color="blue"><b>var</b></font>
  Num: Integer; // clause counter

<font color="blue"><b>function</b></font> IsCompound(<font color="blue"><b>const</b></font> Term: Variant): boolean;
<font color="blue"><b>begin</b></font>
  result := isPaxArray(Term);
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> IsVar(<font color="blue"><b>const</b></font> P: Variant): boolean;
<font color="blue"><b>begin</b></font>
  result := isString(P);
  <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>Exit</b></font>;
  result := (Ord(P) >= Ord(<font color="Red">'U'</font>)) <font color="blue"><b>and</b></font> (Ord(P) <= Ord(<font color="Red">'Z'</font>));
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> CopyTerm(A: Variant): Variant;
<font color="blue"><b>var</b></font>
  I: Integer;
  AI: Variant;
<font color="blue"><b>begin</b></font>
  result := PaxArray(A.length);
  <font color="blue"><b>for</b></font> I:=0 <font color="blue"><b>to</b></font> A.length - 1 <font color="blue"><b>do</b></font>
  <font color="blue"><b>begin</b></font>
    AI := @ A[I];
    <font color="blue"><b>if</b></font> IsCompound(AI) <font color="blue"><b>then</b></font>
      result[I] := CopyTerm(AI)
    <font color="blue"><b>else</b></font>
      result[I] := AI;
  <font color="blue"><b>end</b></font>;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> Inside(Key, Term: Variant): boolean;
<font color="blue"><b>var</b></font>
  I: Integer;
<font color="blue"><b>begin</b></font>
  <font color="blue"><b>if</b></font> IsCompound(Term) <font color="blue"><b>then</b></font>
    <font color="blue"><b>for</b></font> I:=1 <font color="blue"><b>to</b></font> Term.length - 1 <font color="blue"><b>do</b></font>
    <font color="blue"><b>begin</b></font>
      result := Inside(Key, Term[I]);
      <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>else</b></font>
    result := Key = Term;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> Unify(N: Integer; T1, T2: Variant): boolean;
<font color="blue"><b>var</b></font>
  I: Integer;
  P1, P2: Variant;
<font color="blue"><b>begin</b></font>
  result := true;
  <font color="blue"><b>for</b></font> I:=N <font color="blue"><b>to</b></font> T1.length - 1 <font color="blue"><b>do</b></font>
  <font color="blue"><b>begin</b></font>
    P1 := @ T1[I];
    P2 := @ T2[I];
    <font color="blue"><b>if</b></font> IsCompound(P1) <font color="blue"><b>and</b></font> IsCompound(P2) <font color="blue"><b>then</b></font>
      result := Unify(0, P1, P2)
    <font color="blue"><b>else</b></font> <font color="blue"><b>if</b></font> IsVar(P1) <font color="blue"><b>and</b></font> (<font color="blue"><b>not</b></font> Inside(P1, P2)) <font color="blue"><b>then</b></font>
      P1^ := @ P2^
    <font color="blue"><b>else</b></font> <font color="blue"><b>if</b></font> IsVar(P2) <font color="blue"><b>and</b></font> (<font color="blue"><b>not</b></font> Inside(P2, P1)) <font color="blue"><b>then</b></font>
      P2^ := @ P1^
    <font color="blue"><b>else</b></font>
      result := P1 = P2;
    <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>Exit</b></font>;
  <font color="blue"><b>end</b></font>;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>constructor</b></font> TClause.Create(A: Variant);
<font color="blue"><b>begin</b></font>
  <font color="blue"><b>inherited</b></font> Create;
  
  E := A;
  Num := Num + 1;
  Number := Num;
  NX := 1000;
  NY := 0;
  ND := 0;
  NParam := 0;
  Params := PaxArray(10);
  InProof := false;
  
  <font color="blue"><b>if</b></font> A <> <font color="blue"><b>nil</b></font> <font color="blue"><b>then</b></font>
    CreateParams(E);
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> TClause.Length: Integer;
<font color="blue"><b>begin</b></font>
  result := E.length;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> TClause.Sign(I: Integer): <font color="blue"><b>String</b></font>;
<font color="blue"><b>begin</b></font>
  result := E[I][0];
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> TClause.Name(I: Integer): <font color="blue"><b>String</b></font>;
<font color="blue"><b>begin</b></font>
  result := E[I][1];
<font color="blue"><b>end</b></font>;

<font color="blue"><b>procedure</b></font> TClause.CreateParams(P: Variant);
<font color="blue"><b>var</b></font>
  I, J, K: Integer;
  PI: Variant;
<font color="blue"><b>begin</b></font>
  <font color="blue"><b>for</b></font> I:=0 <font color="blue"><b>to</b></font> P.length - 1 <font color="blue"><b>do</b></font>
  <font color="blue"><b>begin</b></font>
    PI := @ P[I];
    <font color="blue"><b>if</b></font> IsCompound(PI) <font color="blue"><b>then</b></font>
      CreateParams(PI)
    <font color="blue"><b>else</b></font> <font color="blue"><b>if</b></font> IsVar(PI) <font color="blue"><b>then</b></font>
    <font color="blue"><b>begin</b></font>
      K := -1;
      <font color="blue"><b>for</b></font> J:=0 <font color="blue"><b>to</b></font> NParam - 1 <font color="blue"><b>do</b></font>
        <font color="blue"><b>if</b></font> Params[J] = PI <font color="blue"><b>then</b></font>
          K := J;
      <font color="blue"><b>if</b></font> K = -1 <font color="blue"><b>then</b></font>
      <font color="blue"><b>begin</b></font>
        K := NParam;
        Params[K] := PI;
        Inc(NParam);
      <font color="blue"><b>end</b></font>;
      P[I] := @ Params[K];
    <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>procedure</b></font> TClause.Rename(L: Variant);
<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> NParam - 1 <font color="blue"><b>do</b></font>
  <font color="blue"><b>begin</b></font>
    <font color="blue"><b>delete</b></font> Params[I];
    Params[I] := L[I];
  <font color="blue"><b>end</b></font>;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>procedure</b></font> TClause.Dump;
<font color="blue"><b>begin</b></font>
  writeln(Number,<font color="Red">'('</font>,NX,<font color="Red">','</font>,NY,<font color="Red">','</font>,ND,<font color="Red">') E='</font>,E);
<font color="blue"><b>end</b></font>;

<font color="blue"><b>procedure</b></font> TClause.PutResolvent(A, B: TClause; LA, LB: Integer);
<font color="blue"><b>var</b></font>
  I, J: Integer;
<font color="blue"><b>begin</b></font>
  E := PaxArray(A.E.length + B.E.length - 2);
  
  J := -1;
  <font color="blue"><b>for</b></font> I:=0 <font color="blue"><b>to</b></font> A.length - 1 <font color="blue"><b>do</b></font>
  <font color="blue"><b>if</b></font> I <> LA <font color="blue"><b>then</b></font>
  <font color="blue"><b>begin</b></font>
    Inc(J);
    E[J] := CopyTerm(A.E[I]);
  <font color="blue"><b>end</b></font>;

  <font color="blue"><b>for</b></font> I:=0 <font color="blue"><b>to</b></font> B.length - 1 <font color="blue"><b>do</b></font>
  <font color="blue"><b>if</b></font> I <> LB <font color="blue"><b>then</b></font>
  <font color="blue"><b>begin</b></font>
    Inc(J);
    E[J] := CopyTerm(B.E[I]);
  <font color="blue"><b>end</b></font>;

  NX := A.Number;
  NY := B.Number;
  ND := LB;
  
  CreateParams(E);
<font color="blue"><b>end</b></font>;

<font color="blue"><b>constructor</b></font> TClauseList.Create;
<font color="blue"><b>begin</b></font>
  <font color="blue"><b>inherited</b></font>;
  fClauses := TList.Create;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>destructor</b></font> TClauseList.Destroy;
<font color="blue"><b>begin</b></font>
  fClauses.Free;
  <font color="blue"><b>inherited</b></font>;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> TClauseList.GetClause(I: Integer): TClause;
<font color="blue"><b>begin</b></font>
  result := fClauses[I];
<font color="blue"><b>end</b></font>;

<font color="blue"><b>procedure</b></font> TClauseList.SetClause(I: Integer; Value: TClause);
<font color="blue"><b>begin</b></font>
  fClauses[I] := Value;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> TClauseList.Add(C: TClause): Integer;
<font color="blue"><b>begin</b></font>
  result := fClauses.Add(C);
<font color="blue"><b>end</b></font>;

<font color="blue"><b>procedure</b></font> TClauseList.Clear;
<font color="blue"><b>begin</b></font>
  fClauses.Clear;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>function</b></font> TClauseList.Count: Integer;
<font color="blue"><b>begin</b></font>
  result := fClauses.Count;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>procedure</b></font> TClauseList.MarkTree(I, N: Integer);
<font color="blue"><b>var</b></font>
  C: TClause;
<font color="blue"><b>begin</b></font>
  <font color="blue"><b>if</b></font> I > N <font color="blue"><b>then</b></font>
  <font color="blue"><b>begin</b></font>
    C := Clauses[I - 1];
    C.InProof := true;
    MarkTree(C.NX, N);
    MarkTree(C.NY, N);
  <font color="blue"><b>end</b></font>;
<font color="blue"><b>end</b></font>;

<font color="blue"><b>procedure</b></font> TClauseList.Output(N: Integer);
<font color="blue"><b>var</b></font>
  I, NX, NY, HC: Integer;
  C: TClause;
<font color="blue"><b>begin</b></font>
  HC := Count - 1;
  <font color="blue"><b>while</b></font> HC > 0 <font color="blue"><b>do</b></font>
  <font color="blue"><b>begin</b></font>
    C := Clauses[HC];
    <font color="blue"><b>if</b></font> C.E.Length = 0 <font color="blue"><b>then</b></font>
      <font color="blue"><b>Break</b></font>;
    Dec(HC);
  <font color="blue"><b>end</b></font>;

  <font color="blue"><b>if</b></font> HC = 0 <font color="blue"><b>then</b></font>
  <font color="blue"><b>begin</b></font>
    writeln(<font color="Red">'Not proved'</font>);
    <font color="blue"><b>Exit</b></font>;
  <font color="blue"><b>end</b></font>;

  NX := Clauses[HC].NX;
  NY := Clauses[HC].NY;
  MarkTree(NX, N);
  MarkTree(NY, N);
  writeln(<font color="Red">'Proof: '</font>);
  <font color="blue"><b>for</b></font> I := N + 1 <font color="blue"><b>to</b></font> HC <font color="blue"><b>do</b></font>
  <font color="blue"><b>begin</b></font>
    C := Clauses[I];
    <font color="blue"><b>if</b></font> C.InProof <font color="blue"><b>then</b></font>
12

demo_pascal_theorem.htm - 源码说明

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

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

⌨️ 快捷键说明

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