Haniel Barbosa, Jasmin C. Blanchette, Mathias Fleury & Pascal Fontaine (2020):
Scalable Fine-Grained Proofs for Formula Processing.
J. of Autom. Reason. 64(3),
pp. 485–550,
doi:10.1007/s10817-018-09502-y.
Nikolaj Bjørner & Leonardo de Moura (2008):
Proofs and refutations, and Z3.
In: IWIL-7,
CEUR 418,
pp. 123–132.
François Bobot, Stéphane Graham-Lengrand, Bruno Marre & Guillaume Bury (2018):
Centralizing equality reasoning in MCSAT.
In: SMT-16.
Maria Paola Bonacina (1996):
On the reconstruction of proofs in distributed theorem proving: a modified Clause-Diffusion method.
J. of Symb. Comput. 21(4–6),
pp. 507–522,
doi:10.1006/jsco.1996.0028.
Maria Paola Bonacina (2018):
On conflict-driven reasoning.
In: AFM-6,
Kalpa Publications 5.
EasyChair,
pp. 31–49,
doi:10.29007/spwm.
Maria Paola Bonacina (2018):
Parallel theorem proving.
In: Handbook of Parallel Constraint Reasoning, chapter 6.
Springer,
pp. 179–235,
doi:10.1007/978-3-319-63516-3_6.
Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen & Cesare Tinelli (2019):
Theory combination: beyond equality sharing.
In: Description Logic, Theory Combination, and All That: Essays Dedicated to Franz Baader,
LNAI 11560.
Springer,
pp. 57–89,
doi:10.1007/978-3-030-22102-7_3.
Maria Paola Bonacina, Stéphane Graham-Lengrand & Natarajan Shankar (2017):
Satisfiability modulo theories and assignments.
In: CADE-26,
LNAI 10395.
Springer,
pp. 42–59,
doi:10.1007/978-3-319-63046-5_4.
Maria Paola Bonacina, Stéphane Graham-Lengrand & Natarajan Shankar (2018):
Proofs in conflict-driven theory combination.
In: CPP-7.
ACM,
pp. 186–200,
doi:10.1145/3167096.
Maria Paola Bonacina, Stéphane Graham-Lengrand & Natarajan Shankar (2020):
Conflict-driven satisfiability for theory combination: transition system and completeness.
J. of Autom. Reason. 64(3),
pp. 579–609,
doi:10.1007/s10817-018-09510-y.
Maria Paola Bonacina, Stéphane Graham-Lengrand & Natarajan Shankar (2021):
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs.
J. of Autom. Reason. Submitted,
pp. 1–54.
http://profs.sci.univr.it/~bonacina/cdsat.html.
Maria Paola Bonacina & Moa Johansson (2015):
Interpolation systems for ground proofs in automated deduction: a survey.
J. of Autom. Reason. 54(4),
pp. 353–390,
doi:10.1007/s10817-015-9325-5.
Franz Brauße, Konstantin Korovin, Margarita Korovina & Norbert Müller (2019):
A CDCL-style calculus for solving non-linear constraints.
In: FroCoS-12,
LNAI 11715.
Springer,
pp. 131–148,
doi:10.1007/978-3-030-29007-8_8.
Luís Cruz-Felipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann & Peter Schneider-Kamp (2017):
Efficient certified RAT verification.
In: CADE-26,
LNAI 10395.
Springer,
pp. 220–236,
doi:10.1007/978-3-319-63046-5_14.
Leonardo de Moura & Dejan Jovanovi\'c (2013):
A model-constructing satisfiability calculus.
In: VMCAI-14,
LNCS 7737.
Springer,
pp. 1–12,
doi:10.1007/978-3-642-35873-9_1.
Leonardo de Moura & Grant Olney Passmore (2013):
Exact global optimization on demand (Presentation only).
In: ADDCT-3.
Available at https://userpages.uni-koblenz.de/~sofronie/addct-2013/.
Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto & Alwen Tiu (2006):
Expressiveness+automation+soundness: towards combining SMT solvers and interactive proof assistants.
In: TACAS-12,
LNCS 3920.
Springer,
pp. 167–181,
doi:10.1007/11691372_11.
Stéphane Graham-Lengrand, Dejan Jovanovi\'c & Bruno Dutertre (2020):
Solving bitvectors with MCSAT: explanations from bits and pieces.
In: IJCAR-10,
LNAI 12166.
Springer,
pp. 103–121,
doi:10.1007/978-3-030-51074-9_7.
Dejan Jovanovi\'c (2017):
Solving nonlinear integer arithmetic with MCSAT.
In: VMCAI-18,
LNCS 10145.
Springer,
pp. 330–346,
doi:10.1007/978-3-319-52234-0_18.
Dejan Jovanovi\'c, Clark Barrett & Leonardo de Moura (2013):
The design and implementation of the model-constructing satisfiability calculus.
In: FMCAD-13.
ACM and IEEE.
Dejan Jovanovi\'c & Leonardo de Moura (2013):
Cutting to the chase: solving linear integer arithmetic.
J. of Autom. Reason. 51,
pp. 79–108,
doi:10.1007/s10817-013-9281-x.
Dejan Jovanovi\'c & Leonardo de Moura (2012):
Solving non-linear arithmetic.
In: IJCAR-6,
LNAI 7364.
Springer,
pp. 339–354,
doi:10.1007/978-3-642-31365-3_27.
Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds & Liana Hadarean (2016):
Lazy proofs for DPLL(T)-based SMT solvers.
In: FMCAD-16.
ACM and IEEE,
pp. 93–100,
doi:10.1109/FMCAD.2016.7886666.
Greg Nelson (1983):
Combining satisfiability procedures by equality sharing.
In: Automatic Theorem Proving: After 25 Years.
AMS,
pp. 201–211,
doi:10.1090/conm/029/11.
Greg Nelson & Derek C. Oppen (1979):
Simplification by Cooperating Decision Procedures.
ACM Trans. on Prog. Lang. and Syst. 1(2),
pp. 245–257,
doi:10.1145/357073.357079.
Natarajan Shankar (2009):
Automated deduction for verification.
ACM Comput. Surv. 41(4),
pp. 507–522,
doi:10.1145/1592434.1592437.
Aleksandar Zelji\'c, Christoph M. Wintersteiger & Philipp Rümmer (2016):
Deciding bit-vector formulas with mcSAT.
In: SAT-19,
LNCS 9710.
Springer,
pp. 249–266,
doi:10.1007/978-3-319-40970-2_16.
Lintao Zhang & Sharad Malik (2003):
Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications.
In: DATE 2003.
IEEE,
pp. 10880–10885,
doi:10.5555/789083.1022835.
eptcs@eptcs.org