Prof. Maria Paola Bonacina | |
Universita` degli Studi di Verona Facolta` di Scienze Matematiche Fisiche Naturali Dipartimento di Informatica ProfessorAppointed: 2002 | |
QualificationsPh.D., State University of New York at Stony Brook, Computer Science, 1992. Dottorato di Ricerca, Universita` degli Studi di Milano, Informatica, 1991. Laurea, Universita` degli Studi di Milano, Scienze dell'Informazione, 1986. Expertise and Research InterestsMy research area is automated reasoning. Automated reasoning studies mechanized logics to prove (automated theorem proving) or disprove by counterexample (automated model building) conjectures about systems (e.g., programs, circuits, data structures, communication protocols, mathematical structures). Automated reasoners include fully automated theorem provers, interactive theorem provers or proof assistants, automated model builders, decision procedures, including SAT (SATisfiability in propositional logic) and SMT (Satisfiability Modulo Theories) solvers, model checkers (concerned with the task of checking whether a conjecture is true in a specific model), proof checkers (concerned with the task of checking whether a given proof is correct), as well as knowledge bases of computer-checked mathematics. An overall long-term goal of the field is to build reasoning environments, where all these components are integrated seamlessly. Major applications of automated reasoning include hardware/software verification and program generation.
My focus is on automated theorem proving, that studies how to enable computers to solve problems formulated as logical theorems, and especially fully automated theorem proving, where the proof is generated without assistance from the user. In tha past I experienced mostly with applications of theorem proving to mathematics. Currently, I am mostly interested in the application of theorem proving to design fast decision procedures to be applied in software analysis (e.g., debugging, verification).
Automated reasoning is important for computer science in at least three ways. First, it has direct applications to central problems in computer science, namely the verification that a piece of software or hardware is correct, or at least free of certain bugs, and, dually, the generation of provably correct software or hardware. Second, it is a fundamental study of mechanical forms of logical reasoning. As such, it is part of the general investigation of what we can do with computing machines. Third, it contributes to the foundations of most of computing with symbolic information, including declarative programming, constraint problem solving, computer algebra, deductive databases, planning and learning.
A computer program for theorem proving is called a theorem-proving strategy. Research in this field consists in the theoretical study, design and implementation of theorem-proving strategies. Most mechanical strategies are refutational. A refutational strategy attempts to prove a conjecture by adding its negation to the assumptions, and deriving a contradiction. Proof by refutation is the mechanical counterpart of proof by contradiction. Alternatively, the strategy may try to disprove the conjecture by building a counter-model, where both assumptions and negation of the conjecture are true. Informally, a counter-model is like a counter-example.
Currently, I am working mostly on:
- Design of decision procedures based on superposition and the Davis-Putnam-Logemann-Loveland procedure modulo theories
- Reasoning-based decision procedures for the analysis of infinite state systems
- Instance-based theorem proving
Earlier topics include:
- A proof-ordering based framework for canonical inference and its application to equational theories first and then implicational systems
- Strategy analysis for the machine-independent evaluation of theorem-proving strategies
- Distributed automated deduction
- Combination of forward and backward reasoning
- Mechanical proofs of mathematical theorems
- A target-oriented framework for completion-based theorem proving
- Declarative programming
For a more detailed and more frequently updated presentation, please refer to my personal homepage. Other ExpertiseDirector of the Association for Automated Reasoning (AAR), April 2008 - October 2010
Trustee of the International Conference on Automated Deduction (CADE Inc.), October 2004 - October 2010, elected for two consecutive three-years terms
Dean of the Graduate School of Sciences, Engineering and Medicine (PhD programs), elected, Universita` degli Studi di Verona, October 2006 - December 2009
Member of the Program Committee, International Joint Conference on Automated Reasoning (IJCAR) 2008
Member of the Program Committee, Workshop on Complexity, Expressibility and Decidability in Automated Reasoning (CEDAR) 2008
Member of the Program Committee, Twenty-first International Conference on Automated Deduction (CADE) 2007
Member of the Program Committee, Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) 2007
Member of the Program Committee, Workshop on Automated Deduction: Decidability, Complexity, Tractability (ADDCT) 2007
Director of Computer Science Studies (Undergraduate programs and Master programs), elected, Universita` degli Studi di Verona, October 2003 - September 2006
Workshop Chair and member of the Program Committee, International Joint Conference on Automated Reasoning (IJCAR) 2006
Member of the Program Committee, Sixth International Workshop on Strategies in Automated Deduction, 2006
Editor (with Thierry Boy de la Tour), volume 125, number 2, Electronic Notes in Theoretical Computer Science, ``Fifth International Workshop on Strategies in Automated Deduction: Selected Papers,'' Elsevier, March 2005
Program Co-Chair of the Fifth International Workshop on Strategies in Automated Deduction (STRATEGIES) 2004
Publicity Chair, member of the Program Committee, Coordinator of the Steering Committee and member of the Program Committee for the Doctoral Program, International Joint Conference on Automated Reasoning (IJCAR) 2004
Secretary and ex-officio Trustee, International Conference on Automated Deduction (CADE Inc.), August 1999 - May 2004
Secretary, Association of Automated Reasoning, September 1997 - May 2004
Editor for the Integration/Distributed Area of the QPQ repository for deductive software at http://www.qpq.org/ since April 2003
Member of the Program Committee and President of the Steering Committee of the Fourth International Workshop on First-Order Theorem Proving (FTP) 2003
Member of the Program Committee, Eighteenth International Conference on Automated Deduction (CADE) 2002
Editor (with Bernhard Gramlich), volume 58, number 2, Electronic Notes in Theoretical Computer Science, ``Fourth International Workshop on Strategies in Automated Deduction: Selected Papers,'' Elsevier, October 2001
Member of the Steering Committee, International Joint Conference on Automated Reasoning (IJCAR) 2001
Program Co-Chair, Fourth International Workshop on Strategies in Automated Deduction (STRATEGIES) 2001
Guest editor (with Ulrich Furbach), Special issue of the Journal of Symbolic Computation on ``Advances in First-Order Theorem Proving:'' Volume 29, Number 2, February 2000
Member of the Program Committee and President of the Steering Committee, Third International Workshop on First-Order Theorem Proving (FTP) 2000
Member of the Program Committee and Steering Committee, Second International Workshop on First-Order Theorem Proving (FTP) 1998
Program Co-Chair and member of the Steering Committee, First International Workshop on First-Order Theorem Proving (FTP) 1997
Registration Chair, Tenth International Symposium on Symbolic and Algebraic Computation and Second International Symposium on Parallel Symbolic Computation (Federated ISSAC-PASCO) 1997
Member of the Program Committee, First International Symposium on Parallel Symbolic Computation (PASCO) 1994
Member of the Organizing Committee, Fourth International Conference on Rewriting Techniques and Applications (RTA) 1991
Reviewer for the following journals:
Journal of Symbolic Computation;
Journal on Satisfiability, Boolean Modeling and Computation;
Journal of Automated Reasoning;
Information Processing Letters;
Information and Computation;
IEEE Transactions on Computer-Aided Design;
Theoretical Computer Science;
Journal of Automated Software Engineering;
ACM Transactions on Computational Logic;
Journal of AI Communications;
Annals of Mathematics and Artificial Intelligence;
Reports in Mathematical Logic;
Journal of Logic and Computation;
as well as many international conferences, symposia, workshops and books. Future ResearchThe successes of model checking in hardware and protocol verification suggest to investigate software model checking. However, software model checking is considerably harder, because software involves infinite state systems. Furthermore, hardware analysis is far from being a solved problem. The increasing complexity of hardware designs and the transfer of functionalities from software to hardware blur the boundaries between the analysis of software and that of hardware designs, and their respective requirements.
Complexity is attacked by abstraction: if a piece of software or a hardware design are too complex to be analyzed as they are, an abstract version that is simpler than the original is analyzed instead. However, abstraction conquers complexity at a price: the abstract program (or design) is not equivalent to the original one. Abstraction introduces a hiatus between the analyzed model and the concrete system. An error detected in the abstract model is not necessarily an error in the concrete program or design. In order to bridge the distance between abstract and concrete, model checking needs automated reasoning. The problem of the correspondence between an error in the model and an error in the concrete program is reduced to a satisfiability problem, and decision procedures for satisfiability are used to settle it. Furthermore, the generated proof is used to refine the abstraction, to make the model less abstract, if it turns out that a spurious error was detected.
The complexity of programs and hardware designs is such that reasoning in propositional logic is not sufficient. The satisfiability problems generated by the model checking of such systems require automated reasoning in equational logic, in first-order theories describing data structures or memory models, in linear arithmetic.
I plan to work on offering automated reasoning support to model checking, by defining, designing and implementing decision procedures for combinations of these theories. Such procedures ought to be:
* Efficient, since each decision is only a small part of the analysis task;
* Scalable, because pratical problems generate very large satisfiability problems;
* Capable to generate intelligent answers (e.g., proofs, unsatisfiable cores, interpolants, counter-models), that can be fed back to the model checker to guide its following work;
* Expressive, in order to handle the needed combinations of theories;
* Easy to build, combine and integrate with model checkers into analyzers for programs or hardare designs.
Since no single technique can satisfy all desiderata, this research program will integrate theorem proving, satisfiability modulo theories and model checking, to build decision procedures and embed them in new analyzers. Industrial RelevanceComputer software is everywhere in contemporary society, as computer networks form the main infrastructure for human communication, embedded computers control the operations of all sorts of machines, and we rely on computation for all sort of functionalities and problem solving in industry, services, science, education and administration. It follows that the economic impact of software errors can hardly be overestimated. However, the sheer complexity of software systems notwithstanding, the cost of software errors could be significantly reduced, by techniques that enable earlier and more effective identification and removal of software defects.
A key ingredient to achieve progress in software correctness and software quality is to avoid the all-or-nothing attitude, whereby either we can prove that programs are correct, or else we should accept that software is unavoidably the weak part of our systems. Another key ingredient is to acknowledge that software artifacts are so complex and varied, that no single technique or approach can suffice, but many and diverse ones are needed.
Approaches to software quality assurance are either process-based (i.e., working on the process of software creation to make sure that it is done well) or evidence-based (i.e., giving evidence that software works well). The mainstay of evidence-based techniques is testing, which is necessary, but expensive, and cannot be exhaustive. Complementary to testing are analytic techniques, with static analysis as forerunner. Analytic techniques are either interactive or fully automated. While all these approaches are complementary, the importance of the problem demands to investigate fully automated techniques, that may lead to truly "push-button" tools. KeywordsCOS Keywords:Artificial Intelligence Or Cybernetics, Automation, Computer and Information Sciences, Computer Programming, Distributed System, Logic.Additional Terms:Artificial Intelligence, Automated Deduction, Automated Reasoning, Decision Procedures, Declarative Programming, Program Analysis, Theoretical Computer Science.Languages(Reading, Writing, Speaking)English: (Fluent, Fluent, Fluent) French: (Fluent, Fluent, Fluent) Italian: (Fluent, Fluent, Fluent) MembershipsAssociation for Automated Reasoning IFIP Working Group on Term Rewriting Honors and Awards2002-2002,
Career Development Award,
College of Liberal Arts and Sciences,
The University of Iowa
2000-2002,
Dean Scholar Award,
College of Liberal Arts and Sciences,
The University of Iowa
1996-1996,
Research Assignment,
College of Liberal Arts and Sciences,
The University of Iowa
1993-1993,
Post-doctoral Fellowship "Human Capital and Mobility",
European Union,
INRIA-Lorraine and CRIN, Nancy, France
1991-1993,
Borsa di studio per il perfezionamento all'estero,
Facolta` di Scienze Matematiche Fisiche Naturali,
Universita` degli Studi di Milano, Milano, Italy
Previous Positions1998-2002, Associate Professor,
University of Iowa,
College of Liberal Arts and Sciences,
Computer Science
1993-1993, Postdoctoral Fellow,
INRIA-Lorraine
1993-1993, Visiting Fellow,
Argonne National Laboratory,
Mathematics and Computer Science
1993-1998, Assistant Professor,
University of Iowa,
College of Liberal Arts and Sciences,
Computer Science
Funding Received- National Science Foundation (NSF):
Faculty Early Career Development Award (CAREER): Distributed deduction with contraction and foundation of strategy analysis,
$210,000,
Sep 1, 1997
to Aug 31, 2002.
- National Science Foundation (NSF):
Research Initiation Award: Strategies for contraction-based distributed automated deduction,
$79,407,
Sep 1, 1994
to Aug 31, 1997.
- General Electric Foundation:
General Electric Foundation Faculty Fellowship: Parallel search in distributed automated deduction,
$23,000,
Oct 1, 1993
to Aug 31, 1994.
- Ministero per l'Istruzione, l'Universita` e la Ricerca (Italy):
Programma di Rilevante Interesse Nazionale (PRIN): Synthesis of deduction-based decision procedures with applications to the automatic formal analysis of software (with 3 colleagues),
Euro 121,500,
Nov 20, 2003
to Nov 19, 2005.
- National Science Foundation (NSF):
Research Instrumentation Grant: Experimental Parallel and Distributed Computing Research at the University of Iowa (with 5 colleagues),
$240,000,
Mar 1, 1994
to Aug 31, 1995.
- University of Iowa:
Old Gold Fellowship: Parallel search in distributed automated deduction,
$5,000,
Jul 1, 1994
to Aug 31, 1994.
- National Science Foundation (NSF):
Research Instrumentation Grant: Instrumentation for Research in Search Technology (with 4 colleagues),
$167,920,
Feb 1, 1998
to Jan 31, 2000.
- Ministero per l'Istruzione, l'Universita` e la Ricerca (Italy):
Programma di Rilevante Interesse Nazionale (PRIN): Integrating automated reasoning in model checking: towards push-button formal verification of large-scale and infinite-state systems (with 4 colleagues),
Euro 142,857,
2008
to 2010.
Publications- Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz (2008) New results on rewrite-based satisfiability procedures, ACM Transactions on Computational Logic, 1-49, In Press
- Maria Paola Bonacina, Nachum Dershowitz (2008) Canonical inference for implicational systems In Alessandro Armando, Peter Baumgartner, Gilles Dowek (eds), Proceedings of the Fourth International Joint Conference on Automated Reasoning (IJCAR), Springer, Lecture Notes in Artificial Intelligence 5195, 380-395 pages
- Maria Paola Bonacina, Mnacho Echenim (February 2008) On variable-inactivity and polynomial T-satisfiability procedures, Journal of Logic and Computation, 18 (1), 77-96
- Maria Paola Bonacina, Mnacho Echenim (2007) T-decision by decomposition In Frank Pfenning (eds), Proceedings of the Twenty-first International Conference on Automated Deduction (CADE), Springer, Lecture Notes in Artificial Intelligence 4603, 199-214 pages
- Maria Paola Bonacina, Mnacho Echenim (2007) Decision procedures for variable-inactive theories and two polynomial T-satisfiability procedures (Position paper) In Silvio Ghilardi, Ulrike Sattler, Viorica Sofronie, Ashish Tiwari (eds), Notes of the First Workshop on Automated Deduction: Decidability, Complexity, Tractability (ADDCT), 65-67 pages
- Maria Paola Bonacina, Mnacho Echenim (2007) Rewrite-based decision procedures In Myla Archer, Thierry Boy de la Tour, Cesar Munoz (eds), Proceedings of the Sixth Workshop on Strategies in Automated Deduction (STRATEGIES 2006), Elsevier, Electronic Notes in Theoretical Computer Science, 174(11), 27-45 pages
- Maria Paola Bonacina, Mnacho Echenim (2007) Rewrite-based satisfiability procedures for recursive data structures In Byron Cook, Roberto Sebastiani (eds), Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006), Elsevier, Electronic Notes in Theoretical Computer Science 174(8), 55-70 pages
- Maria Paola Bonacina, Nachum Dershowitz (January 2007) Abstract canonical inference, ACM Transactions on Computational Logic, 8 (1), 180-208
- Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli (2006) Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures In Ulrich Furbach, Natarajan Shankar (eds), Proceedings of the Third International Joint Conference on Automated Reasoning (IJCAR), Springer, Lecture Notes in Artificial Intelligence 4130, 513-527 pages
- Maria Paola Bonacina, Alberto Martelli, Automated reasoning, Intelligenza Artificiale, 3(1-2), 14-20, June 2006
- Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz (2005) On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal In Bernhard Gramlich (eds), Proceedings of the Fifth International Workshop on Frontiers of Combining Systems (FroCoS), Springer, Lecture Notes in Artificial Intelligence 3717, 65-80 pages
- Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz (2005) Big proof engines as little proof engines: new results on rewrite-based satisfiability procedures In Alessandro Armando, Alessandro Cimatti (eds), Notes of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), 33-41 pages
- Stephan Schulz, Maria Paola Bonacina (2005) On handling distinct objects in the superposition calculus In Boris Konev, Stephan Schulz (eds), Notes of the Fifth International Workshop on the Implementation of Logics (IWIL), 66-77 pages
- Maria Paola Bonacina (February 2005) Towards a unified model of search in theorem proving: subgoal-reduction strategies, Journal of Symbolic Computation, 39 (2), 209-255
- Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Michael Rusinowitch, Aditya Kumar Sehgal (2002) High-performance deduction for verification: a case study in the theory of arrays In Serge Autexier, Heiko Mantel (eds), Notes of the Second International Workshop on Verification (VERIFY), 103-112 pages
- Maria Paola Bonacina (2001) Combination of distributed search and multi-search in Peers-mcd.d In Rajeev Gore', Alexander Leitsch, Tobias Nipkow (eds), Proceedings of the First International Joint Conference on Automated Reasoning (IJCAR), Springer, Lecture Notes in Artificial Intelligence 2083, 448-452 pages
- Maria Paola Bonacina (February 2001) A taxonomy of parallel strategies for deduction, Annals of Mathematics and Artificial Intelligence, 29 (1,2,3&4), 223-257
- Maria Paola Bonacina (December 1999) A model and a first analysis of distributed-search contraction-based strategies, Annals of Mathematics and Artificial Intelligence, 27 (1,2,3&4), 149-199
- Maria Paola Bonacina (August 1999) A taxonomy of theorem-proving strategies In Manuela Veloso, Michael Wooldridge (eds), Artificial Intelligence Today - Recent Trends and Developments, Springer, Lecture Notes in Artificial Intelligence, Berlin, Springer, 43-84 pages, ISBN=3-540-66428-9 (bookchapter)
- Maria Paola Bonacina (1999) Ten years of parallel theorem proving: a perspective In Bernhard Gramlich, Helene Kirchner, Frank Pfenning (eds), Notes of the Third International Workshop on Strategies in Automated Deduction (STRATEGIES), 3-15 pages
- Maria Paola Bonacina, Jieh Hsiang (December 1998) On the modelling of search in theorem proving - Towards a theory of strategy analysis, Information and Computation, 147, 171-208
- Maria Paola Bonacina (1998) Theorem proving strategies: a search-oriented taxonomy (Position paper) In Ricardo Caferra, Gernot Salzer (eds), Notes of the Second International Workshop on First-order Theorem Proving (FTP), Technische Universitaet Wien, Technical Report E1852-GS-981, 256-259 pages
- Maria Paola Bonacina (1998) Analysis of distributed-search contraction-based strategies In Juergen Dix, Luis Farinas del Cerro, Ulrich Furbach (eds), Proceedings of the Sixth European Workshop on Logics in Artificial Intelligence (JELIA), Springer, Lecture Notes in Artificial Intelligence 1489, 107-121 pages
- Maria Paola Bonacina (1998) Mechanical proofs of the Levi commutator problem In Peter Baumgartner, Ulrich Furbach, Michael Kohlhase, William W. McCune, Wolfgang Reif, Mark E. Stickel, Tomas Uribe (eds), Notes of the Workshop of Problem Solving Methodologies with Automated Deduction, 1-10 pages
- Maria Paola Bonacina (1998) Strategy analysis: from sequential to parallel strategies (Position paper) In Bernhard Gramlich, Frank Pfenning (eds), Notes of the Second Workshop on Strategies in Automated Deduction (STRATEGIES), 19-21 pages
- Maria Paola Bonacina, Jieh Hsiang (February 1998) On semantic resolution with lemmaizing and contraction and a formal treatment of caching, New Generation Computing, 16 (2), 163-200
- Maria Paola Bonacina (1997) On the representation of parallel search in theorem proving In Maria Paola Bonacina, Ulrich Furbach (eds), Notes of the First International Workshop on First-order Theorem Proving (FTP), Research Institute for Symbolic Computation (RISC), Johannes Kepler Universitaet, Linz, TR 97-50, 22-28 pages
- Maria Paola Bonacina (1997) Experiments with subdivision of search in distributed theorem proving In Markus Hitz, Erich Kaltofen (eds), Proceedings of the Second International Symposium on Parallel Symbolic Computation (PASCO), ACM Press, 88-100 pages
- Maria Paola Bonacina (1997) The Clause-Diffusion theorem prover Peers-mcd In William W. McCune (eds), Proceedings of the Fourteenth International Conference on Automated Deduction (CADE), Springer, Lecture Notes in Artificial Intelligence 1249, 53-56 pages
- Maria Paola Bonacina (1997) Machine-independent evaluation of theorem-proving strategies (Position paper) In Bernhard Gramlich, Helene Kirchner (eds), Notes of the First Workshop on Strategies in Automated Deduction (STRATEGIES), 37-39 pages
- Maria Paola Bonacina, Jieh Hsiang, On the notion of complexity of search in theorem proving, Bulletin of Symbolic Logic, 3(2), 253-254, June 1997
- Maria Paola Bonacina, A note on the analysis of theorem-proving strategies, Newsletter of the Association for Automated Reasoning, 36, 2-8, April 1997
- Hantao Zhang, Maria Paola Bonacina, Jieh Hsiang (December 1996) PSATO: a distributed propositional prover and its application to quasigroup problems, Journal of Symbolic Computation, 21 (4,5&6), 543-560
- Maria Paola Bonacina (December 1996) On the reconstruction of proofs in distributed theorem proving: a modified Clause-Diffusion method, Journal of Symbolic Computation, 21 (4,5&6), 507-522
- Maria Paola Bonacina, Jieh Hsiang (1996) On the representation of dynamic search spaces in theorem proving In Chu-Sing Yang (eds), Proceedings of the International Conference on Artificial Intelligence, International Computer Symposium, National Sun-Yat Sen University, 85-94 pages
- Maria Paola Bonacina, Jieh Hsiang (1996) On semantic resolution with lemmaizing and contraction In Norman Foo, Randy Goebel (eds), Proceedings of the Fourth Pacific Rim International Conference onArtificial Intelligence (PRICAI), Springer, Lecture Notes in Artificial Intelligence 1114, 372-386 pages
- Maria Paola Bonacina (1996) Distributed automated deduction (Position paper) In Deepak Kapur, Donald W. Loveland (eds), NSF Workshop on Future Directions of Automated Deduction
- Maria Paola Bonacina (1996) Strategy analysis for theorem proving (Position paper) In Deepak Kapur, Donald W. Loveland (eds), NSF Workshop on Future Directions of Automated Deduction
- Maria Paola Bonacina, Jieh Hsiang (March 1996) A category-theoretic treatment of automated theorem proving, Journal of Information Science and Engineering, 12 (1), 101-125
- Maria Paola Bonacina, Jieh Hsiang (September 1995) The Clause-Diffusion methodology for distributed deduction, Fundamenta Informaticae, 24, 177-207
- Maria Paola Bonacina, Jieh Hsiang (July 1995) Towards a foundation of completion procedures as semidecision procedures, Theoretical Computer Science, 146, 199-242
- Maria Paola Bonacina, Jieh Hsiang (March 1995) Distributed deduction by Clause-Diffusion: distributed contraction and the Aquarius prover, Journal of Symbolic Computation, 19 (1,2&3), 245-267
- Maria Paola Bonacina (1994) On the reconstruction of proofs in distributed theorem proving with contraction: a modified Clause-Diffusion method In Hoon Hong (eds), Proceedings of the First International Symposium on Parallel Symbolic Computation (PASCO), World Scientific, Lecture Notes Series in Computing 5, 22-33 pages
- Hantao Zhang, Maria Paola Bonacina (1994) Cumulating search in a distributed computing environment: a case study in parallel satisfiability In Hoon Hong (eds), Proceedings of the First International Symposium on Parallel Symbolic Computation (PASCO), World Scientific, Lecture Notes Series in Computing 5, 422-431 pages
- Maria Paola Bonacina, William W. McCune (1994) Distributed theorem proving by Peers In Alan Bundy (eds), Proceedings of the Twelfth International Conference on Automated Deduction (CADE), Springer-Verlag, Lecture Notes in Artificial Intelligence 814, 841-845 pages
- Maria Paola Bonacina, Jieh Hsiang (1994) Parallelization of deduction strategies: an analytical study, Journal of Automated Reasoning, 13, 1-33
- Maria Paola Bonacina, Jieh Hsiang (1994) On subsumption in distributed derivations, Journal of Automated Reasoning, 12, 225-240
- Maria Paola Bonacina, Jieh Hsiang (1993) Distributed deduction by Clause-Diffusion: the Aquarius prover In Alfonso Miola (eds), Proceedings of the Third International Symposium on Design and Implementation of Symbolic Computation Systems (DISCO), Springer-Verlag, Lecture Notes in Computer Science 722, 272-287 pages
- Maria Paola Bonacina, Jieh Hsiang (1993) On fairness in distributed deduction In Patrice Enjalbert, Alain Finkel, Klaus W. Wagner (eds), Proceedings of the Tenth Annual Symposium on Theoretical Aspects of Computer Science (STACS), Springer-Verlag, Lecture Notes in Computer Science 665, 141-152 pages
- Maria Paola Bonacina, Jieh Hsiang (October 1992) On rewrite programs: semantics and relationship with Prolog, Journal of Logic Programming, 14 (1&2), 155-180
- Maria Paola Bonacina, Jieh Hsiang (1992) A system for distributed simplification-based theorem proving In Bertrand Fronhoefer, Graham Wrightson (eds), Parallelization in Inference System, Springer-Verlag, Lecture Notes in Artificial Intelligence 590
- Maria Paola Bonacina, Jieh Hsiang, Incompleteness of the RUE/NRF inference systems, Newsletter of the Association for Automated Reasoning, 20, 9-12, May 1992
- Maria Paola Bonacina, Jieh Hsiang (1992) High performance simplification-based automated deduction, Transactions of the Ninth Army Conference on Applied Mathematics and Computing 1991, Army Research Office Report 92-1, 321-335 pages
- Maria Paola Bonacina, Problems in Lukasiewicz logic, Newsletter of the Association for Automated Reasoning, 18, 5-12, June 1991
- Maria Paola Bonacina, Jieh Hsiang (1991) A category theory approach to completion-based theorem proving strategies (Abstract), International Conference on Category Theory
- Maria Paola Bonacina, Jieh Hsiang (1991) Completion procedures as semidecision procedures In Stephan Kaplan, Mitsuhiro Okada (eds), Proceedings of the Second International Workshop on Conditional and Typed Term Rewriting Systems (CTRS 1990), Springer-Verlag, Lecture Notes in Computer Science 516, 206-232 pages
- Siva Anantharaman, Maria Paola Bonacina (1991) An application of automated equational reasoning to many-valued logic In Stephan Kaplan, Mitsuhiro Okada (eds), Proceedings of the Second International Workshop on Conditional and Typed Term Rewriting Systems (CTRS 1990), Springer-Verlag, Lecture Notes in Computer Science 516, 156-161 pages
- Maria Paola Bonacina, Jieh Hsiang (1991) On fairness of completion-based theorem proving strategies In Ronald V. Book (eds), Proceedings of the Fourth International Conference on Rewriting Techniques and Applications (RTA), Springer-Verlag, Lecture Notes in Computer Science 488, 348-360 pages
- Maria Paola Bonacina, Jieh Hsiang (1990) Operational and denotational semantics of rewrite programs In Saumya Debray, Manuel Hermenegildo (eds), Proceedings of the North American Conference on Logic Programming, MIT Press, Logic Programming Series, 449-464 pages
- Fabio Baj, Maria Paola Bonacina, Massimo Bruschi, Antonella Zanzi, Another term rewriting based proof of the `non-obvious' theorem, Newsletter of the Association for Automated Reasoning, 13, 4-8, September 1989
- Maria Paola Bonacina, Giancarlo Sanna (1989) KBlab: an equational theorem prover for the Macintosh In Nachum Dershowitz (eds), Proceedings of the Third International Conference on Rewriting Techniques and Applications (RTA), Springer-Verlag, Lecture Notes in Computer Science 355, 548-550 pages
- Maria Paola Bonacina, Petri nets for knowledge representation, Petri Nets Newsletter, 27, 28-36, August 1987
- Maria Paola Bonacina, Nachum Dershowitz, Canonical ground Horn theories In Andreas Podelski, Andrei Voronkov, Reinhard Wilhelm (eds), , Essays in Honor of the Memory of Harald Ganzinger, Berlin, Springer, Unpublished (bookchapter)
Profile DetailsIndividual Expertise profile of Maria Paola Bonacina, Copyright Maria Paola Bonacina. © COS Expertise TM, 2008, ProQuest LLC All rights reserved. |