Articles in proceedings of conferences, symposia and workshops

• Maria Paola Bonacina and Moa Johansson.
  Towards interpolation in an SMT solver with integrated superposition.
  In Notes of the Ninth International Workshop on Satisfiability Modulo Theories (SMT), Twenty-Third 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, 9-18, 2011. [BibTeX entry]

• Maria Paola Bonacina and Moa Johansson.
  On interpolation in decision procedures.
  In Proceedings of the Twentieth 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). [BibTeX entry]

• Maria Paola Bonacina.
  On theorem proving for program checking - Historical perspective and recent developments.
  In Proceedings of the Twelfth International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP) (©Copyright 2010 by ACM, Inc.) Schloss Hagenberg, Linz, Austria, July 2010. ACM Press, 1-11, 2010 (invited). [BibTeX entry]

• Maria Paola Bonacina, Christopher A. Lynch and Leonardo de Moura.
  On deciding satisfiability by DPLL(Γ+T) and unsound theorem proving.
  In Proceedings of the Twenty-second 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 entry]

• Maria Paola Bonacina and Nachum Dershowitz.
  Canonical inference for implicational systems.
  In Proceedings of the Fourth International Joint Conference on Automated Reasoning (IJCAR), Sydney, Australia, August 2008. Springer, Lecture Notes in Artificial Intelligence 5195, 380-395, 2008. [BibTeX entry]

• Maria Paola Bonacina and Mnacho Echenim.
  T-decision by decomposition.
  In Proceedings of the Twenty-first International Conference on Automated Deduction (CADE), Bremen, Germany, July 2007. Springer, Lecture Notes in Artificial Intelligence 4603, 199-214, 2007. [BibTeX entry]

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

• Maria Paola Bonacina and Mnacho Echenim.
  Rewrite-based decision procedures.
  In Proceedings of the Sixth Workshop on Strategies in Automated Deduction (STRATEGIES), Third International Joint Conference on Automated Reasoning (IJCAR) and Fourth 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 entry]

• Maria Paola Bonacina and Mnacho Echenim.
  Rewrite-based satisfiability procedures for recursive data structures.
  In Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), Third International Joint Conference on Automated Reasoning (IJCAR) and Fourth Federated Logic Conference (FLoC), Seattle, Washington, USA, August 2006. Elsevier, Electronic Notes in Theoretical Computer Science, 174(8):55-70, June 2007. [BibTeX entry]

• 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 Third International Joint Conference on Automated Reasoning (IJCAR), Seattle, Washington, USA, August 2006. Springer, Lecture Notes in Artificial Intelligence 4130, 513-527, 2006. [BibTeX entry]

• 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 Fifth International Workshop on Frontiers of Combining Systems (FroCoS), Vienna, Austria, September 2005. Springer, Lecture Notes in Artificial Intelligence 3717, 65-80, 2005. [BibTeX entry]

• 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 Notes of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), Seventeenth International Conference on Computer Aided Verification (CAV), 33-41, Edinburgh, Scotland, UK, July 2005. [BibTeX entry]

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

• 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 Notes of the Second International Workshop on Verification (VERIFY), Third Federated Logic Conference (FLoC), Copenhagen, Denmark, July 2002. Technical Report 07/2002, DIKU, Copenhagen, 103-112, 2002. [BibTeX entry]

• Maria Paola Bonacina.
  Combination of distributed search and multi-search in Peers-mcd.d.
  In Proceedings of the First International Joint Conference on Automated Reasoning (IJCAR), Siena, Italy, June 2001. Springer, Lecture Notes in Artificial Intelligence 2083, 448-452, 2001. [BibTeX entry]

• Maria Paola Bonacina.
  Ten years of parallel theorem proving: a perspective.
  In Notes of the Third International Workshop on Strategies in Automated Deduction, Second Federated Logic Conference (FLoC), 3-15, Trento, Italy, July 1999 (invited). [BibTeX entry]

• Maria Paola Bonacina.
  Theorem proving strategies: a search-oriented taxonomy (Position paper).
  In Proceedings of the Second 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 entry]

• Maria Paola Bonacina.
  Analysis of distributed-search contraction-based strategies.
  In Proceedings of the Sixth 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 entry]

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

• Maria Paola Bonacina.
  Strategy analysis: from sequential to parallel strategies (Position paper).
  In Notes of the Second Workshop on Strategies in Automated Deduction, Fifteenth International Conference on Automated Deduction (CADE), 19-21, Lindau, Germany, July 1998. [BibTeX entry]

• Maria Paola Bonacina.
  On the representation of parallel search in theorem proving (Extended abstract).
  In Proceedings of the First 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 entry]

• Maria Paola Bonacina.
  Experiments with subdivision of search in distributed theorem proving.
  In Proceedings of the Second International Symposium on Parallel Symbolic Computation (PASCO) (©Copyright 1997 by ACM, Inc.) Wailea, Maui, Hawaii, USA, July 1997. ACM Press, 88-100, 1997. [BibTeX entry]

• Maria Paola Bonacina.
  The Clause-Diffusion theorem prover Peers-mcd.
  In Proceedings of the Fourteenth International Conference on Automated Deduction (CADE), Townsville, Australia, July 1997. Springer, Lecture Notes in Artificial Intelligence 1249, 53-56, 1997. [BibTeX entry]

• Maria Paola Bonacina.
  Machine-independent evaluation of theorem-proving strategies (Position paper).
  In Notes of the First Workshop on Strategies in Automated Deduction, Fourteenth International Conference on Automated Deduction (CADE), 37-39, Townsville, Australia, July 1997. [BibTeX entry]

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

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

• Maria Paola Bonacina and Jieh Hsiang.
  On semantic resolution with lemmaizing and contraction.
  In Proceedings of the Fourth Pacific Rim International Conference on Artificial Intelligence (PRICAI), Cairns, Australia, August 1996. Springer, Lecture Notes in Artificial Intelligence 1114, 372-386, 1996. [BibTeX entry]

• Maria Paola Bonacina.
  On the reconstruction of proofs in distributed theorem proving with contraction: a modified Clause-Diffusion method.
  In Proceedings of the First 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 entry]

• Hantao Zhang and Maria Paola Bonacina.
  Cumulating search in a distributed computing environment: a case study in parallel satisfiability.
  In Proceedings of the First 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 entry]

• Maria Paola Bonacina and William W. McCune.
  Distributed theorem proving by Peers.
  In Proceedings of the Twelfth International Conference on Automated Deduction (CADE), Nancy, France, June 1994. Springer-Verlag, Lecture Notes in Artificial Intelligence 814, 841-845, 1994. [BibTeX entry]

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

• Maria Paola Bonacina and Jieh Hsiang.
  On fairness in distributed deduction.
  In Proceedings of the Tenth Annual Symposium on Theoretical Aspects of Computer Science (STACS), Würzburg, Germany, February 1993. Springer-Verlag, Lecture Notes in Computer Science 665, 141-152, 1993. [BibTeX entry]

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

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

• Maria Paola Bonacina and Jieh Hsiang.
  On fairness of completion-based theorem proving strategies.
  In Proceedings of the Fourth International Conference on Rewriting Techniques and Applications (RTA), Como, Italy, April 1991. Springer-Verlag, Lecture Notes in Computer Science 488, 348-360, 1991. [BibTeX entry]

• Maria Paola Bonacina and Jieh Hsiang.
  Completion procedures as semidecision procedures.
  In Proceedings of the Second International Workshop on Conditional and Typed Term Rewriting Systems (CTRS), Montréal, Canada, June 1990. Springer-Verlag, Lecture Notes in Computer Science 516, 206-232, 1991 (invited). [BibTeX entry]

• Siva Anantharaman and Maria Paola Bonacina.
  An application of automated equational reasoning to many-valued logic.
  In Proceedings of the Second International Workshop on Conditional and Typed Term Rewriting Systems (CTRS), Montréal, Canada, June 1990. Springer-Verlag, Lecture Notes in Computer Science 516, 156-161, 1991. [BibTeX entry]

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

• Maria Paola Bonacina and Giancarlo Sanna.
  KBlab: an equational theorem prover for the Macintosh.
  In Proceedings of the Third International Conference on Rewriting Techniques and Applications (RTA), Chapel Hill, North Carolina, April 1989. Springer-Verlag, Lecture Notes in Computer Science 355, 548-550, 1989. [BibTeX entry]

Maria Paola Bonacina