KBlab: An Equational Theorem Prover for the Macintosh. - Maria Paola Bonacina; Giancarlo Sanna (RTA, 1989)

An Application of Automated Equational Reasoning to Many-valued Logic. - Siva Anantharaman; Maria Paola Bonacina (CTRS, 1990)

Completion Procedures as Semidecision Procedures. - Maria Paola Bonacina; Jieh Hsiang (CTRS, 1990)

A System for Distributed Simplification-Based Theorem Proving. - Maria Paola Bonacina; Jieh Hsiang (Dagstuhl Seminar on Parallelization in Inference Systems, 1990)

Operational and Denotational Semantics of Rewrite Programs. - Maria Paola Bonacina; Jieh Hsiang (NACLP, 1990)

On Fairness of Completion-Based Theorem Proving Strategies. - Maria Paola Bonacina; Jieh Hsiang (RTA, 1991)

On Rewrite Programs: Semantics and Relationship with Prolog. - Maria Paola Bonacina; Jieh Hsiang (J. Log. Program., 1992)

Distributed Deduction by Clause-Diffusion: The Aquarius Prover. - Maria Paola Bonacina; Jieh Hsiang (DISCO, 1993)

On Fairness in Distributed Automated Deduction. - Maria Paola Bonacina; Jieh Hsiang (STACS, 1993)

Distributed Theorem Proving by Peers. - Maria Paola Bonacina; William McCune (CADE, 1994)

On the Reconstruction of Proofs in Distributed Theorem Proving with Contraction: A Modified Clause-Diffusion Method. - Maria Paola Bonacina (PASCO, 1994)

Cumulating Search in a Distributed Computing Environment: A Case Study in Parallel Satisfiability. - Hantao Zhang 001; Maria Paola Bonacina (PASCO, 1994)

Parallelization of Deduction Strategies: An Analytical Study. - Maria Paola Bonacina; Jieh Hsiang (J. Autom. Reason., 1994)

On subsumption in distributed derivations. - Maria Paola Bonacina; Jieh Hsiang (J. Autom. Reason., 1994)

The Clause-Diffusion Methodology for Distributed Deduction. - Maria Paola Bonacina; Jieh Hsiang (Fundam. Informaticae, 1995)

Distributed Deduction by Clause-Diffusion: Distributed Contraction and the Aquarius Prover. - Maria Paola Bonacina; Jieh Hsiang (J. Symb. Comput., 1995)

Towards a Foundation of Completion Procedures as Semidecision Procedures. - Maria Paola Bonacina; Jieh Hsiang (Theor. Comput. Sci., 1995)

On Semantic Resolution with Lemmaizing and Contraction. - Maria Paola Bonacina; Jieh Hsiang (PRICAI, 1996)

A Category-Theoretic Treatment of Automated Theorem Proving. - Maria Paola Bonacina; Jieh Hsiang (J. Inf. Sci. Eng., 1996)

On the Reconstruction of Proofs in Distributed Theorem Proving: a Modified Clause-Diffusion Method. - Maria Paola Bonacina (J. Symb. Comput., 1996)

PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems. - Hantao Zhang 001; Maria Paola Bonacina; Jieh Hsiang (J. Symb. Comput., 1996)

The Clause-Diffusion Theorem Prover Peers-mcd (System Description). - Maria Paola Bonacina (CADE, 1997)

Experiments with subdivision of search in distributed theorem proving. - Maria Paola Bonacina (PASCO, 1997)

Analysis of Distributed-Search Contraction-Based Strategies. - Maria Paola Bonacina (JELIA, 1998)

On the Modelling of Search in Theorem Proving - Towards a Theory of Strategy Analysis. - Maria Paola Bonacina; Jieh Hsiang (Inf. Comput., 1998)

On Semantic Resolution with Lemmaizing and Contraction and a Formal Treatment of Caching. - Maria Paola Bonacina; Jieh Hsiang (New Gener. Comput., 1998)

A Taxonomy of Theorem-Proving Strategies. - Maria Paola Bonacina (Artificial Intelligence Today, 1999)

A model and a first analysis of distributed-search contraction-based strategies. - Maria Paola Bonacina (Ann. Math. Artif. Intell., 1999)

A taxonomy of parallel strategies for deduction. - Maria Paola Bonacina (Ann. Math. Artif. Intell., 2000)

Combination of Distributed Search and Multi-search in Peers-mcd.d. - Maria Paola Bonacina (IJCAR, 2001)

Preface: STRATEGIES 2001. - Maria Paola Bonacina; Bernhard Gramlich (STRATEGIES@IJCAR, 2001)

Preface. - Maria Paola Bonacina; Thierry Boy de la Tour (STRATEGIES@IJCAR, 2004)

On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal. - Alessandro Armando; Maria Paola Bonacina; Silvio Ranise; Stephan Schulz 001 (FroCoS, 2005)

Towards a unified model of search in theorem-proving: subgoal-reduction strategies. - Maria Paola Bonacina (J. Symb. Comput., 2005)

Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures. - Maria Paola Bonacina; Silvio Ghilardi; Enrica Nicolini; Silvio Ranise; Daniele Zucchelli (IJCAR, 2006)

Rewrite-Based Satisfiability Procedures for Recursive Data Structures. - Maria Paola Bonacina; Mnacho Echenim (PDPAR/PaUL@FLoC, 2006)

Rewrite-Based Decision Procedures. - Maria Paola Bonacina; Mnacho Echenim (STRATEGIES@IJCAR, 2006)

Automated Reasoning. - Maria Paola Bonacina; Alberto Martelli (Intelligenza Artificiale, 2006)

T-Decision by Decomposition. - Maria Paola Bonacina; Mnacho Echenim (CADE, 2007)

Abstract canonical inference. - Maria Paola Bonacina; Nachum Dershowitz (ACM Trans. Comput. Log., 2007)

Canonical Inference for Implicational Systems. - Maria Paola Bonacina; Nachum Dershowitz (IJCAR, 2008)

On Variable-inactivity and Polynomial tau-Satisfiability Procedures. - Maria Paola Bonacina; Mnacho Echenim (J. Log. Comput., 2008)

On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving. - Maria Paola Bonacina; Christopher Lynch; Leonardo Mendonça de Moura (CADE, 2009)

New results on rewrite-based satisfiability procedures. - Alessandro Armando; Maria Paola Bonacina; Silvio Ranise; Stephan Schulz 001 (ACM Trans. Comput. Log., 2009)

On theorem proving for program checking: historical perspective and recent developments. - Maria Paola Bonacina (PPDP, 2010)

Theory decision by decomposition. - Maria Paola Bonacina; Mnacho Echenim (J. Symb. Comput., 2010)

On Interpolation in Decision Procedures. - Maria Paola Bonacina; Moa Johansson 001 (TABLEAUX, 2011)

On Deciding Satisfiability by Theorem Proving with Speculative Inferences. - Maria Paola Bonacina; Christopher Lynch; Leonardo Mendonça de Moura (J. Autom. Reason., 2011)

Canonical Ground Horn Theories. - Maria Paola Bonacina; Nachum Dershowitz (Programming Logics, 2013)

On Model-Based Reasoning: Recent Trends and Current Developments. - Maria Paola Bonacina (CILC, 2013)

SGGS Theorem Proving: an Exposition. - Maria Paola Bonacina; David A. Plaisted (PAAR@IJCAR, 2014)

Constraint Manipulation in SGGS. - Maria Paola Bonacina; David A. Plaisted (UNIF, 2014)

On First-Order Model-Based Reasoning. - Maria Paola Bonacina; Ulrich Furbach; Viorica Sofronie-Stokkermans (Logic, Rewriting, and Concurrency, 2015)

On Interpolation in Automated Theorem Proving. - Maria Paola Bonacina; Moa Johansson 001 (J. Autom. Reason., 2015)

Interpolation Systems for Ground Proofs in Automated Deduction: a Survey. - Maria Paola Bonacina; Moa Johansson 001 (J. Autom. Reason., 2015)

Semantically-Guided Goal-Sensitive Reasoning: Model Representation. - Maria Paola Bonacina; David A. Plaisted (J. Autom. Reason., 2016)

Automated Reasoning for Explainable Artificial Intelligence. - Maria Paola Bonacina (ARCADE@CADE, 2017)

Satisfiability Modulo Theories and Assignments. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Natarajan Shankar (CADE, 2017)

On Conflict-Driven Reasoning. - Maria Paola Bonacina (AFM@NFM, 2017)

Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness. - Maria Paola Bonacina; David A. Plaisted (J. Autom. Reason., 2017)

Parallel Theorem Proving. - Maria Paola Bonacina (Handbook of Parallel Constraint Reasoning, 2018)

Proofs in conflict-driven theory combination. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Natarajan Shankar (CPP, 2018)

Theory Combination: Beyond Equality Sharing. - Maria Paola Bonacina; Pascal Fontaine; Christophe Ringeissen; Cesare Tinelli (Description Logic, Theory Combination, and All That, 2019)

SGGS Decision Procedures. - Maria Paola Bonacina; Sarah Winkler (IJCAR (1), 2020)

Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Natarajan Shankar (J. Autom. Reason., 2020)

Proof Generation in CDSAT. - Maria Paola Bonacina (PxTP, 2021)

Integrated Deduction (Dagstuhl Seminar 21371). - Maria Paola Bonacina; Philipp Rümmer; Renate A. Schmidt (Dagstuhl Reports, 2021)

On SGGS and Horn Clauses. - Maria Paola Bonacina; Sarah Winkler (PAAR@IJCAR, 2022)

CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Natarajan Shankar (SMT, 2022)

Larry Wos: Visions of Automated Reasoning. - Michael Beeson; Maria Paola Bonacina; Michael Kinyon; Geoff Sutcliffe (J. Autom. Reason., 2022)

Six Decades of Automated Reasoning: Papers in Memory of Larry Wos. - Maria Paola Bonacina (J. Autom. Reason., 2022)

Set of Support, Demodulation, Paramodulation: A Historical Perspective. - Maria Paola Bonacina (J. Autom. Reason., 2022)

Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Natarajan Shankar (J. Autom. Reason., 2022)

QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Christophe Vauthier (CADE, 2023)

Reasoning about Quantifiers in SMT: The QSMA algorithm. - Maria Paola Bonacina (FMCAD, 2023)

The Next Generation of Deduction Systems: From Composition to Compositionality (Dagstuhl Seminar 23471). - Maria Paola Bonacina; Pascal Fontaine; Cláudia Nalon; Claudia Schon; Martin Desharnais (Dagstuhl Reports, 2023)

Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover. - Maria Paola Bonacina; Sarah Winkler (J. Autom. Reason., 2023)

The CDSAT Method for Satisfiability Modulo Theories and Assignment: an Exposition. - Maria Paola Bonacina (CiE, 2025)

The QSMA Algorithm for Quantifiers in SMT. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Christophe Vauthier (J. Autom. Reason., 2025)