Maria Paola Bonacina

Publication Activity (10 Years)

Years Active: 1989-2023
Publications (10 Years): 21

Top Topics

Theorem Proving

Automated Reasoning

Decision Procedures

Diagnostic Systems

Top Venues

J. Autom. Reason.

Dagstuhl Reports

Publications

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