- 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. (An earlier version was presented at the
Dagstuhl Seminar 01101 on Deduction, 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-4):149-199, December 1999;
DOI: 10.1023/A:1018919214722.
- 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. - 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.
- Maria Paola Bonacina.
Theorem proving strategies: a search-oriented taxonomy.
In
*Notes of the Second International Workshop on First-order Theorem Proving*(FTP 1998), Schloss Wilhelminenberg, Vienna, Austria, Techical Report E1852-GS-981, Technische Universität Wien, 256-259, November 1998. - Maria Paola Bonacina.
Analysis of distributed-search contraction-based strategies.
*Proceedings of the Sixth Joint European Workshop on Logics in Artificial Intelligence (JELIA)*, Springer, Lecture Notes in Artificial Intelligence 1489, 107-121, October 1998; DOI: 10.1007/3-540-49545-2_8. - Maria Paola Bonacina.
Strategy analysis: from sequential to parallel strategies.
In
*Notes of the Second Workshop on Strategies in Automated Deduction*(STRATEGIES 1998),*CADE-15*, 19-21, Lindau, Germany, July 1998. - Maria Paola Bonacina.
On the representation of parallel search in theorem proving.
In
*Notes of the First International Workshop on First-order Theorem Proving*(FTP 1997), Schloss Hagenberg, Linz, Austria, October 1997. Technical Report 97-50, RISC, Johannes Kepler Universität, Linz, 22-28, 1997. - Maria Paola Bonacina.
Machine-independent evaluation of theorem-proving strategies.
In
*Notes of the First Workshop on Strategies in Automated Deduction*(STRATEGIES 1997),*CADE-14*, 37-39, Townsville, Queensland, Australia, July 1997. - Maria Paola Bonacina and Jieh Hsiang.
On the notion of complexity of search in theorem proving.
*Logic Colloquium 1996*, San Sebastiàn, Spain, July 1996.*Bulletin of Symbolic Logic*, 3(2):253-254, June 1997. - Maria Paola Bonacina.
A note on the analysis of theorem-proving strategies.
*Newsletter of the Association for Automated Reasoning*, 36:2-8, April 1997. - Maria Paola Bonacina and Jieh Hsiang.
On the representation of dynamic search spaces in theorem proving.
In
*Proceedings of the International Conference on Artificial Intelligence, International Computer Symposium*, 85-94, National Sun-Yat Sen University, Kaohshiung, Taiwan, ROC, December 1996. - 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.
- Maria Paola Bonacina. Future directions of automated deduction: Strategy analysis for theorem proving. National Science Foundation Workshop on the Future Directions of Automated Deduction, Chicago, Illinois, USA, April 1996.

- 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.
- 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).