抽象规范推理
Abstract Canonical Inference
摘要：
一个规范推理的抽象框架被用来探讨不同的证明顺序如何导致饱和度和完备性的不同变体。像完成，paramodulation，饱和，冗余消除和重写系统减少的概念连接到证明顺序。演绎机制的公平性是根据证明顺序来定义的，区别于产生完整性的（普通）“公平性”和产生饱和度的“均匀公平性”。
英文摘要：
An abstract framework of canonical inference is used to explore how different proof orderings induce different variants of saturation and completeness. Notions like completion, paramodulation, saturation, redundancy elimination, and rewrite-system reduction are connected to proof orderings. Fairness of deductive mechanisms is defined in terms of proof orderings, distinguishing between (ordinary) "fairness," which yields completeness, and "uniform fairness," which yields saturation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
