プロローグを使用した回路検証

Question

私は、2ビット全加算回路の検証に使用する関数と述語を与えられています。これは私がこれまで理解しているものである： - Tは端子であり、信号

関数信号（T）が値1又は

signal(T, V) :- V is 1; V is 0. 

機能タイプ0をとる（Xタイプは、回路素子とタイプである）（X）値のXORを取ることができ、及び、又は

type(X, T) :- T is and; T is or; T is xor. 

ゲートxおよび（n、x）nの出力を表す関数out（x）は入力端子である。ゲート述語のため

out(X, O) :- type(X, and), O is I1+I2, in(1, X, I1), in(1, X, I2). 
%%and so on for other gates 

はこれらについて

forall X[{type(X) == OR} ----> {(out(X) =1)}-----> for some y(in(y, X) = 1)] 

として与えられている私は、プロローグコードに変換するかどうかはわからないと（Iの何かを返す方法をプロローグの機能を理解していません結果がパラメータとして提供されなければならないと考える）。

ヘルプは非常に便利です！

Answer 1

まず、問題の表現方法を選択する必要があります。このporpouseの事実は十分です。回路は、入力信号（0または1）として

で表すことができます。これは、無限ループ（後述）を避けるために必要です。 回路 AおよびB ない/ 1を超える>論理演算 - -

XOR/2、/ 2、/ 2>等

このように、回路は、この形状をとるであろう：

今

xor(and(in(In1),in(In2)),or(in(In1),not(in(In3)))) 

は、のは、回路の状態を計算し、述語出力/ 1を、定義してみましょう：

output(xor(In1,In2),1) :- 
    output(In1,Out1), 
    output(In2,Out2), 
    Out1 \== Out2. 
output(xor(In1,In2),0) :- 
    output(In1,Out1), 
    output(In2,Out2), 
    Out1 == Out2. 

output(and(In1,In2),1) :- 
    output(In1,1), 
    output(In2,1). 
output(and(In1,In2),0) :- 
    output(In1,Out1), 
    output(In2,Out2), 
    (Out1==0 ; Out2==0). 

output(or(In1,In2),1) :- 
    (output(In1,1); output(In2,1)). 
output(or(In1,In2,0),0) :- 
    output(In1,0), 
    output(In2,0). 

output(not(In),0) :- 
    output(In,1). 
output(not(In),1) :- 
    output(In,0). 
output(in(0),0). 
output(in(1),1). 

このpredeciateはPORで可逆的です

?- output(xor(and(in(In1),in(In2)),or(in(In1),not(in(In3)))),Result). 
In1 = In2, In2 = In3, In3 = 0, 
Result = 1 ; 
In1 = In2, In2 = In3, In3 = 0, 
Result = 1 ; 
In1 = In3, In3 = 0, 
In2 = Result, Result = 1 ; 
In1 = Result, Result = 1, 
In2 = 0 ; 
In1 = Result, Result = 1, 
In2 = In3, In3 = 0 ; 
In1 = In2, In2 = 1, 
Result = 0 ; 
In1 = In2, In2 = 1, 
In3 = Result, Result = 0 ; 
false. 

output(A,B)はoutput(in(A),B)と混同すべきではない：pouse、入力がすべての出力を得るために自由変数として残すことができるようにします。 秒がちょうど0または1

instatiatedすることができる一方、最初は再帰的な回路で動作するようです任意の回路（無限ループ）をインスタンス化することができる。

?- output(or(in(Input),in(InOut)),InOut). 
Input = InOut, InOut = 1 ; 
InOut = 1.