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 的證明活動(dòng)迂曲，開始于尋找某一規(guī)則，其 then 子句與目標(biāo)匹配寥袭。?
Pyke 接著證明規(guī)則 if 子句為真路捧。?
亦即：規(guī)則的 if 子句，與另一規(guī)則的 then 子句传黄，可以建立連接杰扫。
Pyke 最終會(huì)形成一條“證據(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ù)的“管理器”笨觅。
