SGGS: Semantically-Guided Goal-Sensitive Reasoning
SGGS is a model-based conflict-driven theorem-proving method that generalizes
to first-order logic the Conflict-Driven Clause Learning (CDCL)
procedure for propositional satisfiability.
SGGS is semantically guided by a given initial interpretation
and uses a trail of constrained clauses with selected literals
to represent the current candidate model, which is a modification of the initial interpretation.
Until neither a refutation nor a model have been found,
SGGS makes progress by either fixing the current candidate model
or extending it with an instance of an input clause.
Fixing the current candidate model may involve explaining and solving a conflict
or removing intersections between selected literals.
SGGS is refutationally complete and model-complete in the limit.
These features make it attractive as a theorem-proving or model-building method,
and as a basis for model-constructing decision procedures for
decidable fragments in first-order logic.
Its behavior in Horn logic was also investigated:
- Maria Paola Bonacina and Sarah Winkler.
Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover.
Journal of Automated Reasoning, 67(1):6, 42 pages, March 2023;
DOI: 10.1007/s10817-022-09656-w; Springer Nature SharedIt;
supporting material for the experiments in this paper
(presented in part at the Dagstuhl Seminars 21361 on Extending the Synergies between SAT and Description Logics and
21371 on Integrated Deduction, September 2021:
Slides).
- Maria Paola Bonacina and Sarah Winkler.
On SGGS and Horn clauses.
In Proceedings of the 8th Workshop on
Practical Aspects of Automated Reasoning (PAAR) satellite of the 11th International Joint Conference on Automated Reasoning (IJCAR) held at the 8th Federated Logic Conference (FLoC), Haifa, Israel, August 2022.
CEUR Proceedings 3201:1-20, 2022;
supporting material for the experiments in this paper.
[Slides]
- Maria Paola Bonacina and Sarah Winkler.
SGGS decision procedures.
In Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR), Paris, France, EU, July 2020.
Springer, Lecture Notes in Artificial Intelligence 12166, 356-374, 2020;
DOI: 10.1007/978-3-030-51074-9_20;
supporting material for the experiments in this paper
(presented in part at the
Theoretical Foundations of SAT and SMT
Solving Workshop, Satisfiability: Theory, Practice,
and Beyond Program, Simons Institute for the Theory of Computing,
Berkeley, California, USA, March 2021).
- Maria Paola Bonacina and David A. Plaisted.
Semantically-guided goal-sensitive reasoning: inference system and completeness.
Journal of Automated Reasoning, 59(2):165-218, August 2017; DOI: 10.1007/s10817-016-9384-2;
Springer Nature SharedIt
(presented in part at the
1st European Workshop on Higher Order Reasoning (Matryoshka), Vrije Universiteit Amsterdam, Amsterdam, The Netherlands, EU, June 2018:
Slides;
and at the Theoretical Foundations of SAT Solving Workshop,
Fields Institute for Research in the Mathematical Sciences, University of Toronto, Toronto, Ontario, Canada, August 2016:
Slides).
- Maria Paola Bonacina and David A. Plaisted.
Semantically-guided goal-sensitive reasoning: model representation.
Journal of Automated Reasoning, 56(2):113-141, February 2016; DOI: 10.1007/s10817-015-9334-4.
- Maria Paola Bonacina, Ulrich Furbach, and Viorica Sofronie-Stokkermans.
On first-order model-based reasoning.
In Logic, Rewriting, and Concurrency: Essays Dedicated to José Meseguer (LRC 2015).
Springer, Lecture Notes in Computer Science 9200, 181-204, 2015 (invited);
DOI: 10.1007/978-3-319-23165-5_8
(archived in CoRR as arXiv:1502.02535).
- Maria Paola Bonacina and David A. Plaisted.
SGGS theorem proving: an exposition.
In Proceedings of the 4th Workshop on Practical Aspects in Automated Reasoning (PAAR) satellite of the 7th International Joint Conference on Automated Reasoning (IJCAR) held at the 6th Federated Logic Conference (FLoC), Vienna, Austria, EU, July 2014.
EasyChair EPiC Series in Computing 31, 25-38, July 2015;
DOI: 10.29007/m2vf.
- Maria Paola Bonacina and David A. Plaisted.
Constraint manipulation in SGGS.
In Proceedings of the 28th Workshop on Unification (UNIF) satellite of the 7th International Joint Conference on Automated Reasoning (IJCAR) held at the 6th Federated Logic Conference (FLoC), Vienna, Austria, EU, July 2014.
Technical Report 14-06, Research Institute for Symbolic Computation,
Johannes Kepler Universität, Linz, 47-54, 2014.
- Maria Paola Bonacina and David A. Plaisted.
Semantically-guided goal-sensitive theorem proving (Abstract).
Annual Meeting of the IFIP Working Group on Term Rewriting (WG 1.6) satellite of the joint 25th International Conference on Rewriting Techniques and Applications (RTA) and 12th International Conference on Typed Lambda Calculi and Applications (TLCA) held at the 6th Federated Logic Conference (FLoC), Vienna, Austria, EU, July 2014 (abstract of a technical report with the same title
superseded by the above journal articles).
Maria Paola Bonacina