Exploring Partial Models with SCL - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2023

Exploring Partial Models with SCL

Abstract

The family of SCL (Clause Learning from Simple Models) calculi learns clauses with respect to a partial model assumption, similar to CDCL (Conflict Driven Clause Learning). The partial model always consists of ground first-order literals and is built by decisions and propagations. In contrast to propositional logic where propagation chains are always finite, in first-order logic they can become infinite. Therefore, the SCL family does not require exhaustive propagation and the size of the partial model is always finitely bounded. Any partial model not leading to a conflict constitutes a model for the respective finitely bounded ground clause set. We show that all potential partial models can be explored as part of the SCL calculus for first-order logic without equality and that any overall model is an extension of a partial model considered. Furthermore, SCL turns into a semi-decision procedure for first-order logic by extending the finite bound for any partial model not leading to a conflict.
Fichier principal
Vignette du fichier
Exploring_Partial_Models_with_SCL.pdf (445.53 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-04313819 , version 1 (29-11-2023)

Licence

Attribution

Identifiers

Cite

Martin Bromberger, Simon Schwarz, Christoph Weidenbach. Exploring Partial Models with SCL. Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Jun 2023, Manizales, Colombia. pp.48-22, ⟨10.29007/8BR1⟩. ⟨hal-04313819⟩
28 View
12 Download

Altmetric

Share

Gmail Facebook X LinkedIn More