SCL with Theory Constraints
share
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. The model representation consists of ground background theory literals and ground first-order literals. The model representation language is expressive enough to simulate hierarchic superposition on full first-order theory constrained clauses with variables. Generated clauses enjoy a non-redundancy property. 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. 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.
READ FULL TEXT