Maria Paola Bonacina

Maria Paola Bonacina

The main ideas in the CDSAT (Conflict-Driven Satisfiability) framework for SMT are summarized, leading to approaches to proof generation in CDSAT.

Maria Paola Bonacina, Ulrich Furbach, Viorica Sofronie-Stokkermans

Reasoning semantically in first-order logic is notoriously a challenge. This paper surveys a selection of semantically-guided or model-based methods that aim at meeting aspects of this challenge. For first-order logic we touch upon resolution-based methods, tableaux-based methods, DPLL-inspired methods, and we give a preview of a new method called SGGS, for Semantically-Guided Goal-Sensitive reasoning. For first-order theories we highlight hierarchical and locality-based methods, concluding with the recent Model-Constructing satisfiability calculus.