demo_basic_theorem.htm

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

                <font color="blue"><b>If</b></font> R.length = 1 <font color="blue"><b>Then</b></font>
                  <font color="blue"><b>If</b></font> R.Sign(0) = <font color="Red">"+"</font> <font color="blue"><b>Then</b></font>
                    S = S1
                    P = POS
                  <font color="blue"><b>Else</b></font>
                    S = S2
                    P = NEG
                  <font color="blue"><b>End</b></font> <font color="blue"><b>If</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>If</b></font>
                <font color="blue"><b>Else</b></font>
                  Stack.Push(R)
                <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>If</b></font>
            <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>If</b></font>
      <font color="blue"><b>Next</b></font>
    <font color="blue"><b>Loop</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>
      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>
        S1.AddClauses(POS)
        S2.AddClauses(NEG)
      <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>If</b></font>
  <font color="blue"><b>Finally</b></font>
    POS.Dispose()
    NEG.Dispose()
    Stack.Free()
    
    <font color="blue"><b>Return</b></font> result
  <font color="blue"><b>End</b></font> <font color="blue"><b>Try</b></font>
<font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>

<font color="blue"><b>Function</b></font> TRU(A <font color="blue"><b>As</b></font> TClauseList, SupportSet <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>, TryNumber <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>Boolean</b></font>
  <font color="blue"><b>Dim</b></font> S, S1, S2, S3 <font color="blue"><b>As</b></font> TClauseList
  <font color="blue"><b>Dim</b></font> I, J, K, L, N <font color="blue"><b>AS</b></font> <font color="blue"><b>Integer</b></font>
  <font color="blue"><b>Dim</b></font> W <font color="blue"><b>As</b></font> TList
  <font color="blue"><b>Dim</b></font> C <font color="blue"><b>As</b></font> TClause
  
  S1 = <font color="blue"><b>New</b></font> TClauseList()
  S2 = <font color="blue"><b>New</b></font> TClauseList()
  S3 = <font color="blue"><b>New</b></font> TClauseList()
  
  W = <font color="blue"><b>New</b></font> TList()

  <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
      C = A(I)
      <font color="blue"><b>If</b></font> C.length = 1 <font color="blue"><b>Then</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>If</b></font>
      <font color="blue"><b>Else</b></font>
        S3.Add(C)
        <font color="blue"><b>If</b></font> SupportSet(I) <> <font color="blue"><b>NULL</b></font> <font color="blue"><b>Then</b></font>
          S = <font color="blue"><b>New</b></font> TClauseList()
          <font color="blue"><b>For</b></font> J=0 <font color="blue"><b>To</b></font> SupportSet(I).length - 1
            C = SupportSet(I)(J)
            S.Add(C)
          <font color="blue"><b>Next</b></font>
          W.Add(S)
        <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>If</b></font>
    <font color="blue"><b>Next</b></font>

    <font color="blue"><b>If</b></font> Contradict(A, S1, S2) <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>

    K = 0

    <font color="blue"><b>For</b></font> I=0 <font color="blue"><b>to</b></font> TryNumber - 1
      N = A.Count()
      <font color="blue"><b>If</b></font> GUnit(A, S1, S2, W[K], S3[K]) <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>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>If</b></font> J = K <font color="blue"><b>Then</b></font>
            W(J).Clear
          <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>

          <font color="blue"><b>For</b></font> L=N <font color="blue"><b>To</b></font> A.Count - 1
            <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> <font color="blue"><b>If</b></font>
          <font color="blue"><b>Next</b></font>
        <font color="blue"><b>Next</b></font>
      <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>

      K = K + 1
      <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>If</b></font>
    <font color="blue"><b>Next</b></font>
  <font color="blue"><b>Finally</b></font>
    S1.Dispose()
    S2.Dispose()
    S3.Dispose()
  <font color="blue"><b>End</b></font> <font color="blue"><b>Try</b></font>
  <font color="blue"><b>Return</b></font> false
<font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>

<font color="blue"><b>Dim</b></font> A = <font color="Red">"A"</font>
<font color="blue"><b>Dim</b></font> D = <font color="Red">"D"</font>
<font color="blue"><b>Dim</b></font> F = <font color="Red">"F"</font>
<font color="blue"><b>Dim</b></font> H = <font color="Red">"H"</font>
<font color="blue"><b>Dim</b></font> L = <font color="Red">"L"</font>
<font color="blue"><b>Dim</b></font> P = <font color="Red">"P"</font>
<font color="blue"><b>Dim</b></font> X = <font color="Red">"X"</font>
<font color="blue"><b>Dim</b></font> Y = <font color="Red">"Y"</font>

<font color="blue"><b>Dim</b></font> I, N <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
<font color="blue"><b>Dim</b></font> Clauses <font color="blue"><b>As</b></font> TClauseList
<font color="blue"><b>Dim</b></font> SupportSet <font color="blue"><b>As</b></font> TList

<font color="blue"><b>Sub</b></font> AddClause(E <font color="blue"><b>As</b></font> <font color="blue"><b>Variant</b></font>)
  Clauses.Add(<font color="blue"><b>New</b></font> TClause(E))
<font color="blue"><b>End</b></font> <font color="blue"><b>Sub</b></font>

Num = 0
Clauses = <font color="blue"><b>New</b></font> TClauseList()
SupportSet = <font color="blue"><b>New</b></font> TList()

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>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>NULL</b></font>)
  <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>println</b></font> <font color="Red">"Source clauses:"</font>
Clauses.Dump()

<font color="blue"><b>println</b></font> <font color="Red">"-------------------------------"</font>
<font color="blue"><b>println</b></font> <font color="Red">"Theorem proving"</font>
<font color="blue"><b>println</b></font> <font color="Red">"Unit binary resolution"</font>
<font color="blue"><b>println</b></font> <font color="Red">"-------------------------------"</font>

<font color="blue"><b>println</b></font> <font color="Red">"Theorem :"</font>
<font color="blue"><b>println</b></font> <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
  Clauses(I).Free
<font color="blue"><b>Next</b></font>
Clauses.Dispose
SupportSet.Free
</pre>
</blockquote>

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