Articles in journals

• Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar. CDSAT for predicate-sharing theories: arrays, maps, and vectors with abstract domain.
  In preparation for submission to a journal, 46 pages.

• Maria Paola Bonacina, Stéphane Graham-Lengrand, and Christophe Vauthier. The QSMA algorithm for quantifiers in SMT.
  Submitted to a journal, 44 pages.

• 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. [BibTeX]

• Maria Paola Bonacina. Set of support, demodulation, paramodulation: a historical perspective.
  Journal of Automated Reasoning, 66(4):463-497, November 2022; DOI: 10.1007/s10817-022-09628-0; Springer Nature SharedIt. [BibTeX]

• Michael Beeson, Maria Paola Bonacina, Michael Kinyon, and Geoff Sutcliffe. Larry Wos - Visions of automated reasoning.
  Journal of Automated Reasoning, 66(4):439-461, November 2022; DOI: 10.1007/s10817-022-09620-8. [BibTeX]

• Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar. Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs.
  Journal of Automated Reasoning 66(1):43-91, February 2022; DOI: 10.1007/s10817-021-09606-y; Springer Nature SharedIt. [BibTeX]

• Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar. Conflict-driven satisfiability for theory combination: transition system and completeness.
  Journal of Automated Reasoning, 64(3):579-609, March 2020; DOI: 10.1007/s10817-018-09510-y; Springer Nature SharedIt. [BibTeX] [Slides]

• 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. [BibTeX] [Slides1] [Slides2] [Slides3]

• 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. [BibTeX] [Slides1] [Slides2]

• Maria Paola Bonacina and Moa Johansson. Interpolation systems for ground proofs in automated deduction: a survey.
  Journal of Automated Reasoning, 54(4):353-390, April 2015; DOI: 10.1007/s10817-015-9325-5. [BibTeX] [Slides]

• Maria Paola Bonacina and Moa Johansson. On interpolation in automated theorem proving.
  Journal of Automated Reasoning, 54(1):69-97, January 2015; DOI: 10.1007/s10817-014-9314-0. [BibTeX] [Slides]

• Maria Paola Bonacina, Christopher A. Lynch and Leonardo de Moura. On deciding satisfiability by theorem proving with speculative inferences.
  Journal of Automated Reasoning, 47(2):161-189, August 2011; DOI: 10.1007/s10817-010-9213-y. [BibTeX] [Slides1] [Slides2] [Slides3]

• Maria Paola Bonacina and Mnacho Echenim. Theory decision by decomposition.
  Journal of Symbolic Computation, 45(2):229-260, February 2010; DOI: 10.1016/j.jsc.2008.10.008. [BibTeX] [Slides]

• Alessandro Armando, Maria Paola Bonacina, Silvio Ranise and Stephan Schulz. New results on rewrite-based satisfiability procedures.
  ACM Transactions on Computational Logic, 10(1):129-179, January 2009; DOI: 10.1145/1459010.1459014. [BibTeX] [Slides1] [Slides2]

• Maria Paola Bonacina and Mnacho Echenim. On variable-inactivity and polynomial T-satisfiability procedures.
  Journal of Logic and Computation, 18(1):77-96, February 2008; DOI: 10.1093/logcom/exm055. [BibTeX] [Slides]

• Maria Paola Bonacina and Nachum Dershowitz. Abstract canonical inference.
  ACM Transactions on Computational Logic, 8(1):180-208, January 2007; DOI: 10.1145/1182613.1182619. [BibTeX] [Slides]

• Maria Paola Bonacina. Towards a unified model of search in theorem proving: subgoal-reduction strategies.
  Journal of Symbolic Computation, 39(2):209-255, February 2005; DOI: 10.1016/j.jsc.2004.11.001. [BibTeX]

• Maria Paola Bonacina. A taxonomy of parallel strategies for deduction.
  Annals of Mathematics and Artificial Intelligence, 29(1,2,3&4):223-257, 2000; DOI: 10.1023/A:1018932114059. [BibTeX] [Slides of a colloquium at the Libera Università degli Studi di Bolzano, Italy, March 2001]

• Maria Paola Bonacina. A model and a first analysis of distributed-search contraction-based strategies.
  Annals of Mathematics and Artificial Intelligence, 27(1,2,3&4):149-199, December 1999; DOI: 10.1023/A:1018919214722. [BibTeX] [Slides of colloquia at the Università degli Studi di Roma "La Sapienza", L'Aquila, Trento, Verona, Pisa, May-June 2000]

• Maria Paola Bonacina and Jieh Hsiang. On the modelling of search in theorem proving - Towards a theory of strategy analysis.
  Information and Computation, 147:171-208, December 1998; DOI: 10.1006/inco.1998.2739. [BibTeX] [Slides of a colloquium at TU Graz, Austria, May 2000]

• Maria Paola Bonacina and Jieh Hsiang. On semantic resolution with lemmaizing and contraction and a formal treatment of caching.
  New Generation Computing, 16(2):163-200, February 1998; DOI: 10.1007/BF03037315. [BibTeX]

• Maria Paola Bonacina. On the reconstruction of proofs in distributed theorem proving: a modified Clause-Diffusion method.
  Journal of Symbolic Computation, 21(4,5&6):507-522, April-June 1996; DOI: 10.1006/jsco.1996.0028. [BibTeX] [Slides of a colloquium at TU Dresden, Germany, May 1999]

• Hantao Zhang, Maria Paola Bonacina and Jieh Hsiang. PSATO: a distributed propositional prover and its application to quasigroup problems.
  Journal of Symbolic Computation, 21(4,5&6):543-560, April-June 1996; DOI: 10.1006/jsco.1996.0030. [BibTeX]

• Maria Paola Bonacina and Jieh Hsiang. A category-theoretic treatment of automated theorem proving.
  Journal of Information Science and Engineering, 12(1):101-125, March 1996. [BibTeX]

• Maria Paola Bonacina and Jieh Hsiang. The Clause-Diffusion methodology for distributed deduction.
  Fundamenta Informaticae, 24(1&2):177-207, September 1995; DOI: 10.3233/FI-1995-24128. [BibTeX] [Slides of a talk at LORIA, Nancy, France, EU, April 1993]

• Maria Paola Bonacina and Jieh Hsiang. Towards a foundation of completion procedures as semidecision procedures.
  Theoretical Computer Science, 146:199-242, July 1995; DOI: 10.1016/0304-3975(94)00187-N. [BibTeX]

• Maria Paola Bonacina and Jieh Hsiang. Distributed deduction by Clause-Diffusion: distributed contraction and the Aquarius prover.
  Journal of Symbolic Computation, 19(1,2&3):245-267, January-March 1995; DOI: 10.1006/jsco.1995.1014. [BibTeX] [Slides of colloquia at the University of Colorado at Denver, CO, and at the University of Iowa, Iowa City, IA, USA, April-May 1993]

• Maria Paola Bonacina and Jieh Hsiang. On subsumption in distributed derivations.
  Journal of Automated Reasoning, 12(2):225-240, June 1994; DOI: 10.1007/BF00881888. [BibTeX]

• Maria Paola Bonacina and Jieh Hsiang. Parallelization of deduction strategies: an analytical study.
  Journal of Automated Reasoning, 13(1):1-33, February 1994; DOI: 10.1007/BF00881910. [BibTeX] [Slides of a tutorial at CADE-12, Nancy, France, EU, June 1994]

• Maria Paola Bonacina and Jieh Hsiang. On rewrite programs: semantics and relationship with Prolog.
  The Journal of Logic Programming, 14(1&2):155-180, October 1992; DOI: 10.1016/0743-1066(92)90050-D. [BibTeX] [Slides of Colloquia at the CUNY Graduate Center, New York, NY, and at the University of Idaho, Moscow, ID, USA, May 1993]

Maria Paola Bonacina