# Item

ITEM ACTIONSEXPORT

Released

Paper

#### SCL with Theory Constraints

##### MPS-Authors

##### External Resource

No external resources are shared

##### Fulltext (restricted access)

There are currently no full texts shared for your IP range.

##### Fulltext (public)

arXiv:2003.04627.pdf

(Preprint), 268KB

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Bromberger, M., Fiori, A., & Weidenbach, C. (2020). SCL with Theory Constraints. Retrieved from https://arxiv.org/abs/2003.04627.

Cite as: https://hdl.handle.net/21.11116/0000-0007-7AFE-3

##### Abstract

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.

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.