Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

SCL with Theory Constraints

Martin Bromberger 1, 2 Alberto Fiori 1, 2 Christoph Weidenbach 1, 2
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [28 references]  Display  Hide  Download

https://hal.inria.fr/hal-02975868
Contributor : Christoph Weidenbach <>
Submitted on : Friday, October 23, 2020 - 9:14:47 AM
Last modification on : Saturday, October 24, 2020 - 3:37:59 AM

File

2003.04627.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02975868, version 1
  • ARXIV : 2003.04627

Collections

Citation

Martin Bromberger, Alberto Fiori, Christoph Weidenbach. SCL with Theory Constraints. 2020. ⟨hal-02975868⟩

Share

Metrics

Record views

27

Files downloads

61