Symbolic Model Construction for Saturated Constrained Horn Clauses
Logic in Computer Science
2023-09-19 v2
Abstract
Clause sets saturated by hierarchic ordered resolution do not offer a model representation that can be effectively queried, in general. They only offer the guarantee of the existence of a model. We present an effective symbolic model construction for saturated constrained Horn clauses. Constraints are in linear arithmetic, the first-order part is restricted to a function-free language. The model is constructed in finite time, and non-ground clauses can be effectively evaluated with respect to the model. Furthermore, we prove that our model construction produces the least model.
Cite
@article{arxiv.2305.05064,
title = {Symbolic Model Construction for Saturated Constrained Horn Clauses},
author = {Martin Bromberger and Lorenz Leutgeb and Christoph Weidenbach},
journal= {arXiv preprint arXiv:2305.05064},
year = {2023}
}