Maria Paola Bonacina

86 papers A 11B 5C 2Journal 36Unranked 27
YearRankTypeTitle / Venue / Authors
2025 C conf
The CDSAT Method for Satisfiability Modulo Theories and Assignment: an Exposition.
CiE
Maria Paola Bonacina
2025 J jnl
The QSMA Algorithm for Quantifiers in SMT.
J. Autom. Reason.
Maria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier
2023 A conf
QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment.
CADE
Maria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier
2023 B conf
Reasoning about Quantifiers in SMT: The QSMA algorithm.
FMCAD
Maria Paola Bonacina
2023 J jnl
Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover.
J. Autom. Reason.
Maria Paola Bonacina, Sarah Winkler
2023 J jnl
The Next Generation of Deduction Systems: From Composition to Compositionality (Dagstuhl Seminar 23471).
Dagstuhl Reports
Maria Paola Bonacina, Pascal Fontaine, Cláudia Nalon, Claudia Schon, Martin Desharnais
2022 — conf
CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length.
SMT
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
2022 J jnl
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs.
J. Autom. Reason.
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
2022 J jnl
Larry Wos: Visions of Automated Reasoning.
J. Autom. Reason.
Michael Beeson, Maria Paola Bonacina, Michael Kinyon, Geoff Sutcliffe
2022 — conf
On SGGS and Horn Clauses.
PAAR@IJCAR
Maria Paola Bonacina, Sarah Winkler
2022 J jnl
Set of Support, Demodulation, Paramodulation: A Historical Perspective.
J. Autom. Reason.
Maria Paola Bonacina
2022 J jnl
Six Decades of Automated Reasoning: Papers in Memory of Larry Wos.
J. Autom. Reason.
Maria Paola Bonacina
2021 J jnl
Integrated Deduction (Dagstuhl Seminar 21371).
Dagstuhl Reports
Maria Paola Bonacina, Philipp Rümmer, Renate A. Schmidt
2021 — conf
Proof Generation in CDSAT.
PxTP
Maria Paola Bonacina
2020 J jnl
Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness.
J. Autom. Reason.
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
2020 — conf
SGGS Decision Procedures.
IJCAR (1)
Maria Paola Bonacina, Sarah Winkler
2019 — conf
Theory Combination: Beyond Equality Sharing.
Description Logic, Theory Combination, and All That
Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, Cesare Tinelli
2018 — ch.
Parallel Theorem Proving.
Handbook of Parallel Constraint Reasoning
Maria Paola Bonacina
2018 B conf
Proofs in conflict-driven theory combination.
CPP
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
2017 — conf
Automated Reasoning for Explainable Artificial Intelligence.
ARCADE@CADE
Maria Paola Bonacina
2017 — conf
On Conflict-Driven Reasoning.
AFM@NFM
Maria Paola Bonacina
2017 A conf
Satisfiability Modulo Theories and Assignments.
CADE
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
2017 J jnl
Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness.
J. Autom. Reason.
Maria Paola Bonacina, David A. Plaisted
2016 J jnl
Semantically-Guided Goal-Sensitive Reasoning: Model Representation.
J. Autom. Reason.
Maria Paola Bonacina, David A. Plaisted
2015 J jnl
Interpolation Systems for Ground Proofs in Automated Deduction: a Survey.
J. Autom. Reason.
Maria Paola Bonacina, Moa Johansson
2015 — conf
On First-Order Model-Based Reasoning.
Logic, Rewriting, and Concurrency
Maria Paola Bonacina, Ulrich Furbach, Viorica Sofronie-Stokkermans
2015 J jnl
On First-Order Model-Based Reasoning.
CoRR
Maria Paola Bonacina, Ulrich Furbach, Viorica Sofronie-Stokkermans
2015 J jnl
On Interpolation in Automated Theorem Proving.
J. Autom. Reason.
Maria Paola Bonacina, Moa Johansson
2014 — conf
Constraint Manipulation in SGGS.
UNIF
Maria Paola Bonacina, David A. Plaisted
2014 — conf
SGGS Theorem Proving: an Exposition.
PAAR@IJCAR
Maria Paola Bonacina, David A. Plaisted
2013 A ed.
Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings
CADE
Maria Paola Bonacina
2013 — ed.
Automated Reasoning and Mathematics - Essays in Memory of William W. McCune
Automated Reasoning and Mathematics
Maria Paola Bonacina, Mark E. Stickel
2013 — conf
Canonical Ground Horn Theories.
Programming Logics
Maria Paola Bonacina, Nachum Dershowitz
2013 — conf
On Model-Based Reasoning: Recent Trends and Current Developments.
CILC
Maria Paola Bonacina
2011 J jnl
On Deciding Satisfiability by Theorem Proving with Speculative Inferences.
J. Autom. Reason.
Maria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura
2011 B conf
On Interpolation in Decision Procedures.
TABLEAUX
Maria Paola Bonacina, Moa Johansson
2010 C conf
On theorem proving for program checking: historical perspective and recent developments.
PPDP
Maria Paola Bonacina
2010 J jnl
Theory decision by decomposition.
J. Symb. Comput.
Maria Paola Bonacina, Mnacho Echenim
2009 J jnl
New results on rewrite-based satisfiability procedures.
ACM Trans. Comput. Log.
Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz
2009 A conf
On Deciding Satisfiability by DPLL(G+
CADE
Maria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura
2008 A conf
Canonical Inference for Implicational Systems.
IJCAR
Maria Paola Bonacina, Nachum Dershowitz
2008 J jnl
On Variable-inactivity and Polynomial tau-Satisfiability Procedures.
J. Log. Comput.
Maria Paola Bonacina, Mnacho Echenim
2007 J jnl
Abstract canonical inference.
ACM Trans. Comput. Log.
Maria Paola Bonacina, Nachum Dershowitz
2007 A conf
T-Decision by Decomposition.
CADE
Maria Paola Bonacina, Mnacho Echenim
2006 J jnl
Automated Reasoning.
Intelligenza Artificiale
Maria Paola Bonacina, Alberto Martelli
2006 A conf
Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures.
IJCAR
Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
2006 J jnl
New results on rewrite-based satisfiability procedures
CoRR
Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz
2006 — conf
Rewrite-Based Decision Procedures.
STRATEGIES@IJCAR
Maria Paola Bonacina, Mnacho Echenim
2006 — conf
Rewrite-Based Satisfiability Procedures for Recursive Data Structures.
PDPAR/PaUL@FLoC
Maria Paola Bonacina, Mnacho Echenim
2005 — conf
On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal.
FroCoS
Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz
2005 — ed.
Proceedings of the 5th International Workshop on Strategies in Automated Deduction, STRATEGIES@IJCAR 2004, Cork, Ireland, July 4, 2004
STRATEGIES@IJCAR
Maria Paola Bonacina, Thierry Boy de la Tour
2005 J jnl
Towards a unified model of search in theorem-proving: subgoal-reduction strategies.
J. Symb. Comput.
Maria Paola Bonacina
2004 J jnl
Abstract Canonical Inference
CoRR
Maria Paola Bonacina, Nachum Dershowitz
2004 — conf
Preface.
STRATEGIES@IJCAR
Maria Paola Bonacina, Thierry Boy de la Tour
2001 — ed.
4th International Workshop on Strategies in Automated Deduction, STRATEGIES 2001, in connection with IJCAR 2001, Siena, Italy, June 18, 2001, Selected Papers
STRATEGIES@IJCAR
Maria Paola Bonacina, Bernhard Gramlich
2001 A conf
Combination of Distributed Search and Multi-search in Peers-mcd.d.
IJCAR
Maria Paola Bonacina
2001 — conf
Preface: STRATEGIES 2001.
STRATEGIES@IJCAR
Maria Paola Bonacina, Bernhard Gramlich
2000 J jnl
A taxonomy of parallel strategies for deduction.
Ann. Math. Artif. Intell.
Maria Paola Bonacina
1999 — ch.
A Taxonomy of Theorem-Proving Strategies.
Artificial Intelligence Today
Maria Paola Bonacina
1999 J jnl
A model and a first analysis of distributed-search contraction-based strategies.
Ann. Math. Artif. Intell.
Maria Paola Bonacina
1998 B conf
Analysis of Distributed-Search Contraction-Based Strategies.
JELIA
Maria Paola Bonacina
1998 J jnl
On Semantic Resolution with Lemmaizing and Contraction and a Formal Treatment of Caching.
New Gener. Comput.
Maria Paola Bonacina, Jieh Hsiang
1998 J jnl
On the Modelling of Search in Theorem Proving - Towards a Theory of Strategy Analysis.
Inf. Comput.
Maria Paola Bonacina, Jieh Hsiang
1997 — conf
Experiments with subdivision of search in distributed theorem proving.
PASCO
Maria Paola Bonacina
1997 A conf
The Clause-Diffusion Theorem Prover Peers-mcd (System Description).
CADE
Maria Paola Bonacina
1996 J jnl
A Category-Theoretic Treatment of Automated Theorem Proving.
J. Inf. Sci. Eng.
Maria Paola Bonacina, Jieh Hsiang
1996 B conf
On Semantic Resolution with Lemmaizing and Contraction.
PRICAI
Maria Paola Bonacina, Jieh Hsiang
1996 J jnl
On the Reconstruction of Proofs in Distributed Theorem Proving: a Modified Clause-Diffusion Method.
J. Symb. Comput.
Maria Paola Bonacina
1996 J jnl
PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems.
J. Symb. Comput.
Hantao Zhang, Maria Paola Bonacina, Jieh Hsiang
1995 J jnl
Distributed Deduction by Clause-Diffusion: Distributed Contraction and the Aquarius Prover.
J. Symb. Comput.
Maria Paola Bonacina, Jieh Hsiang
1995 J jnl
The Clause-Diffusion Methodology for Distributed Deduction.
Fundam. Informaticae
Maria Paola Bonacina, Jieh Hsiang
1995 J jnl
Towards a Foundation of Completion Procedures as Semidecision Procedures.
Theor. Comput. Sci.
Maria Paola Bonacina, Jieh Hsiang
1994 — conf
Cumulating Search in a Distributed Computing Environment: A Case Study in Parallel Satisfiability.
PASCO
Hantao Zhang, Maria Paola Bonacina
1994 A conf
Distributed Theorem Proving by Peers.
CADE
Maria Paola Bonacina, William McCune
1994 J jnl
On subsumption in distributed derivations.
J. Autom. Reason.
Maria Paola Bonacina, Jieh Hsiang
1994 — conf
On the Reconstruction of Proofs in Distributed Theorem Proving with Contraction: A Modified Clause-Diffusion Method.
PASCO
Maria Paola Bonacina
1994 J jnl
Parallelization of Deduction Strategies: An Analytical Study.
J. Autom. Reason.
Maria Paola Bonacina, Jieh Hsiang
1993 — conf
Distributed Deduction by Clause-Diffusion: The Aquarius Prover.
DISCO
Maria Paola Bonacina, Jieh Hsiang
1993 A conf
On Fairness in Distributed Automated Deduction.
STACS
Maria Paola Bonacina, Jieh Hsiang
1992 J jnl
On Rewrite Programs: Semantics and Relationship with Prolog.
J. Log. Program.
Maria Paola Bonacina, Jieh Hsiang
1991 — conf
On Fairness of Completion-Based Theorem Proving Strategies.
RTA
Maria Paola Bonacina, Jieh Hsiang
1990 — conf
A System for Distributed Simplification-Based Theorem Proving.
Dagstuhl Seminar on Parallelization in Inference Systems
Maria Paola Bonacina, Jieh Hsiang
1990 — conf
An Application of Automated Equational Reasoning to Many-valued Logic.
CTRS
Siva Anantharaman, Maria Paola Bonacina
1990 — conf
Completion Procedures as Semidecision Procedures.
CTRS
Maria Paola Bonacina, Jieh Hsiang
1990 — conf
Operational and Denotational Semantics of Rewrite Programs.
NACLP
Maria Paola Bonacina, Jieh Hsiang
1989 — conf
KBlab: An Equational Theorem Prover for the Macintosh.
RTA
Maria Paola Bonacina, Giancarlo Sanna