default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDMaria Paola Bonacina
Person information
- affiliation: University of Verona, Italy
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
[j30]Maria Paola Bonacina
, Sarah Winkler:
Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover. J. Autom. Reason. 67(1): 6 (2023)- [c43]Maria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier:
QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment. CADE 2023: 78-95 - [c42]Maria Paola Bonacina:
Reasoning about Quantifiers in SMT: The QSMA algorithm. FMCAD 2023: 1 - [i5]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): 130-150 (2023) - 2022
- [j29]Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs. J. Autom. Reason. 66(1): 43-91 (2022) - [j28]Maria Paola Bonacina:
Six Decades of Automated Reasoning: Papers in Memory of Larry Wos. J. Autom. Reason. 66(4): 437-438 (2022) - [j27]Michael Beeson, Maria Paola Bonacina, Michael Kinyon, Geoff Sutcliffe:
Larry Wos: Visions of Automated Reasoning. J. Autom. Reason. 66(4): 439-461 (2022) - [j26]Maria Paola Bonacina:
Set of Support, Demodulation, Paramodulation: A Historical Perspective. J. Autom. Reason. 66(4): 463-497 (2022) - [c41]Maria Paola Bonacina, Sarah Winkler:
On SGGS and Horn Clauses. PAAR@IJCAR 2022 - [c40]Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length. SMT 2022: 18-37 - 2021
- [c39]Maria Paola Bonacina:
Proof Generation in CDSAT. PxTP 2021: 1-4 - [i4]Maria Paola Bonacina, Philipp Rümmer, Renate A. Schmidt:
Integrated Deduction (Dagstuhl Seminar 21371). Dagstuhl Reports 11(8): 35-51 (2021) - 2020
- [j25]Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness. J. Autom. Reason. 64(3): 579-609 (2020) - [c38]Maria Paola Bonacina, Sarah Winkler:
SGGS Decision Procedures. IJCAR (1) 2020: 356-374
2010 – 2019
- 2019
- [c37]Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, Cesare Tinelli:
Theory Combination: Beyond Equality Sharing. Description Logic, Theory Combination, and All That 2019: 57-89 - 2018
- [c36]Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
Proofs in conflict-driven theory combination. CPP 2018: 186-200 - [p2]Maria Paola Bonacina:
Parallel Theorem Proving. Handbook of Parallel Constraint Reasoning 2018: 179-235 - 2017
- [j24]Maria Paola Bonacina, David A. Plaisted:
Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness. J. Autom. Reason. 59(2): 165-218 (2017) - [c35]Maria Paola Bonacina:
Automated Reasoning for Explainable Artificial Intelligence. ARCADE@CADE 2017: 24-28 - [c34]Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
Satisfiability Modulo Theories and Assignments. CADE 2017: 42-59 - [c33]Maria Paola Bonacina:
On Conflict-Driven Reasoning. AFM@NFM 2017: 31-49 - 2016
- [j23]Maria Paola Bonacina, David A. Plaisted:
Semantically-Guided Goal-Sensitive Reasoning: Model Representation. J. Autom. Reason. 56(2): 113-141 (2016) - 2015
- [j22]Maria Paola Bonacina, Moa Johansson:
On Interpolation in Automated Theorem Proving. J. Autom. Reason. 54(1): 69-97 (2015) - [j21]Maria Paola Bonacina, Moa Johansson:
Interpolation Systems for Ground Proofs in Automated Deduction: a Survey. J. Autom. Reason. 54(4): 353-390 (2015) - [c32]Maria Paola Bonacina, Ulrich Furbach, Viorica Sofronie-Stokkermans:
On First-Order Model-Based Reasoning. Logic, Rewriting, and Concurrency 2015: 181-204 - [i3]Maria Paola Bonacina, Ulrich Furbach, Viorica Sofronie-Stokkermans:
On First-Order Model-Based Reasoning. CoRR abs/1502.02535 (2015) - 2014
- [c31]Maria Paola Bonacina, David A. Plaisted:
SGGS Theorem Proving: an Exposition. PAAR@IJCAR 2014: 25-38 - [c30]Maria Paola Bonacina, David A. Plaisted:
Constraint Manipulation in SGGS. UNIF 2014: 47-54 - 2013
- [c29]Maria Paola Bonacina, Nachum Dershowitz:
Canonical Ground Horn Theories. Programming Logics 2013: 35-71 - [c28]Maria Paola Bonacina:
On Model-Based Reasoning: Recent Trends and Current Developments. CILC 2013: 9 - [e4]Maria Paola Bonacina, Mark E. Stickel:
Automated Reasoning and Mathematics - Essays in Memory of William W. McCune. Lecture Notes in Computer Science 7788, Springer 2013, ISBN 978-3-642-36674-1 [contents] - [e3]Maria Paola Bonacina:
Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings. Lecture Notes in Computer Science 7898, Springer 2013, ISBN 978-3-642-38573-5 [contents] - 2011
- [j20]Maria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura:
On Deciding Satisfiability by Theorem Proving with Speculative Inferences. J. Autom. Reason. 47(2): 161-189 (2011) - [c27]Maria Paola Bonacina, Moa Johansson:
On Interpolation in Decision Procedures. TABLEAUX 2011: 1-16 - 2010
- [j19]Maria Paola Bonacina, Mnacho Echenim:
Theory decision by decomposition. J. Symb. Comput. 45(2): 229-260 (2010) - [c26]Maria Paola Bonacina:
On theorem proving for program checking: historical perspective and recent developments. PPDP 2010: 1-12
2000 – 2009
- 2009
- [j18]Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz:
New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1): 4:1-4:51 (2009) - [c25]Maria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura:
On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving. CADE 2009: 35-50 - 2008
- [j17]Maria Paola Bonacina, Mnacho Echenim:
On Variable-inactivity and Polynomial tau-Satisfiability Procedures. J. Log. Comput. 18(1): 77-96 (2008) - [c24]Maria Paola Bonacina, Nachum Dershowitz:
Canonical Inference for Implicational Systems. IJCAR 2008: 380-395 - 2007
- [j16]Maria Paola Bonacina, Nachum Dershowitz:
Abstract canonical inference. ACM Trans. Comput. Log. 8(1): 6 (2007) - [c23]Maria Paola Bonacina, Mnacho Echenim:
T-Decision by Decomposition. CADE 2007: 199-214 - 2006
- [j15]Maria Paola Bonacina, Alberto Martelli:
Automated Reasoning. Intelligenza Artificiale 3(1-2): 14-20 (2006) - [c22]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: 513-527 - [c21]Maria Paola Bonacina, Mnacho Echenim:
Rewrite-Based Decision Procedures. STRATEGIES@IJCAR 2006: 27-45 - [c20]Maria Paola Bonacina, Mnacho Echenim:
Rewrite-Based Satisfiability Procedures for Recursive Data Structures. PDPAR/PaUL@FLoC 2006: 55-70 - [i2]Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz:
New results on rewrite-based satisfiability procedures. CoRR abs/cs/0604054 (2006) - 2005
- [j14]Maria Paola Bonacina:
Towards a unified model of search in theorem-proving: subgoal-reduction strategies. J. Symb. Comput. 39(2): 209-255 (2005) - [c19]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: 65-80 - [e2]Maria Paola Bonacina, Thierry Boy de la Tour:
Proceedings of the 5th International Workshop on Strategies in Automated Deduction, STRATEGIES@IJCAR 2004, Cork, Ireland, July 4, 2004. Electronic Notes in Theoretical Computer Science 125(2), Elsevier 2005 [contents] - 2004
- [c18]Maria Paola Bonacina, Thierry Boy de la Tour:
Preface. STRATEGIES@IJCAR 2004: 1-3 - [i1]Maria Paola Bonacina, Nachum Dershowitz:
Abstract Canonical Inference. CoRR cs.LO/0406030 (2004) - 2001
- [c17]Maria Paola Bonacina:
Combination of Distributed Search and Multi-search in Peers-mcd.d. IJCAR 2001: 448-452 - [c16]Maria Paola Bonacina, Bernhard Gramlich:
Preface: STRATEGIES 2001. STRATEGIES@IJCAR 2001: 217-218 - [e1]Maria Paola Bonacina, Bernhard Gramlich:
4th International Workshop on Strategies in Automated Deduction, STRATEGIES 2001, in connection with IJCAR 2001, Siena, Italy, June 18, 2001, Selected Papers. Electronic Notes in Theoretical Computer Science 58(2), Elsevier 2001 [contents] - 2000
- [j13]Maria Paola Bonacina:
A taxonomy of parallel strategies for deduction. Ann. Math. Artif. Intell. 29(1-4): 223-257 (2000)
1990 – 1999
- 1999
- [j12]Maria Paola Bonacina:
A model and a first analysis of distributed-search contraction-based strategies. Ann. Math. Artif. Intell. 27(1-4): 149-199 (1999) - [p1]Maria Paola Bonacina:
A Taxonomy of Theorem-Proving Strategies. Artificial Intelligence Today 1999: 43-84 - 1998
- [j11]Maria Paola Bonacina, Jieh Hsiang:
On the Modelling of Search in Theorem Proving - Towards a Theory of Strategy Analysis. Inf. Comput. 147(2): 171-208 (1998) - [j10]Maria Paola Bonacina, Jieh Hsiang:
On Semantic Resolution with Lemmaizing and Contraction and a Formal Treatment of Caching. New Gener. Comput. 16(2): 163-200 (1998) - [c15]Maria Paola Bonacina:
Analysis of Distributed-Search Contraction-Based Strategies. JELIA 1998: 107-121 - 1997
- [c14]Maria Paola Bonacina:
The Clause-Diffusion Theorem Prover Peers-mcd (System Description). CADE 1997: 53-56 - [c13]Maria Paola Bonacina:
Experiments with subdivision of search in distributed theorem proving. PASCO 1997: 88-100 - 1996
- [j9]Maria Paola Bonacina, Jieh Hsiang:
A Category-Theoretic Treatment of Automated Theorem Proving. J. Inf. Sci. Eng. 12(1): 101-125 (1996) - [j8]Maria Paola Bonacina:
On the Reconstruction of Proofs in Distributed Theorem Proving: a Modified Clause-Diffusion Method. J. Symb. Comput. 21(4): 507-522 (1996) - [j7]Hantao Zhang, Maria Paola Bonacina, Jieh Hsiang:
PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems. J. Symb. Comput. 21(4): 543-560 (1996) - [c12]Maria Paola Bonacina, Jieh Hsiang:
On Semantic Resolution with Lemmaizing and Contraction. PRICAI 1996: 372-386 - 1995
- [j6]Maria Paola Bonacina, Jieh Hsiang:
The Clause-Diffusion Methodology for Distributed Deduction. Fundam. Informaticae 24(1/2): 177-207 (1995) - [j5]Maria Paola Bonacina, Jieh Hsiang:
Distributed Deduction by Clause-Diffusion: Distributed Contraction and the Aquarius Prover. J. Symb. Comput. 19(1-3): 245-267 (1995) - [j4]Maria Paola Bonacina, Jieh Hsiang:
Towards a Foundation of Completion Procedures as Semidecision Procedures. Theor. Comput. Sci. 146(1&2): 199-242 (1995) - 1994
- [j3]Maria Paola Bonacina, Jieh Hsiang:
On subsumption in distributed derivations. J. Autom. Reason. 12(2): 225-240 (1994) - [j2]Maria Paola Bonacina, Jieh Hsiang:
Parallelization of Deduction Strategies: An Analytical Study. J. Autom. Reason. 13(1): 1-33 (1994) - [c11]Maria Paola Bonacina, William McCune:
Distributed Theorem Proving by Peers. CADE 1994: 841-845 - [c10]Maria Paola Bonacina:
On the Reconstruction of Proofs in Distributed Theorem Proving with Contraction: A Modified Clause-Diffusion Method. PASCO 1994: 22-33 - [c9]Hantao Zhang, Maria Paola Bonacina:
Cumulating Search in a Distributed Computing Environment: A Case Study in Parallel Satisfiability. PASCO 1994: 422-431 - 1993
- [c8]Maria Paola Bonacina, Jieh Hsiang:
Distributed Deduction by Clause-Diffusion: The Aquarius Prover. DISCO 1993: 272-287 - [c7]Maria Paola Bonacina, Jieh Hsiang:
On Fairness in Distributed Automated Deduction. STACS 1993: 141-152 - 1992
- [j1]Maria Paola Bonacina, Jieh Hsiang:
On Rewrite Programs: Semantics and Relationship with Prolog. J. Log. Program. 14(1&2): 155-180 (1992) - 1991
- [c6]Maria Paola Bonacina, Jieh Hsiang:
On Fairness of Completion-Based Theorem Proving Strategies. RTA 1991: 348-360 - 1990
- [c5]Siva Anantharaman, Maria Paola Bonacina:
An Application of Automated Equational Reasoning to Many-valued Logic. CTRS 1990: 156-161 - [c4]Maria Paola Bonacina, Jieh Hsiang:
Completion Procedures as Semidecision Procedures. CTRS 1990: 206-232 - [c3]Maria Paola Bonacina, Jieh Hsiang:
A System for Distributed Simplification-Based Theorem Proving. Dagstuhl Seminar on Parallelization in Inference Systems 1990: 370 - [c2]Maria Paola Bonacina, Jieh Hsiang:
Operational and Denotational Semantics of Rewrite Programs. NACLP 1990: 449-464
1980 – 1989
- 1989
- [c1]Maria Paola Bonacina, Giancarlo Sanna:
KBlab: An Equational Theorem Prover for the Macintosh. RTA 1989: 548-550
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-01-09 12:47 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
