人工智能中很重要的一个环节就是知识表示，知识表示的一般方法包括状态空间表示法，谓词逻辑表示法，问题规约表示，和语义网络表示法，在知识表示后的知识检索非常重要。
关于检索有很多方式我介绍一种将常见的谓词演算转化为元组计算的形式化表示的方法。
谓词逻辑法采用谓词合适公式和一阶谓词演算把要解决的问题变为一个有待证明的问题，然后采用消解定理和消解反演来证明一个新语句是从已知的正确语句导出的，从而证明这个新语句也是正确的。谓词逻辑是一种形式语言，能够把数学中的逻辑论证符号化。谓词逻辑法常与其它表示方法混合使用，灵活方便，可以表示比较复杂的问题。
表示如下：
并R ∪ S = {t| R(t) U S(t)}
减法R – S = {t| R(t) ∧ ┑S(t)}
乘法R X S = {t | ∃R(t) ∃S(t) t(1) = R1∧t(2) = R2∧... ∧t(n+r) = S(r)}
投影∏23（R） = {t| ∃R(t) t(1) = R(2) ∧t(2) = R(3)}
连接R ∞ S = {t | ∃R(t) ∃S(t) t(1) = R1∧t(2) = R2∧... ∧t(n+r) = S(r)} 同时对R（i） = S(j)的项进行合并。
函数σF = {t| R(t) ∧F’}
自然连接
以上t(i) R(i)均表示列。
以上是形式化表示，具体的表示查询则为：
T知识使用结构（A，B，C）表示，S知识使用结构（C，D）表示则建立两个知识之间的查询，并查处符合条件的A值可以使用以下方式形式化的查询：
∏A σA=? (T ∞ S)