目标表达式
在逆向演绎系统中，目标表达式可以为无蕴含的任意与或形式。可用类似于正向系统中转化事实表达式的过程，将任意形式的目标表达式转化成标准的与或形式。不同的是，应Skolem化全称量词量化的变量，略去存在量词，则目标表达式中尚存的变量都认为是存在量词量化的变量。在重新命名变量时，应使同一变量名不出现在不同的主要析取式中。
例如有目标表达式
($y)("x){P(x)®[Q(x,y)ÙØ[R(x)ÙS(y)]]}
可转化为
ØP(f(y))Ú{[Q(f(y),y)Ù[ØR(x)ÚØS(y)]]}
重新命名变量后得
ØP(f(z))Ú{[Q(f(y),y)Ù[ØR(x)ÚØS(y)]]}
与或形式的目标公式可以用与或图表示，如下图所示。图中k-连接符用来连接表示合取关系的子表达式，1-连接符用来连接表示析取关系的子表达式。根结点表示目标表达式，称为目标结点，其后代称为子目标结点。叶结点表示单个文字。从图中结束在叶结点的解图集中可以读出子句为
ØP(f(z)
Q(f(y),y)ÙØR(f(y))
Q(f(y),y)ÙØS(y)
目标子句是文字的合取 ，其中的变量是存在量词量化的。