PSATO: a distributed propositional prover and its application to quasigroup problems H Zhang, MP Bonacina, J Hsiang Journal of Symbolic Computation 21 (4,5&6), 543-560, 1996 | 272 | 1996 |

New results on rewrite-based satisfiability procedures A Armando, MP Bonacina, S Ranise, S Schulz ACM Transactions on Computational Logic (TOCL) 10 (1), 129-179, 2009 | 120 | 2009 |

Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures MP Bonacina, S Ghilardi, E Nicolini, S Ranise, D Zucchelli Proceedings of the Third International Conference on Automated Reasoning …, 2006 | 63 | 2006 |

A taxonomy of parallel strategies for deduction MP Bonacina Annals of Mathematics and Artificial Intelligence 29 (1-4), 223-257, 2000 | 56 | 2000 |

On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal A Armando, MP Bonacina, S Ranise, S Schulz Proceedings of the Fifth International Workshop on Frontiers of Combining …, 2005 | 49 | 2005 |

On deciding satisfiability by theorem proving with speculative inferences MP Bonacina, CA Lynch, L De Moura Journal of Automated Reasoning 47 (2), 161-189, 2011 | 45 | 2011 |

Towards a foundation of completion procedures as semidecision procedures MP Bonacina, J Hsiang Theoretical Computer Science 146 (1-2), 199-242, 1995 | 45 | 1995 |

Abstract canonical inference MP Bonacina, N Dershowitz ACM Transactions on Computational Logic (TOCL) 8 (1), 180-208, 2007 | 42 | 2007 |

Parallelization of deduction strategies: an analytical study MP Bonacina, J Hsiang Journal of Automated Reasoning 13 (1), 1-33, 1994 | 41 | 1994 |

On rewrite programs: semantics and relationship with Prolog MP Bonacina, J Hsiang The Journal of Logic Programming 14 (1&2), 155-180, 1992 | 39 | 1992 |

On Variable-inactivity and Polynomial -Satisfiability Procedures MP Bonacina, M Echenim Journal of Logic and Computation 18 (1), 77-96, 2008 | 38 | 2008 |

Theory decision by decomposition MP Bonacina, M Echenim Journal of Symbolic Computation 45 (2), 229-260, 2010 | 35 | 2010 |

A taxonomy of theorem-proving strategies MP Bonacina Artificial Intelligence Today - Recent Trends and Developments 1600, 43-84, 1999 | 35 | 1999 |

The Clause-Diffusion methodology for distributed deduction MP Bonacina, J Hsiang Fundamenta Informaticae 24 (1), 177-207, 1995 | 33 | 1995 |

Distributed automated deduction MP Bonacina State University of New York at Stony Brook, 1992 | 29 | 1992 |

On Deciding Satisfiability by DPLL (Gamma+T) and Unsound Theorem Proving MP Bonacina, C Lynch, L De Moura Proceedings of the Twenty-Second International Conference on Automated …, 2009 | 25* | 2009 |

Rewrite-based satisfiability procedures for recursive data structures MP Bonacina, M Echenim Electronic Notes in Theoretical Computer Science 174 (8), 55-70, 2007 | 24 | 2007 |

Distributed theorem proving by Peers MP Bonacina, WW McCune Proceedings of the Twelfth International Conference on Automated Deduction …, 1994 | 24 | 1994 |

On the modelling of search in theorem proving—towards a theory of strategy analysis MP Bonacina, J Hsiang Information and Computation 147 (1), 171-208, 1998 | 23 | 1998 |

Distributed deduction by Clause-Diffusion: The Aquarius prover MP Bonacina, J Hsiang Proceedings of the Third International Symposium on Design and …, 1993 | 22 | 1993 |