- Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar.

Proofs in conflict-driven theory combination.

In*Proceedings of the Seventh ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)*,*Forty-Fifth 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] - Maria Paola Bonacina.

On conflict-driven reasoning.

In*Proceedings of the Sixth Workshop on Automated Formal Methods (AFM)*,*Ninth NASA Formal Methods Symposium (NFM)*, Menlo Park, California, USA, May 2017. EasyChair Kalpa Publications in Computing, 1-17, in press,**2018**. [BibTeX] [Slides] (Early version at AFM 2017) - Maria Paola Bonacina.

Automated reasoning for explainable artificial intelligence.

In Proceedings of the First Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE),*Twenty-Sixth International Conference on Automated Deduction (CADE)*, Gothenburg, Sweden, August 2017. EasyChair EPiC Series in Computing 51, 24-28, November**2017**. [BibTeX] [Slides] - Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar.

Satisfiability modulo theories and assignments.

In*Proceedings of the Twenty-Sixth International Conference on Automated Deduction (CADE)*, Gothenburg, Sweden, August 2017. Springer, Lecture Notes in Artificial Intelligence 10395, 42-59,**2017**; DOI: 10.1007/978-3-319-63046-5_4. [BibTeX] [Slides of a talk given at the Big Proof Program, Isaac Newton Institute for Mathematical Sciences, Cambridge, England, UK, July 2017] - Maria Paola Bonacina and David A. Plaisted.

SGGS theorem proving: an exposition.

In Proceedings of the Fourth Workshop on Practical Aspects in Automated Reasoning (PAAR),*Seventh International Joint Conference on Automated Reasoning (IJCAR)*and*Sixth Federated Logic Conference (FLoC)*, Vienna, Austria, July 2014. EasyChair EPiC Series in Computing 31, 25-38, July**2015**. [BibTeX] [Extended version of the slides based also on colloquia at MPI Saarbrücken in June 2014 and Koblenz in September 2014] - Maria Paola Bonacina and David A. Plaisted.

Constraint manipulation in SGGS.

In*Notes of the Twenty-Eighth Workshop on Unification (UNIF)*,*Seventh International Joint Conference on Automated Reasoning (IJCAR)*and*Sixth 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)*,*Sixth Federated Logic Conference (FLoC)*, Vienna, Austria, July**2014**. [Slides] - Maria Paola Bonacina.

On model-based reasoning: recent trends and current developments (Abstract).

In*Proceedings of the Twenty-Eighth Italian Conference on Computational Logic (CILC)*, Catania, Italy, September 2013. CEUR Proceedings 1068:9-9,**2013**(**invited**). [BibTeX] [Slides] - Maria Paola Bonacina.

Two-stage interpolation systems (Abstract).

In*Notes of the First International Workshop on Interpolation: from Proofs to Applications (IPrA), Twenty-fifth International Conference on Computer Aided Verification (CAV)*, Saint Petersburg, Russia, July 2013. Technical Report, Technische Universität Wien,**2013**. [BibTeX] - 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] - 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**); DOI: 10.1007/978-3-642-22119-4_1. [BibTeX] - 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)*, Schloss Hagenberg, Linz, Austria, July 2010. ACM Press, 1-11,**2010**(**invited**); DOI: 10.1145/1836089.1836090 (©[ACM Inc.][2010]). [BibTeX] [Slides] - 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] [Slides] [Slides of colloquia at ETHZ and EPFL, Switzerland, April 2009] - 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**; DOI: 10.1007/978-3-540-71070-7_33. [BibTeX] [Slides] - 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**; 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*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] - 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] - 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**; DOI: 10.1016/j.entcs.2006.11.039. [BibTeX] - 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**; DOI: 10.1007/11814771_42. [BibTeX] - 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**; 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*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] [Slides] - 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] - 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] [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] - 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**; DOI: 10.1007/3-540-45744-5_37. [BibTeX] [Slides] - Maria Paola Bonacina.

Ten years of parallel theorem proving: a perspective.

In*Notes of the Third International Workshop on Strategies in Automated Deduction (STRATEGIES), Second Federated Logic Conference (FLoC)*, 3-15, Trento, Italy, July**1999**(**invited**). [BibTeX] [Slides] - 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] - 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] - 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] [Slides] - Maria Paola Bonacina.

Strategy analysis: from sequential to parallel strategies (Position paper).

In*Notes of the Second Workshop on Strategies in Automated Deduction (STRATEGIES), Fifteenth International Conference on Automated Deduction (CADE)*, 19-21, Lindau, Germany, July**1998**. [BibTeX] - 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] [Slides] - Maria Paola Bonacina.

Experiments with subdivision of search in distributed theorem proving.

In*Proceedings of the Second International Symposium on Parallel Symbolic Computation (PASCO)*, Wailea, 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 Fourteenth 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*Notes of the First Workshop on Strategies in Automated Deduction (STRATEGIES), Fourteenth 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 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 Fourth 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.

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

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, 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 deduction.

In*Proceedings of the Tenth 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] - 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] - Maria Paola Bonacina and Jieh Hsiang.

A system for distributed simplification-based theorem proving.

In Bertrand Fronhöfer and Graham Wrightson (Eds.)*Proceedings of the First 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.

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 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, 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 Second 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 Second 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.) - 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] - 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, Lecture Notes in Computer Science 355, 548-550,**1989**; DOI: 10.1007/3-540-51081-8_135. [BibTeX]