Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Publications
Maria Paola Bonacina, Ulrich Furbach, and Viorica Sofronie-Stokkermans. On first-order model-based reasoning.
In Logic, Rewriting, and Concurrency: Essays Dedicated to José Meseguer
and Festschrift Symposium, Urbana Champaign, Illinois, USA, September 2015.
Springer,
Lecture Notes in Computer Science 9200, 181-204, 2015 (invited);
DOI: 10.1007/978-3-319-23165-5_8.
[BibTeX]
Maria Paola Bonacina and David A. Plaisted.
Semantically-guided goal-sensitive theorem proving.
Research Report 92/2014, Dipartimento di Informatica, Università degli Studi di
Verona, 1-58, January 2014 (revised January 2015).
[BibTeX]
2014
Maria Paola Bonacina and David A. Plaisted. Constraint manipulation
in SGGS.
In Notes of the Twenty-Eighth Workshop on Unification (UNIF),
Seventh International Joint Conference on Automated Reasoning (IJCAR) and
Sixth Federated Logic Conference (FLoC), Vienna, Austria, July 2014.
Technical Report 14-06, Research Institute for Symbolic Computation,
Johannes Kepler Universität, Linz, 47-54, 2014.
[BibTeX]
Maria Paola Bonacina and David A. Plaisted. Semantically-guided
goal-sensitive theorem proving (Abstract). Annual Meeting of the IFIP Working Group in Term Rewriting (WG 1.6),
Sixth Federated Logic Conference (FLoC), Vienna, Austria, July 2014.
Maria Paola Bonacina.
Two-stage interpolation systems (Abstract).
In Notes of the First International Workshop on Interpolation:
from Proofs to Applications (IPrA),
Twenty-fifth International Conference on Computer Aided Verification (CAV),
Saint Petersburg, Russia, July 2013.
[BibTeX]
Maria Paola Bonacina (Editor).
Proceedings of the Twenty-Fourth International Conference on Automated
Deduction (CADE-24). Springer,
Lecture Notes in Artificial Intelligence 7898, XVI 466 p. 95 illus., June 2013;
ISBN: 978-3-642-38573-5;
DOI: 10.1007/978-3-642-38574-2.
[BibTeX]
Maria Paola Bonacina and Maribel Fernández (Editors). Notes of the Second Workshop on Strategies in
Rewriting Proving and Programming (IWS). Sixth International Joint Conference on Automated Reasoning (IJCAR),
Manchester, England, UK, June 2012.
Maria Paola Bonacina and Moa Johansson.
Towards interpolation in an SMT solver with integrated superposition.
In Notes of the Ninth International Workshop on Satisfiability Modulo Theories (SMT),
Twenty-Third International Conference on Computer Aided Verification (CAV),
Snowbird, Utah, USA, July 2011.
Technical Report No. UCB/EECS-2011-80,
Department of Electrical Engineering and Computer Sciences,
University of California at Berkeley, 2011.
[BibTeX]
Maria Paola Bonacina and Moa Johansson.
On interpolation in decision procedures.
In Proceedings of the Twentieth International Conference on Automated
Reasoning with Analytic Tableaux and Related Methods (TABLEAUX),
Bern, Switzerland, July 2011.
Springer,
Lecture Notes in Artificial Intelligence, 6793, 1-16, 2011 (invited);
DOI: 10.1007/978-3-642-22119-4_1.
[BibTeX]
Maria Paola Bonacina and Nachum Dershowitz.
Canonical inference for implicational systems.
In Proceedings of the Fourth International Joint Conference on
Automated Reasoning (IJCAR), Sydney, Australia, August 2008.
Springer,
Lecture Notes in Artificial Intelligence 5195, 380-395, 2008.
[BibTeX]
Maria Paola Bonacina and Mnacho Echenim. T-decision
by decomposition.
In Proceedings of the Twenty-first International Conference on
Automated Deduction (CADE), Bremen, Germany, July 2007.
Springer,
Lecture Notes in Artificial Intelligence 4603, 199-214, 2007.
[BibTeX]
Maria Paola Bonacina and Mnacho Echenim.
Decision procedures for variable-inactive theories and
two polynomial T-satisfiability procedures (Position paper).
In Notes of the
First Workshop on Automated Deduction: Decidability, Complexity, Tractability (ADDCT),
Twenty-first International Conference on Automated Deduction (CADE),
65-67, Bremen, Germany, July 2007.
[BibTeX]
Maria Paola Bonacina and Mnacho Echenim.
Rewrite-based decision procedures.
In Proceedings of the Sixth Workshop on Strategies in Automated Deduction (STRATEGIES),
Third International Joint Conference on Automated Reasoning (IJCAR)
and Fourth Federated Logic Conference (FLoC),
Seattle, Washington, USA, August 2006.
Elsevier,
Electronic Notes in Theoretical Computer Science,
174(11):27-45, July 2007;
DOI: 10.1016/j.entcs.2006.11.042.
[BibTeX]
Maria Paola Bonacina and Mnacho Echenim.
Rewrite-based satisfiability procedures for recursive data structures.
In Proceedings of the Fourth Workshop on Pragmatics of
Decision Procedures in Automated Reasoning (PDPAR),
Third International Joint Conference on Automated Reasoning (IJCAR)
and Fourth Federated Logic Conference (FLoC),
Seattle, Washington, USA, August 2006.
Elsevier,
Electronic Notes in Theoretical Computer Science,
174(8):55-70, June 2007.
[BibTeX]
Maria Paola Bonacina and Mnacho Echenim.
Generic theorem proving for decision procedures.
Research Report 41/2006, Dipartimento di Informatica,
Università degli Studi di Verona, August 2006 (revised March 2007), 1-46.
[BibTeX]
Maria Paola Bonacina and Alberto Martelli.
Automated reasoning. Intelligenza Artificiale, 3(1/2):14-20, June 2006.
(Special issue on Artificial Intelligence 50th Anniversary 1956-2006).
[BibTeX]
Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, and Stephan Schulz.
Big proof engines as little proof engines:
new results on rewrite-based satisfiability procedures (Extended abstract).
In Notes of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR),
Seventeenth International Conference on Computer Aided Verification (CAV),
33-41, Edinburgh, Scotland, UK, July 2005.
[BibTeX]
Stephan Schulz and Maria Paola Bonacina.
On handling distinct objects in the superposition calculus.
In Notes of the Fifth International Workshop on the Implementation
of Logics (IWIL), Eleventh International Conference on Logic for Programming,
Artificial Intelligence, and Reasoning (LPAR), 66-77,
Montevideo, Uruguay, March 2005.
[BibTeX]
Maria Paola Bonacina and Thierry Boy de la Tour (Editors). Fifth Workshop on Strategies in Automated Deduction: Selected Papers. Elsevier,
Electronic Notes in Theoretical Computer Science 125(2), March 2005.
Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Michaël Rusinowitch, and
Aditya Kumar Sehgal.
High-performance deduction for verification: a case study in the theory of arrays.
In Notes of the Second International Workshop on Verification (VERIFY),
Third Federated Logic Conference (FLoC), Copenhagen, Denmark, July 2002.
Technical Report 07/2002, DIKU, Copenhagen, 103-112, 2002.
[BibTeX]
2001
Maria Paola Bonacina and Bernhard Gramlich (Editors). Fourth Workshop on Strategies in Automated Deduction: Selected Papers. Elsevier,
Electronic Notes in Theoretical Computer Science 58(2), October 2001.
Maria Paola Bonacina and Ulrich Furbach (Editors). Advances in First-order Theorem Proving.
Academic Press,
Journal of Symbolic Computation
29(2), special issue, February 2000.
Maria Paola Bonacina.
A taxonomy of theorem-proving strategies.
In Manuela Veloso and Michael Wooldridge (Eds.)
Artificial Intelligence Today - Recent Trends and Developments. Springer,
Lecture Notes in Artificial Intelligence 1600, 43-84, August 1999 (invited).
[BibTeX]
Maria Paola Bonacina. Ten years of
parallel theorem proving: a perspective.
In Notes of the Third International Workshop on Strategies
in Automated Deduction, Second Federated Logic Conference (FLoC),
3-15, Trento, Italy, July 1999 (invited).
[BibTeX]
Maria Paola Bonacina.
Theorem proving strategies: a search-oriented taxonomy (Position paper).
In Proceedings of the Second International Workshop on First-order Theorem
Proving (FTP), Schloss Wilhelminenberg, Vienna, Austria, November 1998.
Technical Report E1852-GS-981, Technische Universität Wien, 256-259, 1998.
[BibTeX]
Maria Paola Bonacina.
Mechanical proofs of the Levi commutator problem.
In Notes of the Workshop on Problem Solving Methodologies with Automated Deduction,
Fifteenth International Conference on Automated Deduction (CADE),
1-10, Lindau, Germany, July 1998.
[BibTeX]
Maria Paola Bonacina.
Strategy analysis: from sequential to parallel strategies (Position paper).
In Notes of the Second Workshop on Strategies in Automated Deduction,
Fifteenth International Conference on Automated Deduction (CADE),
19-21, Lindau, Germany, July 1998.
[BibTeX]
Maria Paola Bonacina.
On the representation of parallel search in theorem proving (Extended abstract).
In Notes of the First International Workshop on First-order Theorem
Proving (FTP), Schloss Hagenberg, Linz, Austria, October 1997.
Technical Report 97-50, Research Institute for Symbolic Computation,
Johannes Kepler Universität, Linz, 22-28, 1997.
[BibTeX]
Maria Paola Bonacina and Ulrich Furbach (Editors). Notes of the First International Workshop on
First-order Theorem Proving (FTP).
Schloss Hagenberg, Linz, Austria, October 1997.
Technical Report 97-50, Research Institute for Symbolic Computation,
Johannes Kepler Universität, Linz, 1997.
Maria Paola Bonacina. The Clause-Diffusion
theorem prover Peers-mcd.
In Proceedings of the Fourteenth International Conference on
Automated Deduction (CADE), Townsville, Australia, July 1997.
Springer,
Lecture Notes in Artificial Intelligence 1249, 53-56, 1997.
[BibTeX]
Maria Paola Bonacina.
Machine-independent evaluation of theorem-proving strategies (Position paper).
In Notes of the First Workshop on Strategies in Automated Deduction,
Fourteenth International Conference on Automated Deduction (CADE),
37-39, Townsville, Australia, July 1997.
[BibTeX]
Maria Paola Bonacina and Jieh Hsiang.
On the notion of complexity of search in theorem proving (Abstract). Logic Colloquium 1996, San Sebastiàn, Spain, July 1996.
Bulletin of Symbolic Logic, 3(2):253-254, June 1997.
[BibTeX]
Maria Paola Bonacina and Jieh Hsiang.
On the representation of dynamic search spaces in theorem proving.
In Proceedings of the International Computer Symposium, 85-94,
Kaohshiung, Taiwan, ROC, December 1996.
[BibTeX]
Maria Paola Bonacina and Jieh Hsiang. On semantic resolution
with lemmaizing and contraction.
In Proceedings of the Fourth Pacific Rim International Conference on
Artificial Intelligence (PRICAI), Cairns, Australia, August 1996.
Springer,
Lecture Notes in Artificial Intelligence 1114, 372-386, 1996.
[BibTeX]
Maria Paola Bonacina and William W. McCune. Distributed theorem
proving by Peers.
In Proceedings of the Twelfth International Conference on
Automated Deduction (CADE), Nancy, France, June 1994.
Springer-Verlag,
Lecture Notes in Artificial Intelligence 814, 841-845, 1994.
[BibTeX]
Maria Paola Bonacina and Jieh Hsiang. Distributed deduction
by Clause-Diffusion: the Aquarius prover.
In Proceedings of the Third International Symposium on Design and
Implementation of Symbolic Computation Systems (DISCO), Gmunden, Austria, September 1993.
Springer-Verlag,
Lecture Notes in Computer Science 722, 272-287, 1993.
[BibTeX]
Maria Paola Bonacina and Jieh Hsiang. On fairness in
distributed deduction.
In Proceedings of the Tenth Annual Symposium on Theoretical Aspects of
Computer Science (STACS), Würzburg, Germany, February 1993.
Springer-Verlag,
Lecture Notes in Computer Science 665, 141-152, 1993.
[BibTeX]
1992
Maria Paola Bonacina. Distributed automated deduction.
Ph.D. Thesis, Department of Computer Science, State University of
New York at Stony Brook, December 1992.
[BibTeX]
Maria Paola Bonacina and Jieh Hsiang.
A system for distributed simplification-based theorem proving.
In Bertrand Fronhöfer and Graham Wrightson (Eds.)
Proceedings of the First International Workshop on Parallelization in Inference
Systems, Schloss Dagstuhl, Germany, December 1990.
Springer-Verlag,
Lecture Notes in Artificial Intelligence 590, 370-370, 1992.
[BibTeX]
Maria Paola Bonacina and Jieh Hsiang.
High performance simplification-based automated deduction.
In Transactions of the Ninth US Army Conference on
Applied Mathematics and Computing, Minneapolis, Minnesota, USA, June 1991.
ARO Report 92-1, 321-335, 1992.
[BibTeX]
1991
Maria Paola Bonacina and Jieh Hsiang.
A category theory approach to completion-based theorem proving strategies (Abstract). International Conference on Category Theory 1991,
Montréal, Canada, June 1991.
[BibTeX]
Maria Paola Bonacina and Jieh Hsiang. Completion procedures
as semidecision procedures.
In Proceedings of the Second International Workshop on Conditional and
Typed Term Rewriting Systems (CTRS), Montréal, Canada, June 1990.
Springer-Verlag,
Lecture Notes in Computer Science 516, 206-232, 1991 (invited).
[BibTeX]
Siva Anantharaman and Maria Paola Bonacina.
An application of automated equational reasoning to many-valued logic.
In Proceedings of the Second International Workshop on Conditional and
Typed Term Rewriting Systems (CTRS), Montréal, Canada, June 1990.
Springer-Verlag,
Lecture Notes in Computer Science 516, 156-161, 1991.
[BibTeX]
(This version in the post-workshop proceedings replaced the version presented at the workshop
entitled An application
of the theorem prover SBR3 to many-valued logic.)
1990
Maria Paola Bonacina.
Sulla dimostrazione di teoremi per completamento.
Thesis of Dottorato di Ricerca, Dipartimento di Scienze dell'Informazione,
Università degli Studi di Milano, Milano, Italy, December 1990
(defended in Milano in front of a Departmental committee in January 1991,
and in Rome in front of a national committee in July 1991).
Available in English with title On completion theorem proving,
as Technical Report of the Department of Computer Science, State University of
New York at Stony Brook, December 1990.
[BibTeX]
Maria Paola Bonacina and Jieh Hsiang. Operational and
denotational semantics of rewrite programs.
In Proceedings of the North American Conference on Logic Programming
(previously Symposium on Logic Programming and later renamed
International Symposium on Logic Programming), Austin, Texas, USA, October 1990.
MIT Press, Logic Programming Series, 449-464, 1990.
[BibTeX]
Siva Anantharaman, Nirina Andrianarivelo, Maria Paola Bonacina and Jieh Hsiang.
SBR3: a refutational prover for equational theorems.
Technical Report, Department of Computer Science, State University
of New York at Stony Brook, May 1990, 1-6.
[BibTeX]
1989
Siva Anantharaman and Maria Paola Bonacina. Automated proofs in
Lukasiewicz logic.
Technical Report, Department of Computer Science, State University of New York at Stony Brook,
November 1989 and Rapport de Recherche No. 89-11, LIFO Orléans, 1-14.
[BibTeX]
Fabio Baj, Maria Paola Bonacina, Massimo Bruschi and Antonella Zanzi.
Another term rewriting based proof of the `non-obvious' theorem. Newsletter of the Association for Automated Reasoning, 13:4-8, September 1989.
[BibTeX]
Maria Paola Bonacina and Giancarlo Sanna. KBlab: an equational
theorem prover for the Macintosh.
In Proceedings of the Third International Conference on Rewriting
Techniques and Applications (RTA), Chapel Hill, North Carolina, USA, April 1989.
Springer-Verlag,
Lecture Notes in Computer Science 355, 548-550, 1989.
[BibTeX]
1987
Maria Paola Bonacina.
Petri nets for knowledge representation. Petri Nets Newsletter, 27:28-36, August 1987.
[BibTeX]
1986
Maria Paola Bonacina.
L'algoritmo di Knuth-Bendix.
Thesis of Laurea (undergraduate), Dipartimento di Scienze dell'Informazione,
Università degli Studi di Milano, Milano, Italy, July 1986.