论文标题
与理论约束的SCL
SCL with Theory Constraints
论文作者
论文摘要
我们在没有平等的一阶逻辑的情况下，将一阶逻辑的SCL演算提升为一阶逻辑，而无需平等模量的背景理论。简而言之，SCL（t）微积分描述了一种通过部分模型假设指导层次分辨率推断的新方法，而不是在层次上的超级定位中完成的先验固定顺序。模型表示由地面背景理论文字和前景一阶文字组成。模型指导方法的一个主要优点是，SCL（T）生成的条款享有非差额属性，该属性使对重言式进行了昂贵的测试，并且远期包含完全过时。 SCL（t）是纯句集的半决定程序，是子句集，而没有一阶函数符号，范围为背景理论。此外，如果考虑到一阶逻辑模型的考虑组合，背景理论具有抽象的有限模型属性，则可以将SCL（t）变成决策过程。
We lift the SCL calculus for first-order logic without equality to the SCL(T) calculus for first-order logic without equality modulo a background theory. In a nutshell, the SCL(T) calculus describes a new way to guide hierarchic resolution inferences by a partial model assumption instead of an a priori fixed order as done for instance in hierarchic superposition. The model representation consists of ground background theory literals and ground foreground first-order literals. One major advantage of the model guided approach is that clauses generated by SCL(T) enjoy a non-redundancy property that makes expensive testing for tautologies and forward subsumption completely obsolete. SCL(T) is a semi-decision procedure for pure clause sets that are clause sets without first-order function symbols ranging into the background theory sorts. Moreover, SCL(T) can be turned into a decision procedure if the considered combination of a first-order logic modulo a background theory enjoys an abstract finite model property.
