@online{DBLP:journals/corr/abs-2003-04627,
TITLE = {{SCL} with Theory Constraints},
AUTHOR = {Bromberger, Martin and Fiori, Alberto and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2003.04627},
EPRINT = {2003.04627},
EPRINTTYPE = {arXiv},
YEAR = {2020},
ABSTRACT = {We lift the SCL calculus for first-order logic without equality to the SCL(T)<br>calculus for first-order logic without equality modulo a background theory. In<br>a nutshell, the SCL(T) calculus describes a new way to guide hierarchic<br>resolution inferences by a partial model assumption instead of an a priori<br>fixed order as done for instance in hierarchic superposition. The model<br>representation consists of ground background theory literals and ground<br>foreground first-order literals. One major advantage of the model guided<br>approach is that clauses generated by SCL(T) enjoy a non-redundancy property<br>that makes expensive testing for tautologies and forward subsumption completely<br>obsolete. SCL(T) is a semi-decision procedure for pure clause sets that are<br>clause sets without first-order function symbols ranging into the background<br>theory sorts. Moreover, SCL(T) can be turned into a decision procedure if the<br>considered combination of a first-order logic modulo a background theory enjoys<br>an abstract finite model property.<br>},
}