Maria Paola Bonacina

Affiliations:
  • University of Verona, Italy


According to our database1, Maria Paola Bonacina authored at least 76 papers between 1989 and 2023.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover.
J. Autom. Reason., March, 2023

Reasoning about Quantifiers in SMT: The QSMA algorithm.
Proceedings of the Formal Methods in Computer-Aided Design, 2023

QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment.
Proceedings of the Automated Deduction - CADE 29, 2023

2022
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs.
J. Autom. Reason., 2022

Set of Support, Demodulation, Paramodulation: A Historical Perspective.
J. Autom. Reason., 2022

Six Decades of Automated Reasoning: Papers in Memory of Larry Wos.
J. Autom. Reason., 2022

Larry Wos: Visions of Automated Reasoning.
J. Autom. Reason., 2022

CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length.
Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), 2022

On SGGS and Horn Clauses.
Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11, 2022

2021
Integrated Deduction (Dagstuhl Seminar 21371).
Dagstuhl Reports, 2021

Proof Generation in CDSAT.
Proceedings of the Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, 2021

2020
Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness.
J. Autom. Reason., 2020

SGGS Decision Procedures.
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019
Theory Combination: Beyond Equality Sharing.
Proceedings of the Description Logic, Theory Combination, and All That, 2019

2018
Proofs in conflict-driven theory combination.
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

Parallel Theorem Proving.
Proceedings of the Handbook of Parallel Constraint Reasoning., 2018

2017
Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness.
J. Autom. Reason., 2017

On Conflict-Driven Reasoning.
Proceedings of the Automated Formal Methods, 2017

Satisfiability Modulo Theories and Assignments.
Proceedings of the Automated Deduction - CADE 26, 2017

Automated Reasoning for Explainable Artificial Intelligence.
Proceedings of the ARCADE 2017, 2017

2016
Semantically-Guided Goal-Sensitive Reasoning: Model Representation.
J. Autom. Reason., 2016

2015
Interpolation Systems for Ground Proofs in Automated Deduction: a Survey.
J. Autom. Reason., 2015

On Interpolation in Automated Theorem Proving.
J. Autom. Reason., 2015

On First-Order Model-Based Reasoning.
Proceedings of the Logic, Rewriting, and Concurrency, 2015

2014
Constraint Manipulation in SGGS.
Proceedings of the 28th International Workshop on Unification, 2014

SGGS Theorem Proving: an Exposition.
Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

2013
On Model-Based Reasoning: Recent Trends and Current Developments.
Proceedings of the 28th Italian Conference on Computational Logic, 2013

Canonical Ground Horn Theories.
Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2011
On Deciding Satisfiability by Theorem Proving with Speculative Inferences.
J. Autom. Reason., 2011

On Interpolation in Decision Procedures.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2011

2010
Theory decision by decomposition.
J. Symb. Comput., 2010

On theorem proving for program checking: historical perspective and recent developments.
Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2010

2009
New results on rewrite-based satisfiability procedures.
ACM Trans. Comput. Log., 2009

On Deciding Satisfiability by DPLL(G+<i>T</i>) and Unsound Theorem Proving.
Proceedings of the Automated Deduction, 2009

2008
On Variable-inactivity and Polynomial tau-Satisfiability Procedures.
J. Log. Comput., 2008

Canonical Inference for Implicational Systems.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007
Abstract canonical inference.
ACM Trans. Comput. Log., 2007

T-Decision by Decomposition.
Proceedings of the Automated Deduction, 2007

2006
Automated Reasoning.
Intelligenza Artificiale, 2006

Rewrite-Based Decision Procedures.
Proceedings of the 6th International Workshop on Strategies in Automated Deduction, 2006

Rewrite-Based Satisfiability Procedures for Recursive Data Structures.
Proceedings of the Combined Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006) and the First International Workshop on Probabilistic Automata and Logics (PaUL 2006), 2006

Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

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

On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal.
Proceedings of the Frontiers of Combining Systems, 5th International Workshop, 2005

2004
Preface.
Proceedings of the 5th International Workshop on Strategies in Automated Deduction, 2004

2001
Preface: STRATEGIES 2001.
Proceedings of the 4th International Workshop on Strategies in Automated Deduction, 2001

Combination of Distributed Search and Multi-search in Peers-mcd.d.
Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000
A taxonomy of parallel strategies for deduction.
Ann. Math. Artif. Intell., 2000

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

A Taxonomy of Theorem-Proving Strategies.
Proceedings of the Artificial Intelligence Today: Recent Trends and Developments, 1999

1998
On Semantic Resolution with Lemmaizing and Contraction and a Formal Treatment of Caching.
New Gener. Comput., 1998

On the Modelling of Search in Theorem Proving - Towards a Theory of Strategy Analysis.
Inf. Comput., 1998

Analysis of Distributed-Search Contraction-Based Strategies.
Proceedings of the Logics in Artificial Intelligence, European Workshop, 1998

1997
Experiments with subdivision of search in distributed theorem proving.
Proceedings of the 2nd International Workshop on Parallel Symbolic Computation, 1997

The Clause-Diffusion Theorem Prover Peers-mcd (System Description).
Proceedings of the Automated Deduction, 1997

1996
PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems.
J. Symb. Comput., 1996

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

A Category-Theoretic Treatment of Automated Theorem Proving.
J. Inf. Sci. Eng., 1996

On Semantic Resolution with Lemmaizing and Contraction.
Proceedings of the PRICAI'96: Topics in Artificial Intelligence, 1996

1995
Towards a Foundation of Completion Procedures as Semidecision Procedures.
Theor. Comput. Sci., 1995

Distributed Deduction by Clause-Diffusion: Distributed Contraction and the Aquarius Prover.
J. Symb. Comput., 1995

The Clause-Diffusion Methodology for Distributed Deduction.
Fundam. Informaticae, 1995

1994
On subsumption in distributed derivations.
J. Autom. Reason., 1994

Parallelization of Deduction Strategies: An Analytical Study.
J. Autom. Reason., 1994

Cumulating Search in a Distributed Computing Environment: A Case Study in Parallel Satisfiability.
Proceedings of the First International Symposium on Parallel Symbolic Computation, 1994

On the Reconstruction of Proofs in Distributed Theorem Proving with Contraction: A Modified Clause-Diffusion Method.
Proceedings of the First International Symposium on Parallel Symbolic Computation, 1994

Distributed Theorem Proving by Peers.
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993
On Fairness in Distributed Automated Deduction.
Proceedings of the STACS 93, 1993

Distributed Deduction by Clause-Diffusion: The Aquarius Prover.
Proceedings of the Design and Implementation of Symbolic Computation Systems, 1993

1992
On Rewrite Programs: Semantics and Relationship with Prolog.
J. Log. Program., 1992

1991
On Fairness of Completion-Based Theorem Proving Strategies.
Proceedings of the Rewriting Techniques and Applications, 4th International Conference, 1991

1990
Operational and Denotational Semantics of Rewrite Programs.
Proceedings of the Logic Programming, Proceedings of the 1990 North American Conference, Austin, Texas, USA, October 29, 1990

A System for Distributed Simplification-Based Theorem Proving.
Proceedings of the Parallelization in Inference Systems, 1990

Completion Procedures as Semidecision Procedures.
Proceedings of the Conditional and Typed Rewriting Systems, 1990

An Application of Automated Equational Reasoning to Many-valued Logic.
Proceedings of the Conditional and Typed Rewriting Systems, 1990

1989
KBlab: An Equational Theorem Prover for the Macintosh.
Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989


  Loading...