References & Citations
Computer Science > Logic in Computer Science
Title: SCL with Theory Constraints
(Submitted on 10 Mar 2020 (v1), last revised 22 Oct 2020 (this version, v5))
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.
Submission history
From: Christoph Weidenbach [view email][v1] Tue, 10 Mar 2020 10:43:56 GMT (40kb)
[v2] Wed, 16 Sep 2020 07:27:32 GMT (29kb)
[v3] Tue, 29 Sep 2020 18:32:32 GMT (30kb)
[v4] Fri, 9 Oct 2020 14:20:42 GMT (48kb)
[v5] Thu, 22 Oct 2020 10:23:53 GMT (48kb)
Link back to: arXiv, form interface, contact.