Report
SCL with Theory Constraints
| العنوان: | SCL with Theory Constraints |
|---|---|
| المؤلفون: | Bromberger, Martin, Fiori, Alberto, Weidenbach, Christoph |
| سنة النشر: | 2020 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Logic in Computer Science, F.0, F.3, I.1, I.2 |
| الوصف: | 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. Comment: 22 pages |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2003.04627 |
| رقم الانضمام: | edsarx.2003.04627 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |