Machine interpretation of line drawings K Sugihara MIT press, 1986 | 430 | 1986 |

Solving polynomial systems using a branch and prune approach P Van Hentenryck, D McAllester, D Kapur SIAM Journal on Numerical Analysis 34 (2), 797-827, 1997 | 376 | 1997 |

Algebraic and geometric reasoning using Dixon resultants D Kapur, T Saxena, L Yang Proceedings of the international symposium on Symbolic and algebraic …, 1994 | 222 | 1994 |

Geometric reasoning D Kapur, JL Mundy Applied Optics 28 (24), 5383, 1989 | 175 | 1989 |

Proof by consistency D Kapur, DR Musser Artificial Intelligence 31 (2), 125-157, 1987 | 174 | 1987 |

NP-completeness of the set unification and matching problems D Kapur, P Narendran International conference on automated deduction, 489-495, 1986 | 167 | 1986 |

A mechanizable induction principle for equational specifications H Zhang, D Kapur, MS Krishnamoorthy International Conference on Automated Deduction, 162-181, 1988 | 166 | 1988 |

Using Gröbner bases to reason about geometry problems D Kapur Journal of Symbolic Computation 2 (4), 399-408, 1986 | 165 | 1986 |

An equational approach to theorem proving in first-order predicate calculus D Kapur, P Narendran ACM SIGSOFT Software Engineering Notes 10 (4), 63-66, 1985 | 159 | 1985 |

An overview of rewrite rule laboratory (RRL) D Kapur, H Zhang Computers & Mathematics with Applications 29 (2), 91-114, 1995 | 154 | 1995 |

On sufficient-completeness and related properties of term rewriting systems D Kapur, P Narendran, H Zhang Acta Informatica 24 (4), 395-415, 1987 | 154 | 1987 |

Generating all polynomial invariants in simple loops E Rodríguez-Carbonell, D Kapur Journal of Symbolic Computation 42 (4), 443-476, 2007 | 148 | 2007 |

Geometry theorem proving using Hilbert's Nullstellensatz D Kapur Proceedings of the fifth ACM symposium on Symbolic and algebraic computation …, 1986 | 126 | 1986 |

Complexity of matching problems D Benanav, D Kapur, P Narendran Journal of symbolic computation 3 (1-2), 203-216, 1987 | 120 | 1987 |

Complexity of unification problems with associative-commutative operators D Kapur, P Narendran Journal of Automated Reasoning 9 (2), 261-288, 1992 | 115 | 1992 |

A Completion Procedure for Computing a Canonical Basis for a *k*-SubalgebraD Kapur, K Madlener Computers and mathematics, 1-11, 1989 | 113 | 1989 |

Automatic generation of polynomial loop invariants: Algebraic foundations E Rodríguez-Carbonell, D Kapur Proceedings of the 2004 international symposium on Symbolic and algebraic …, 2004 | 111 | 2004 |

Automatically generating loop invariants using quantifier elimination D Kapur Dagstuhl Seminar Proceedings, 2006 | 108 | 2006 |

Automatic generation of polynomial invariants of bounded degree using abstract interpretation E Rodríguez-Carbonell, D Kapur Science of Computer Programming 64 (1), 54-75, 2007 | 107 | 2007 |

A finite Thue system with decidable word problem and without equivalent finite canonical system D Kapur, P Narendran Theoretical Computer Science 35, 337-344, 1985 | 105 | 1985 |