Pyke 通過回溯的方式，嘗試每個(gè)可能的匹配。因此，同一規(guī)則可能多次適用成功，每次成功匹配的是不同的事實(shí)。在規(guī)則的 if 子句的“前提列表”中，是進(jìn)還是退、是上還是下，取決于前提的證明是成功還是失敗。在列表中往后退，嘗試別的證明辦法，這個(gè)過程叫做回溯。
推理
規(guī)則保存在規(guī)則庫中，各有不同的具體內(nèi)容。規(guī)則之間沒有嵌套和顯性關(guān)聯(lián)。Pyke 必須自己設(shè)法來解決規(guī)則之間的整合，以完成某些大型任務(wù)。 Pyke 用的辦法叫做“推理”，它有兩種不同的方式：
1）應(yīng)用正向推理規(guī)則，要求規(guī)則庫已經(jīng)激活。 正向推理規(guī)則可以斷言新的事實(shí)，可以激活更多的規(guī)則庫。?
2）當(dāng)你的程序要求 Pyke 證明某個(gè)具體目標(biāo)時(shí)，使用反向推理規(guī)則（例如，向 Pyke 詢問）。 應(yīng)用這些規(guī)則，是為了回答某個(gè)問題，而非斷言新事實(shí)，或者激活更多的規(guī)則庫。 反向推理規(guī)則，還能匯集 Python 函數(shù)，形成具體的“調(diào)用順序圖”或叫做“方案圖”的程序，以處理實(shí)際問題。
正向推理（用?foreach?和?asssert?代替?if?和?then）
規(guī)則庫激活后，正向規(guī)則執(zhí)行的順序，以其在.krb規(guī)則庫文件中的次序?yàn)闇?zhǔn)。
為了進(jìn)行正向推理，Pyke 查看哪個(gè)規(guī)則的 if 子句，與已知事實(shí)相匹配（ if 子句可以多次匹配成功，參見“回溯”）。 規(guī)則匹配成功后，開始啟用它，將其 than 子句中的事實(shí)，加入已知事實(shí)的列表。 新的事實(shí)與其他正向規(guī)則 if 子句匹配后，可以將其啟用。各種深度的推理過程，都可發(fā)生這種匹配。正向推理的過程，持續(xù)到?jīng)]有規(guī)則可供使用。
規(guī)則的 if 子句中有事實(shí)陳述的模式，它們可能與幾個(gè)事實(shí)匹配，于是，規(guī)則可能多次匹配啟用。 規(guī)則 then 子句的事實(shí)陳述也有模式。每當(dāng)規(guī)則啟用，then 子句中的模式變量，可以約束成不同值，從而斷言出不同事實(shí)。
注意，foreach?子句末尾的事實(shí)，可以多次匹配成功，由此多次啟用?assert?子句。?
可是，?foreach?子句起始的事實(shí)，僅能匹配失敗一次。若匹配失敗，整個(gè)規(guī)則適用失敗。
反向推理 （用?use?和?when?代替?then?和 if）
Pyke 的證明活動，開始于尋找某一規(guī)則，其 then 子句與目標(biāo)匹配。?
Pyke 接著證明規(guī)則 if 子句為真。?
亦即：規(guī)則的 if 子句，與另一規(guī)則的 then 子句，可以建立連接。
Pyke 最終會形成一條“證據(jù)鏈”，從第一條規(guī)則的 if 子句開始，到下一規(guī)則的 then 子句結(jié)束。
Pyke 只允許在 use 子句里出現(xiàn)一個(gè)事實(shí)陳述，這與正向推理的 assert 子句（允許多個(gè)事實(shí)）不同。
在向 Pyke 求證某個(gè)目標(biāo)的要求之后，這些規(guī)則才被調(diào)用。?
提出求證要求的最簡方式，是用函數(shù)?some_engine.prove_1_goal?或者?some_engine.prove_goal。函數(shù)?prove_1_goal?返回找到的第一個(gè)證據(jù)后，便停止運(yùn)行（或者引起意外：pyke.knowledge_engine.CanNotProve）。函數(shù)?prove_goal?返回的是求證過程中產(chǎn)生的全部證據(jù)的“管理器”。
