Publications

• In progress
  • 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.

• 2024
  • Maria Paola Bonacina, Pascal Fontaine, Cláudia Nalon, Claudia Schon (Editors), and Martin Desharnais (Editorial Assistant). The Next Generation of Deduction Systems: From Composition to Compositionality - Report from Dagstuhl Seminar 23471.
    Dagstuhl Publishing, Dagstuhl Reports 13(11):130-150, April 2024; DOI: 10.4230/DagRep.13.11.130. [BibTeX]

• 2023
  • Maria Paola Bonacina. Reasoning about quantifiers in SMT: the QSMA algorithm.
    In Proceedings of the 23rd International Conference on Formal Methods in Computer-Aided Design (FMCAD), Ames, Iowa, USA, October 2023. TU Wien Academic Press, 1-1, 2023 (abstract of keynote speech); DOI: 10.34727/2023/isbn.978-3-85448-060-0_1. [BibTeX] [Slides]

  • Maria Paola Bonacina, Stéphane Graham-Lengrand, and Christophe Vauthier. QSMA: a new algorithm for quantified satisfiability modulo theory and assignment.
    In Proceedings of the 29th International Conference on Automated Deduction (CADE), Rome, Italy, EU, July 2023. Springer, Lecture Notes in Artificial Intelligence 14132, 78-95, 2023; DOI: 10.1007/978-3-031-38499-8_5. [BibTeX] [Slides]

  • 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]

• 2022
  • Maria Paola Bonacina (Lead Guest Editor). Six Decades of Automated Reasoning: Papers in Memory of Larry Wos.
    Journal of Automated Reasoning, 66(4):437-584, November 2022. [Foreword with DOI: 10.1007/s10817-022-09637-z] and Springer Nature SharedIt]

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

  • Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar. CDSAT for nondisjoint theories with shared predicates: arrays with abstract length.
    In Proceedings of the 20th International Workshop on Satisfiability Modulo Theories (SMT) 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 3185:18-37, 2022. [BibTeX] [Slides]

  • 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, Philipp Rümmer, and Renate A. Schmidt (Editors). Integrated Deduction - Report from Dagstuhl Seminar 21371.
    Dagstuhl Publishing, Dagstuhl Reports 11(8):35-51, February 2022; DOI: 10.4230/DagRep.11.8.35. [BibTeX]

• 2021
  • Maria Paola Bonacina. Proof generation in CDSAT. (Abstract of keynote speech)
    In Proceedings of the 7th International Workshop on Proof eXchange in Theorem Proving (PxTP) satellite of the 28th International Conference on Automated Deduction (CADE), Pittsburgh, Pennsylvania, USA, July 2021. Open Publishing Association, Electronic Proceedings in Theoretical Computer Science 336:1-4, July 2021; DOI: 10.4204/EPTCS.336.1. [BibTeX] [Slides]

• 2020
  • 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 (nominated for best paper award); DOI: 10.1007/978-3-030-51074-9_20. [BibTeX] [Slides]

  • 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]

• 2019
  • Maria Paola Bonacina. Conflict-driven reasoning in unions of theories.
    In Proceedings of the 12th International Symposium on Frontiers of Combining Systems (FroCoS), London, England, UK, September 2019. Springer, Lecture Notes in Artificial Intelligence 11715, xi-xiii, 2019 (abstract of keynote speech). [BibTeX] [Slides]

  • Maria Paola Bonacina and Giulio Mazzi. The Eos SMT/SMA-solver: a preliminary report.
    In Proceedings of the 17th International Workshop on Satisfiability Modulo Theories (SMT) satellite of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT), 1-10, Lisbon, Portugal, EU, July 2019. [BibTeX]

  • Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, and Cesare Tinelli. Theory combination: beyond equality sharing.
    In Description Logic, Theory Combination, and All That: Essays Dedicated to Franz Baader. Springer, Lecture Notes in Artificial Intelligence 11560, 57-89, June 2019 (invited); DOI: 10.1007/978-3-030-22102-7_3. [BibTeX]

• 2018
  • Maria Paola Bonacina. Deduzione automatica.
    In Le Direzioni della Ricerca Logica in Italia - Volume 2. ETS Edizioni, Analitica, Chapter 3, 77-139, June 2018 (invited). [BibTeX] [Slides]

  • Maria Paola Bonacina. Parallel theorem proving.
    In Handbook of Parallel Constraint Reasoning. Springer, Chapter 6, 179-235, May 2018 (invited); DOI: 10.1007/978-3-319-63516-3_6. [BibTeX] [Slides]

  • Maria Paola Bonacina. On conflict-driven reasoning.
    In Proceedings of the 6th Workshop on Automated Formal Methods (AFM) satellite of the 9th NASA Formal Methods Symposium (NFM), Menlo Park, California, USA, May 2017. EasyChair Kalpa Publications in Computing 5, 31-49, April 2018; DOI: 10.29007/spwm. [BibTeX] [Slides]

  • Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar. Proofs in conflict-driven theory combination.
    In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP) satellite of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Los Angeles, California, USA, January 2018. ACM Press, 186-200, 2018; DOI: 10.1145/3167096 (©[ACM Inc.][2018]). [BibTeX] [Slides]

• 2017
  • Maria Paola Bonacina. Automated reasoning for explainable artificial intelligence.
    In Proceedings of the 1st Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE) satellite of the 26th International Conference on Automated Deduction (CADE), Gothenburg, Sweden, August 2017. EasyChair EPiC Series in Computing 51, 24-28, November 2017; DOI: 10.29007/4b7h. [BibTeX] [Slides]

  • Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar. Satisfiability modulo theories and assignments.
    In Proceedings of the 26th International Conference on Automated Deduction (CADE), Gothenburg, Sweden, August 2017. Springer, Lecture Notes in Artificial Intelligence 10395, 42-59, 2017 (nominated for best paper award); DOI: 10.1007/978-3-319-63046-5_4. [BibTeX] [Slides1] [Slides2]

  • 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]

• 2016
  • 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]

• 2015
  • 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 and Festschrift Symposium, Urbana Champaign, Illinois, USA, September 2015. Springer, Lecture Notes in Computer Science 9200, 181-204, 2015 (invited); DOI: 10.1007/978-3-319-23165-5_8. [BibTeX] [Slides]

  • 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, July 2014. EasyChair EPiC Series in Computing 31, 25-38, July 2015; DOI: 10.29007/m2vf. [BibTeX] [Slides]

  • 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]

• 2014
  • 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, July 2014. Technical Report 14-06, Research Institute for Symbolic Computation, Johannes Kepler Universität, Linz, 47-54, 2014. [BibTeX]

  • Maria Paola Bonacina and David A. Plaisted. Semantically-guided goal-sensitive theorem proving (Abstract).
    Annual Meeting of the IFIP Working Group in 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, July 2014 (Abstract of a technical report with the same title superseded by the journal articles on SGGS).

• 2013
  • Maria Paola Bonacina. On model-based reasoning: recent trends and current developments (Abstract).
    In Proceedings of the 28th Italian Conference on Computational Logic (CILC), Catania, Italy, September 2013. CEUR Proceedings 1068:9-9, 2013 (invited talk). [BibTeX] [Slides]

  • Maria Paola Bonacina. Two-stage interpolation systems (Abstract).
    In Proceedings of the 1st International Workshop on Interpolation: from Proofs to Applications (iPRA) satellite of the 25th International Conference on Computer Aided Verification (CAV), Saint Petersburg, Russia, July 2013. Technical Report, Technische Universität Wien, 2013. [BibTeX]

  • Maria Paola Bonacina (Editor). Proceedings of the 24th International Conference on Automated Deduction (CADE-24).
    Springer, Lecture Notes in Artificial Intelligence 7898, XVI 466 p. 95 illus., June 2013; ISBN: 978-3-642-38573-5; DOI: 10.1007/978-3-642-38574-2. [Preface] [BibTeX]

  • Maria Paola Bonacina and Nachum Dershowitz. Canonical ground Horn theories.
    In Programming Logics: Essays in Memory of Harald Ganzinger. Springer, Lecture Notes in Artificial Intelligence 7797, 35-71, March 2013 (invited); DOI: 10.1007/978-3-642-37651-1_3. [BibTeX] [Slides]

  • Maria Paola Bonacina and Mark E. Stickel (Editors). Automated Reasoning and Mathematics: Essays in Memory of William W. McCune.
    Springer, Lecture Notes in Artificial Intelligence 7788, XX 259 p. 27 illus., March 2013; ISBN: 978-3-642-36674-1; DOI: 10.1007/978-3-642-36675-8. [Preface] [BibTeX]

• 2012
  • Maria Paola Bonacina and Maribel Fernández (Editors). Proceedings of the 2nd Workshop on Strategies in Rewriting Proving and Programming (IWS).
    Satellite of the 6th International Joint Conference on Automated Reasoning (IJCAR), Manchester, England, UK, June 2012. [Preface]

• 2011
  • 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 Moa Johansson. Towards interpolation in an SMT solver with integrated superposition.
    In Proceedings of the 9th International Workshop on Satisfiability Modulo Theories (SMT) satellite of the 23rd International Conference on Computer Aided Verification (CAV), Snowbird, Utah, USA, July 2011. Technical Report No. UCB/EECS-2011-80, Department of Electrical Engineering and Computer Sciences, University of California at Berkeley, 2011. [BibTeX]

  • Maria Paola Bonacina and Moa Johansson. On interpolation in decision procedures.
    In Proceedings of the 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), Bern, Switzerland, July 2011. Springer, Lecture Notes in Artificial Intelligence, 6793, 1-16, 2011 (invited talk); DOI: 10.1007/978-3-642-22119-4_1. [BibTeX]

• 2010
  • Maria Paola Bonacina. On theorem proving for program checking - Historical perspective and recent developments.
    In Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP), Schloss Hagenberg, Linz, Austria, July 2010. ACM Press, 1-11, 2010 (invited talk); DOI: 10.1145/1836089.1836090 (©[ACM Inc.][2010]). [BibTeX] [Slides]

  • 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]

• 2009
  • Maria Paola Bonacina, Christopher A. Lynch, and Leonardo de Moura. On deciding satisfiability by DPLL(Γ+T) and unsound theorem proving.
    In Proceedings of the 22nd International Conference on Automated Deduction (CADE), Montréal, Canada, August 2009. Springer, Lecture Notes in Artificial Intelligence 5663, 35-50, 2009; DOI: 10.1007/978-3-642-02959-2_3. [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]

• 2008
  • Maria Paola Bonacina and Nachum Dershowitz. Canonical inference for implicational systems.
    In Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR), Sydney, Australia, August 2008. Springer, Lecture Notes in Artificial Intelligence 5195, 380-395, 2008; DOI: 10.1007/978-3-540-71070-7_33. [BibTeX] [Slides]

  • 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]

• 2007
  • Maria Paola Bonacina and Mnacho Echenim. T-decision by decomposition.
    In Proceedings of the 21st International Conference on Automated Deduction (CADE), Bremen, Germany, July 2007. Springer, Lecture Notes in Artificial Intelligence 4603, 199-214, 2007; DOI: 10.1007/978-3-540-73595-3_14. [BibTeX]

  • Maria Paola Bonacina and Mnacho Echenim. Decision procedures for variable-inactive theories and two polynomial T-satisfiability procedures (Position paper).
    In Proceedings of the 1st Workshop on Automated Deduction: Decidability, Complexity, Tractability (ADDCT) satellite of the 21st International Conference on Automated Deduction (CADE), 65-67, Bremen, Germany, July 2007. [BibTeX]

  • Maria Paola Bonacina and Mnacho Echenim. Rewrite-based decision procedures.
    In Proceedings of the 6th Workshop on Strategies in Automated Deduction (STRATEGIES) satellite of the 3rd International Joint Conference on Automated Reasoning (IJCAR) held at the 4th Federated Logic Conference (FLoC), Seattle, Washington, USA, August 2006. Elsevier, Electronic Notes in Theoretical Computer Science, 174(11):27-45, July 2007; DOI: 10.1016/j.entcs.2006.11.042. [BibTeX]

  • Maria Paola Bonacina and Mnacho Echenim. Rewrite-based satisfiability procedures for recursive data structures.
    In Proceedings of the 4th Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR) satellite of the 3rd International Joint Conference on Automated Reasoning (IJCAR) held at the 4th Federated Logic Conference (FLoC), Seattle, Washington, USA, August 2006. Elsevier, Electronic Notes in Theoretical Computer Science, 174(8):55-70, June 2007; DOI: 10.1016/j.entcs.2006.11.039. [BibTeX]

  • Maria Paola Bonacina and Mnacho Echenim. Generic theorem proving for decision procedures.
    Research Report 41/2006, Dipartimento di Informatica, Università degli Studi di Verona, August 2006 (revised March 2007), 1-46. [BibTeX]

  • 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]

• 2006
  • Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, and Daniele Zucchelli. Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures.
    In Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR), Seattle, Washington, USA, August 2006. Springer, Lecture Notes in Artificial Intelligence 4130, 513-527, 2006; DOI: 10.1007/11814771_42. [BibTeX]

  • Maria Paola Bonacina and Alberto Martelli. Automated reasoning.
    Intelligenza Artificiale, 3(1/2):14-20 (Special issue on Artificial Intelligence 50th Anniversary 1956-2006) June 2006 (invited). [BibTeX] [Slides]

  • Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, and Daniele Zucchelli. Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures.
    Internal Report No. 308-06, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, May 2006, 1-20. [BibTeX]

• 2005
  • Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, and Stephan Schulz. On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal.
    In Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS), Vienna, Austria, September 2005. Springer, Lecture Notes in Artificial Intelligence 3717, 65-80, 2005; DOI: 10.1007/11559306_4. [BibTeX] [Slides]

  • Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, and Stephan Schulz. Big proof engines as little proof engines: new results on rewrite-based satisfiability procedures (Extended abstract).
    In Proceedings of the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR) satellite of the 17th International Conference on Computer Aided Verification (CAV), 33-41, Edinburgh, Scotland, UK, July 2005. [BibTeX] [Slides]

  • Stephan Schulz and Maria Paola Bonacina. On handling distinct objects in the superposition calculus.
    In Proceedings of the 5th International Workshop on the Implementation of Logics (IWIL) satellite of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 66-77, Montevideo, Uruguay, March 2005. [BibTeX]

  • Maria Paola Bonacina and Thierry Boy de la Tour (Editors). 5th Workshop on Strategies in Automated Deduction: Selected Papers.
    Elsevier, Electronic Notes in Theoretical Computer Science 125(2):1-164, March 2005. [Preface with DOI: 10.1016/j.entcs.2005.02.001]

  • 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]

• 2002
  • Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Michaël Rusinowitch, and Aditya Kumar Sehgal. High-performance deduction for verification: a case study in the theory of arrays.
    In Proceedings of the 2nd International Workshop on Verification (VERIFY) satellite of the 18th International Conference on Automated Deduction (CADE) held at the3rd Federated Logic Conference (FLoC), Copenhagen, Denmark, July 2002. Technical Report 07/2002, DIKU, Copenhagen, 103-112, 2002. [BibTeX] [Slides at the Meeting of the IFIP Working Group on Term Rewriting (WG 1.6)] [Slides of a colloquium at IMAG, INPG, Grenoble, France, November 2002]

• 2001
  • Maria Paola Bonacina and Bernhard Gramlich (Editors). 4th Workshop on Strategies in Automated Deduction: Selected Papers.
    Elsevier, Electronic Notes in Theoretical Computer Science 58(2):117-208, October 2001. [Preface with DOI: 10.1016/S1571-0661(05)80580-8]

  • Maria Paola Bonacina. Combination of distributed search and multi-search in Peers-mcd.d.
    In Proceedings of the 1st International Joint Conference on Automated Reasoning (IJCAR), Siena, Italy, June 2001. Springer, Lecture Notes in Artificial Intelligence 2083, 448-452, 2001; DOI: 10.1007/3-540-45744-5_37. [BibTeX] [Slides]

• 2000
  • 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 and Ulrich Furbach (Editors). Advances in First-order Theorem Proving.
    Academic Press, Journal of Symbolic Computation 29(2), special issue, February 2000. [Preface]

• 1999
  • 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. A taxonomy of theorem-proving strategies.
    In Artificial Intelligence Today - Recent Trends and Developments. Springer, Lecture Notes in Artificial Intelligence 1600, 43-84, August 1999 (invited); DOI: 10.1007/3-540-48317-9_3. [BibTeX] [Slides of colloquia at the University of Oregon, Eugene, OR, USA, and at the Università degli Studi di Roma "La Sapienza", Italy, May 2000]

  • Maria Paola Bonacina. Ten years of parallel theorem proving: a perspective.
    In Proceedings of the 3rd International Workshop on Strategies in Automated Deduction (STRATEGIES) satellite of the 16th International Conference on Automated Deduction (CADE) held at the 2nd Federated Logic Conference (FLoC), 3-15, Trento, Italy, July 1999 (invited talk). [BibTeX] [Slides]

• 1998
  • 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. Theorem proving strategies: a search-oriented taxonomy (Position paper).
    In Proceedings of the 2nd International Workshop on First-order Theorem Proving (FTP), Schloss Wilhelminenberg, Vienna, Austria, November 1998. Technical Report E1852-GS-981, Technische Universität Wien, 256-259, 1998. [BibTeX]

  • Maria Paola Bonacina. Analysis of distributed-search contraction-based strategies.
    In Proceedings of the 6th European Workshop on Logics in Artificial Intelligence (JELIA), Schloss Dagstuhl, Germany, October 1998. Springer, Lecture Notes in Artificial Intelligence 1489, 107-121, 1998; DOI: 10.1007/3-540-49545-2_8. [BibTeX]

  • Maria Paola Bonacina. Mechanical proofs of the Levi commutator problem.
    In Proceedings of the Workshop on Problem Solving Methodologies with Automated Deduction satellite of the 15th International Conference on Automated Deduction (CADE), 1-10, Lindau, Germany, July 1998. [BibTeX] [Slides]

  • Maria Paola Bonacina. Strategy analysis: from sequential to parallel strategies (Position paper).
    In Proceedings of the 2nd Workshop on Strategies in Automated Deduction (STRATEGIES) satellite of the 15th International Conference on Automated Deduction (CADE), 19-21, Lindau, Germany, July 1998. [BibTeX]

  • 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]

• 1997
  • Maria Paola Bonacina. On the representation of parallel search in theorem proving (Extended abstract).
    In Proceedings of the 1st International Workshop on First-order Theorem Proving (FTP), Schloss Hagenberg, Linz, Austria, October 1997. Technical Report 97-50, Research Institute for Symbolic Computation, Johannes Kepler Universität, Linz, 22-28, 1997. [BibTeX] [Slides]

  • Maria Paola Bonacina and Ulrich Furbach (Editors). Proceedings of the 1st International Workshop on First-order Theorem Proving (FTP).
    Schloss Hagenberg, Linz, Austria, October 1997. Technical Report 97-50, Research Institute for Symbolic Computation, Johannes Kepler Universität, Linz, 1997. [Preface]

  • Maria Paola Bonacina. Experiments with subdivision of search in distributed theorem proving.
    In Proceedings of the 2nd International Symposium on Parallel Symbolic Computation (PASCO), Maui, Hawaii, USA, July 1997. ACM Press, 88-100, 1997; DOI: 10.1145/266670.266696 (©[ACM Inc.][1997]). [BibTeX]

  • Maria Paola Bonacina. The Clause-Diffusion theorem prover Peers-mcd.
    In Proceedings of the 14th International Conference on Automated Deduction (CADE), Townsville, Australia, July 1997. Springer, Lecture Notes in Artificial Intelligence 1249, 53-56, 1997; DOI: 10.1007/3-540-63104-6_6. [BibTeX] [Slides]

  • Maria Paola Bonacina. Machine-independent evaluation of theorem-proving strategies (Position paper).
    In Proceedings of the 1st Workshop on Strategies in Automated Deduction (STRATEGIES) satellite of the 14th International Conference on Automated Deduction (CADE), 37-39, Townsville, Australia, July 1997. [BibTeX]

  • Maria Paola Bonacina and Jieh Hsiang. On the notion of complexity of search in theorem proving (Abstract).
    Logic Colloquium 1996, San Sebastiàn, Spain, July 1996. Bulletin of Symbolic Logic, 3(2):253-254, June 1997. [BibTeX]

  • Maria Paola Bonacina. A note on the analysis of theorem-proving strategies.
    Newsletter of the Association for Automated Reasoning, 36:2-8, April 1997. [BibTeX]

• 1996
  • Maria Paola Bonacina and Jieh Hsiang. On the representation of dynamic search spaces in theorem proving.
    In Proceedings of the International Computer Symposium, 85-94, Kaohshiung, Taiwan, ROC, December 1996. [BibTeX]

  • Maria Paola Bonacina and Jieh Hsiang. On semantic resolution with lemmaizing and contraction.
    In Proceedings of the 4th Pacific Rim International Conference on Artificial Intelligence (PRICAI), Cairns, Australia, August 1996. Springer, Lecture Notes in Artificial Intelligence 1114, 372-386, 1996; DOI: 10.1007/3-540-61532-6_32. [BibTeX] [Slides]

  • Maria Paola Bonacina. A note on the analysis of theorem-proving strategies.
    Technical Report, Department of Computer Science, The University of Iowa, May 1996, 1-12. [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. Future directions of automated deduction: Strategy analysis for theorem proving.
    NSF Workshop on Future Directions of Automated Deduction, Chicago, Illinois, USA, April 1996. [BibTeX]

  • Maria Paola Bonacina. Future directions of automated deduction: Distributed automated deduction.
    NSF Workshop on Future Directions of Automated Deduction, Chicago, Illinois, USA, April 1996. [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]

• 1995
  • 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]

• 1994
  • Maria Paola Bonacina. On the reconstruction of proofs in distributed theorem proving with contraction: a modified Clause-Diffusion method.
    In Proceedings of the 1st International Symposium on Parallel Symbolic Computation (PASCO), Schloss Hagenberg, Linz, Austria, September 1994. World Scientific, Lecture Notes Series in Computing 5, 22-33, 1994. [BibTeX] [Slides]

  • Hantao Zhang and Maria Paola Bonacina. Cumulating search in a distributed computing environment: a case study in parallel satisfiability.
    In Proceedings of the 1st International Symposium on Parallel Symbolic Computation (PASCO), Schloss Hagenberg, Linz, Austria, September 1994. World Scientific, Lecture Notes Series in Computing 5, 422-431, 1994. [BibTeX] [Slides]

  • Maria Paola Bonacina and William W. McCune. Distributed theorem proving by Peers.
    In Proceedings of the 12th International Conference on Automated Deduction (CADE), Nancy, France, EU, June 1994. Springer, Lecture Notes in Artificial Intelligence 814, 841-845, 1994; DOI: 10.1007/3-540-58156-1_72. [BibTeX] [Slides]

  • 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]

• 1993
  • Maria Paola Bonacina and Jieh Hsiang. Distributed deduction by Clause-Diffusion: the Aquarius prover.
    In Proceedings of the 3rd International Symposium on Design and Implementation of Symbolic Computation Systems (DISCO), Gmunden, Austria, September 1993. Springer, Lecture Notes in Computer Science 722, 272-287, 1993; DOI: 10.1007/BFb0013183. [BibTeX] [Slides]

  • Maria Paola Bonacina and Jieh Hsiang. On fairness in distributed automated deduction.
    In Proceedings of the 10th Annual Symposium on Theoretical Aspects of Computer Science (STACS), Würzburg, Germany, February 1993. Springer, Lecture Notes in Computer Science 665, 141-152, 1993; DOI: 10.1007/3-540-56503-5_17. [BibTeX] [Slides]

• 1992
  • Maria Paola Bonacina. Distributed automated deduction.
    Ph.D. Thesis, Department of Computer Science, State University of New York at Stony Brook, December 1992. [BibTeX] [Slides]

  • 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 and Jieh Hsiang. A system for distributed simplification-based theorem proving (Project summary).
    In Proceedings of the 1st International Workshop on Parallelization in Inference Systems, Schloss Dagstuhl, Germany, December 1990. Springer, Lecture Notes in Artificial Intelligence 590, 370-370, 1992; DOI: 10.1007/3-540-55425-4_18. [BibTeX]

  • Maria Paola Bonacina and Jieh Hsiang. Incompleteness of the RUE/NRF inference systems.
    Newsletter of the Association for Automated Reasoning, 20:9-12, May 1992. [BibTeX]

  • Maria Paola Bonacina and Jieh Hsiang. High performance simplification-based automated deduction.
    In Transactions of the 9th US Army Conference on Applied Mathematics and Computing, Minneapolis, Minnesota, USA, June 1991. ARO Report 92-1, 321-335, 1992. [BibTeX]

• 1991
  • Maria Paola Bonacina and Jieh Hsiang. A category theory approach to completion-based theorem proving strategies (Abstract).
    International Conference on Category Theory 1991, Montréal, Canada, June 1991 (Full version). [BibTeX]

  • Maria Paola Bonacina. Problems in Lukasiewicz logic.
    Newsletter of the Association for Automated Reasoning, 18:5-12, June 1991. [BibTeX]

  • Maria Paola Bonacina and Jieh Hsiang. On fairness of completion-based theorem proving strategies.
    In Proceedings of the 4th International Conference on Rewriting Techniques and Applications (RTA), Como, Italy, April 1991. Springer, Lecture Notes in Computer Science 488, 348-360, 1991; DOI: 10.1007/3-540-53904-2_109. [BibTeX]

  • Maria Paola Bonacina and Jieh Hsiang. Completion procedures as semidecision procedures.
    In Proceedings of the 2nd International Workshop on Conditional and Typed Term Rewriting Systems (CTRS), Montréal, Canada, June 1990. Springer, Lecture Notes in Computer Science 516, 206-232, 1991 (invited); DOI: 10.1007/3-540-54317-1_92. [BibTeX]

  • Siva Anantharaman and Maria Paola Bonacina. An application of automated equational reasoning to many-valued logic.
    In Proceedings of the 2nd International Workshop on Conditional and Typed Term Rewriting Systems (CTRS), Montréal, Canada, June 1990. Springer, Lecture Notes in Computer Science 516, 156-161, 1991; DOI: 10.1007/3-540-54317-1_88. [BibTeX] (This version in the post-workshop proceedings replaced the version presented at the workshop entitled An application of the theorem prover SBR3 to many-valued logic.)

• 1990
  • Maria Paola Bonacina. Sulla dimostrazione di teoremi per completamento.
    Thesis of Dottorato di Ricerca, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, Milano, Italy, December 1990 (defended in Milano in front of a Departmental committee in January 1991, and in Rome in front of a national committee in July 1991).
    Available in English with title On completion theorem proving, as Technical Report of the Department of Computer Science, State University of New York at Stony Brook, December 1990. [BibTeX]

  • Maria Paola Bonacina and Jieh Hsiang. Operational and denotational semantics of rewrite programs.
    In Proceedings of the North American Conference on Logic Programming (previously Symposium on Logic Programming and later renamed International Symposium on Logic Programming), Austin, Texas, USA, October 1990. MIT Press, Logic Programming Series, 449-464, 1990. [BibTeX]

  • Siva Anantharaman, Nirina Andrianarivelo, Maria Paola Bonacina and Jieh Hsiang. SBR3: a refutational prover for equational theorems.
    Technical Report, Department of Computer Science, State University of New York at Stony Brook, May 1990, 1-6. [BibTeX]

• 1989
  • Siva Anantharaman and Maria Paola Bonacina. Automated proofs in Lukasiewicz logic.
    Technical Report, Department of Computer Science, State University of New York at Stony Brook, November 1989 and Rapport de Recherche No. 89-11, LIFO Orléans, 1-14. [BibTeX]

  • Fabio Baj, Maria Paola Bonacina, Massimo Bruschi and Antonella Zanzi. Another term rewriting based proof of the `non-obvious' theorem.
    Newsletter of the Association for Automated Reasoning, 13:4-8, September 1989. [BibTeX]

  • Maria Paola Bonacina and Giancarlo Sanna. KBlab: an equational theorem prover for the Macintosh.
    In Proceedings of the 3rd International Conference on Rewriting Techniques and Applications (RTA), Chapel Hill, North Carolina, USA, April 1989. Springer, Lecture Notes in Computer Science 355, 548-550, 1989; DOI: 10.1007/3-540-51081-8_135. [BibTeX]

• 1987
  • Maria Paola Bonacina. Petri nets for knowledge representation.
    Petri Nets Newsletter, 27:28-36, August 1987. [BibTeX]

• 1986
  • Maria Paola Bonacina. L'algoritmo di Knuth-Bendix.
    Thesis of Laurea (undergraduate), Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, Milano, Italy, July 1986.

Maria Paola Bonacina