demo_basic_theorem.htm

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

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

<body>

<h3>
LISPPA: Mechanical theorem proving (paxBasic).
</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>Imports</b></font> SysUtils, Classes, Contnrs

<font color="blue"><b>Dim</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>]
<font color="blue"><b>Dim</b></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>]
<font color="blue"><b>Dim</b></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>Dim</b></font> Num <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font> = 0

<font color="blue"><b>Function</b></font> IsCompound(Term <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>) <font color="blue"><b>As</b></font> <font color="blue"><b>Boolean</b></font>
  <font color="blue"><b>return</b></font> isPaxArray(Term)
<font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>

<font color="blue"><b>Function</b></font> IsVar(P <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>) <font color="blue"><b>As</b></font> <font color="blue"><b>Boolean</b></font>
  <font color="blue"><b>Dim</b></font> result
  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>Return</b></font> false
  <font color="blue"><b>Else</b></font>
    <font color="blue"><b>Return</b></font> (Asc(P) >= Asc(<font color="Red">"U"</font>)) <font color="blue"><b>And</b></font> (Asc(P) <= Asc(<font color="Red">"Z"</font>))
  <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
<font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>

<font color="blue"><b>Function</b></font> CopyTerm(A <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>) <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>
  <font color="blue"><b>Dim</b></font> I <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
  <font color="blue"><b>Dim</b></font> AI, result <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</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
    AI = <font color="blue"><b>AddressOf</b></font> 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>If</b></font>
  <font color="blue"><b>Next</b></font>
  <font color="blue"><b>Return</b></font> result
<font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>

<font color="blue"><b>Function</b></font> Inside(Key <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>, Term <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>) <font color="blue"><b>As</b></font> <font color="blue"><b>Boolean</b></font>
  <font color="blue"><b>Dim</b></font> I <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</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>If</b></font> Inside(Key, Term(I)) <font color="blue"><b>Then</b></font>
        <font color="blue"><b>Return</b></font> true
      <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
    <font color="blue"><b>Next</b></font>
    <font color="blue"><b>Return</b></font> false
  <font color="blue"><b>Else</b></font>
    <font color="blue"><b>Return</b></font> (Key = Term)
  <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
<font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>

<font color="blue"><b>Function</b></font> Unify(N <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>, T1 <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>, T2 <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>) <font color="blue"><b>As</b></font> <font color="blue"><b>Boolean</b></font>
  <font color="blue"><b>Dim</b></font> I <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
  <font color="blue"><b>Dim</b></font> P1, P2 <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>
  <font color="blue"><b>For</b></font> I=N <font color="blue"><b>to</b></font> T1.length - 1
    P1 = <font color="blue"><b>AddressOf</b></font> T1(I)
    P2 = <font color="blue"><b>AddressOf</b></font> 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>
      <font color="blue"><b>If</b></font> <font color="blue"><b>Not</b></font> Unify(0, P1, P2) <font color="blue"><b>Then</b></font>
        <font color="blue"><b>Return</b></font> false
      <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
    <font color="blue"><b>ElseIf</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>
      <font color="blue"><b>TerminalOf</b></font> P1 = <font color="blue"><b>AddressOf</b></font> <font color="blue"><b>TerminalOf</b></font> P2
    <font color="blue"><b>ElseIf</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>
      <font color="blue"><b>TerminalOf</b></font> P2 = <font color="blue"><b>AddressOf</b></font> <font color="blue"><b>TerminalOf</b></font> P1
    <font color="blue"><b>ElseIf</b></font> P1 <> P2 <font color="blue"><b>Then</b></font>
      <font color="blue"><b>Return</b></font> false
    <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
  <font color="blue"><b>Next</b></font>
  <font color="blue"><b>Return</b></font> true
<font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>

<font color="blue"><b>Class</b></font> TClause
  <font color="blue"><b>Inherits</b></font> TObject
  
  <font color="blue"><b>Dim</b></font> E, Params <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>
  <font color="blue"><b>Dim</b></font> Number, NParam, NX, NY, ND <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
  <font color="blue"><b>Dim</b></font> InProof <font color="blue"><b>As</b></font> <font color="blue"><b>Boolean</b></font>
  
  <font color="blue"><b>Sub</b></font> <font color="blue"><b>New</b></font>(A <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>)
    <font color="blue"><b>Me</b></font> = <font color="blue"><b>MyBase</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>NULL</b></font> <font color="blue"><b>then</b></font>
      CreateParams(E)
    <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
  <font color="blue"><b>End</b></font> <font color="blue"><b>Sub</b></font>
  
  <font color="blue"><b>Sub</b></font> Dispose()
    <font color="blue"><b>MyBase</b></font>.Free
  <font color="blue"><b>End</b></font> <font color="blue"><b>Sub</b></font>

  <font color="blue"><b>Sub</b></font> CreateParams(P <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>)
    <font color="blue"><b>Dim</b></font> I, J, K <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
    <font color="blue"><b>Dim</b></font> PI <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>
    <font color="blue"><b>For</b></font> I=0 <font color="blue"><b>To</b></font> P.length - 1
      PI = <font color="blue"><b>AddressOf</b></font> P(I)
      <font color="blue"><b>If</b></font> IsCompound(PI) <font color="blue"><b>Then</b></font>
        CreateParams(PI)
      <font color="blue"><b>ElseIf</b></font> IsVar(PI) <font color="blue"><b>Then</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>If</b></font> Params(J) = PI <font color="blue"><b>Then</b></font>
            K = J
          <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
        <font color="blue"><b>Next</b></font>
        <font color="blue"><b>If</b></font> K = -1 <font color="blue"><b>Then</b></font>
          K = NParam
          Params(K) = PI
          NParam += 1
        <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
        P(I) = <font color="blue"><b>AddressOf</b></font> Params(K)
      <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
    <font color="blue"><b>Next</b></font>
  <font color="blue"><b>End</b></font> <font color="blue"><b>Sub</b></font>
  
  <font color="blue"><b>Function</b></font> Length <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
    <font color="blue"><b>Return</b></font> E.length
  <font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>

  <font color="blue"><b>Function</b></font> Sign(I <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>) <font color="blue"><b>As</b></font> <font color="blue"><b>String</b></font>
    <font color="blue"><b>Return</b></font> E(I)(0)
  <font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>

  <font color="blue"><b>Function</b></font> Name(I <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>) <font color="blue"><b>As</b></font> <font color="blue"><b>String</b></font>
    <font color="blue"><b>return</b></font> E(I)(1)
  <font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>
  
  <font color="blue"><b>Sub</b></font> Rename(L <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>)
    <font color="blue"><b>Dim</b></font> I <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
    <font color="blue"><b>For</b></font> I=0 <font color="blue"><b>To</b></font> NParam - 1
      <font color="blue"><b>Delete</b></font> Params(I)
      Params(I) = L(I)
    <font color="blue"><b>Next</b></font>
  <font color="blue"><b>End</b></font> <font color="blue"><b>Sub</b></font>
  
  <font color="blue"><b>Sub</b></font> Dump
    <font color="blue"><b>println</b></font> 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>Sub</b></font>

  <font color="blue"><b>Sub</b></font> PutResolvent(A <font color="blue"><b>As</b></font> TClause, B <font color="blue"><b>As</b></font> TClause, LA <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>, LB <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>)
    <font color="blue"><b>Dim</b></font> I, J <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</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>If</b></font> I <> LA <font color="blue"><b>Then</b></font>
        J += 1
        E(J) = CopyTerm(A.E(I))
      <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
    <font color="blue"><b>Next</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>If</b></font> I <> LB <font color="blue"><b>Then</b></font>
        J += 1
        E(J) = CopyTerm(B.E(I))
      <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
    <font color="blue"><b>Next</b></font>
123

demo_basic_theorem.htm - 源码说明

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

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

⌨️ 快捷键说明

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