References

  1. 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.
  2. Nikolaj Bjørner & Leonardo de Moura (2008): Proofs and refutations, and Z3. In: IWIL-7, CEUR 418, pp. 123–132.
  3. François Bobot, Stéphane Graham-Lengrand, Bruno Marre & Guillaume Bury (2018): Centralizing equality reasoning in MCSAT. In: SMT-16.
  4. 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.
  5. Maria Paola Bonacina (2018): On conflict-driven reasoning. In: AFM-6, Kalpa Publications 5. EasyChair, pp. 31–49, doi:10.29007/spwm.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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/.
  17. 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.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. 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.
  24. 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.
  25. 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.
  26. Natarajan Shankar (2009): Automated deduction for verification. ACM Comput. Surv. 41(4), pp. 507–522, doi:10.1145/1592434.1592437.
  27. 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.
  28. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org