English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Paper

SCL with Theory Constraints

MPS-Authors
/persons/resource/persons117832

Bromberger,  Martin
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons244456

Fiori,  Alberto
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons45719

Weidenbach,  Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

External Ressource
No external resources are shared
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: http://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.