组合逻辑公理

我正在用组合逻辑进行定理验证的一些实验，这看起来很有希望，但是有一个绊脚石：已经指出在组合逻辑中，确实如此。 I = SKK但这不是一个定理，它必须作为公理添加。有谁知道需要添加的公理的完整列表？ 编辑：你当然可以手工证明我= SKK，但除非我遗漏了某些东西，否则它不是具有相等性的组合逻辑系统中的定理。话虽如此，你可以将我扩展到SKK ......但我仍然缺少一些重要的东西。取一组子句p（X）和~p（X），这很容易解决普通一阶逻辑中的矛盾，并将它们转换为SK，执行替换并评估S和K的所有调用，我的程序生成以下（我使用'用于Unlambda的反击）： ''eq''s''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''' 'k true'k true 看起来我需要的是一套适当的规则来处理部分调用'k和'，我只是没看到这些规则应该是什么，我在这个领域找到的所有文献都是为数学家的目标受众而不是程序员。我怀疑一旦你明白答案可能很简单。