二元锁归结式

二元锁归结式（binary lock resolvent），计算机科学技术名词，若将子句中的每个文字都附上一个自然数（子句配锁），对于两个已配锁的子句，如果其归结文字分别是两个子句中带有最小锁的文字，称两个子句的归结式为二元锁归结式。