Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
94 | Dan Benanav, Deepak Kapur, Paliath Narendran |
Complexity of Matching Problems. |
RTA |
1985 |
DBLP DOI BibTeX RDF |
Associative-Commutative, NP-Completeness, Matching, Associative, Commutative |
87 | Patrick Lincoln, Jim Christian |
Adventures in Associative-Commutative Unification (A Summary). |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
87 | François Fages |
Associative-Commutative Unification. |
CADE |
1984 |
DBLP DOI BibTeX RDF |
|
78 | David A. Basin |
Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators in Isomorphism Complete. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
62 | Leo Bachmair, Ashish Tiwari 0001, Laurent Vigneron |
Abstract Congruence Closure. |
J. Autom. Reason. |
2003 |
DBLP DOI BibTeX RDF |
congruence closure, associative-commutative theories, term rewriting |
56 | Catherine Delor, Laurence Puel |
Extension of the Associative Path Ordering to a Chain of Associative Commutative Symbols. |
RTA |
1993 |
DBLP DOI BibTeX RDF |
|
55 | Emmanuel Kounalis, Denis Lugiez, Loic Pottier |
A Solution of the Complement Problem in Associative-Commutative Theories. |
MFCS |
1991 |
DBLP DOI BibTeX RDF |
The Subsumption Lattice of First-Order terms, Associative and Commutative Reasoning, AC-Disunification, Pattern-Matching, Inductive Learning, Sufficient-Completeness |
55 | Paliath Narendran, Michaël Rusinowitch |
Any Gound Associative-Commutative Theory Has a Finite Canonical System. |
RTA |
1991 |
DBLP DOI BibTeX RDF |
|
50 | Evelyne Contejean |
A Certified AC Matching Algorithm. |
RTA |
2004 |
DBLP DOI BibTeX RDF |
|
49 | Leo Bachmair, David A. Plaisted |
Associative Path Orderings. |
RTA |
1985 |
DBLP DOI BibTeX RDF |
|
42 | Joachim Steinbach |
Improving Assoviative Path Orderings. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
39 | Steven Eker |
Associative-Commutative Rewriting on Large Terms. |
RTA |
2003 |
DBLP DOI BibTeX RDF |
|
39 | Pierre-Etienne Moreau, Hélène Kirchner |
A Compiler for Rewrite Programs in Associative-Commutative Theories. |
PLILP/ALP |
1998 |
DBLP DOI BibTeX RDF |
AC theories, AC many-to-one matching, compilation, rewrite systems |
39 | Laurent Vigneron |
Associative-Commutative Deduction with Constraints. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
39 | Leo Bachmair, Ta Chen, I. V. Ramakrishnan |
Associative-Commutative Discrimination Nets. |
TAPSOFT |
1993 |
DBLP DOI BibTeX RDF |
|
39 | Emmanuel Kounalis, Denis Lugiez |
Compilation of Pattern Matching with Associative-Commutative Functions. |
TAPSOFT, Vol.1 |
1991 |
DBLP DOI BibTeX RDF |
|
39 | Isabelle Gnaedig, Pierre Lescanne |
Proving Termination of Associative Commutative Rewriting Systems by Rewriting. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
38 | Ruvim Lipyanski |
Pythagorean Triples in Unification Theory of Nilpotent Rings. |
FCT |
2001 |
DBLP DOI BibTeX RDF |
|
38 | C. Faure |
A Meta Simplifier. |
ISSAC |
1990 |
DBLP DOI BibTeX RDF |
|
31 | Deepak Kapur, G. Sivakumar |
Proving Associative-Communicative Termination Using RPO-Compatible Orderings. |
FTP (LNCS Selection) |
1998 |
DBLP DOI BibTeX RDF |
|
31 | Franz Baader, Klaus U. Schulz |
Combination Techniques and Decision Problems for Disunification. |
RTA |
1993 |
DBLP DOI BibTeX RDF |
|
31 | Ahlem Ben Cherifa, Pierre Lescanne |
An Actual Implementation of a Procedure That Mechanically Proves Termination of Rewriting Systems Based on Inequalities Between Polynomial Interpretations. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
31 | Deepak Kapur, Paliath Narendran |
NP-Completeness of the Set Unification and Matching Problems. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
25 | Katherine A. Yelick |
Combining Unification Algorithms for Confined Regular Equational Theories. |
RTA |
1985 |
DBLP DOI BibTeX RDF |
|
24 | Deepak Kapur |
Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties. |
Log. Methods Comput. Sci. |
2023 |
DBLP DOI BibTeX RDF |
|
24 | Jia Huang, Erkko Lehtonen |
The associative-commutative spectrum of a binary operation. |
Discret. Math. |
2023 |
DBLP DOI BibTeX RDF |
|
24 | Deepak Kapur |
Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
24 | Deepak Kapur |
A Modular Associative Commutative (AC) Congruence Closure Algorithm. |
FSCD |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Manuel Krebber |
Non-linear Associative-Commutative Many-to-One Pattern Matching with Sequence Variables. |
CoRR |
2017 |
DBLP BibTeX RDF |
|
24 | Wenwen Zong, Yong Su, Huawen Liu, Bernard De Baets |
On the Construction of Associative, Commutative and Increasing Operations by Paving. |
AGOP |
2017 |
DBLP DOI BibTeX RDF |
|
24 | Peter Nightingale, Özgür Akgün, Ian P. Gent, Christopher Jefferson, Ian Miguel |
Automatically Improving Constraint Models in Savile Row through Associative-Commutative Common Subexpression Elimination. |
CP |
2014 |
DBLP DOI BibTeX RDF |
|
24 | Sergiu Bursuc, Hubert Comon-Lundh, Stéphanie Delaune |
Associative-Commutative Deducibility Constraints. |
STACS |
2007 |
DBLP DOI BibTeX RDF |
|
24 | Keiichirou Kusakari, Masaki Nakamura 0001, Yoshihito Toyama |
Elimination Transformations for Associative-Commutative Rewriting Systems. |
J. Autom. Reason. |
2006 |
DBLP DOI BibTeX RDF |
(AC-)termination, (AC-)dependency pair, argument filtering, elimination transformation |
24 | Roberto Di Cosmo, François Pottier, Didier Rémy |
Subtyping Recursive Types Modulo Associative Commutative Products. |
TLCA |
2005 |
DBLP DOI BibTeX RDF |
|
24 | David Hemer |
Higher-order associative commutative pattern matching for component retrieval. |
CATS |
2004 |
DBLP DOI BibTeX RDF |
|
24 | Christophe Costa Florêncio |
Rigid grammars in the Associative-Commutative Lambek Calculus are not learnable. |
EACL |
2003 |
DBLP BibTeX RDF |
|
24 | Steven Eker |
Single Elementary Associative-Commutative Matching. |
J. Autom. Reason. |
2002 |
DBLP DOI BibTeX RDF |
|
24 | Christophe Costa Florêncio |
A Note on the Complexity of Associative-Commutative Lambek Calculus. |
TAG+ |
2002 |
DBLP BibTeX RDF |
|
24 | Hélène Kirchner, Pierre-Etienne Moreau |
Promoting rewriting to a programming language: a compiler for non-deterministic rewrite programs in associative-commutative theories. |
J. Funct. Program. |
2001 |
DBLP DOI BibTeX RDF |
|
24 | Claude Marché, Xavier Urbain |
Termination of Associative-Commutative Rewriting by Dependency Pairs. |
RTA |
1998 |
DBLP DOI BibTeX RDF |
|
24 | Narjes Ben Rajeb |
Preuves par induction implicite: cas des théories associatives-commutatives et observationnelles. (Proofs by implicit induction: case of associative-commutative and observational theories). |
|
1997 |
RDF |
|
24 | Paliath Narendran, Michaël Rusinowitch |
Any Ground Associative-Commutative Theory Has a Finite Canonical System. |
J. Autom. Reason. |
1996 |
DBLP DOI BibTeX RDF |
|
24 | Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch |
Automated Verification by Induction with Associative-Commutative Operators. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
24 | Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch |
SPIKE-AC: A System for Proofs by Induction in Associative-Commutative Theories. |
RTA |
1996 |
DBLP DOI BibTeX RDF |
|
24 | Michaël Rusinowitch, Laurent Vigneron |
Automated deduction with associative-commutative operators. |
Appl. Algebra Eng. Commun. Comput. |
1995 |
DBLP DOI BibTeX RDF |
|
24 | Steven M. Eker |
Associative-Commutative Matching Via Bipartite Graph Matching. |
Comput. J. |
1995 |
DBLP DOI BibTeX RDF |
|
24 | Ta Chen, Siva Anantharaman |
STORM: A MAny-to-One Associative-Commutative Matcher. |
RTA |
1995 |
DBLP DOI BibTeX RDF |
|
24 | Leo Bachmair, Ta Chen, I. V. Ramakrishnan, Siva Anantharaman, Jacques Chabin |
Experiments with Associative-Commutative Discrimination Nets. |
IJCAI |
1995 |
DBLP BibTeX RDF |
|
24 | Jean-Luc Moysset |
Décision des problèmes de compléments associatifs-commutatifs. (Decision of associative-commutative complement problems). |
|
1995 |
RDF |
|
24 | Leo Bachmair, Harald Ganzinger |
Associative-Commutative Superposition. |
CTRS |
1994 |
DBLP DOI BibTeX RDF |
|
24 | Leo Bachmair |
Associative-Commutative Reduction Orderings. |
Inf. Process. Lett. |
1992 |
DBLP DOI BibTeX RDF |
|
24 | Deepak Kapur, Paliath Narendran |
Complexity of Unification Problems with Associative-Commutative Operators. |
J. Autom. Reason. |
1992 |
DBLP DOI BibTeX RDF |
|
24 | E. Paul |
A General Refutational Completeness Result for an Inference Procedure Based on Associative-Commutative Unification. |
J. Symb. Comput. |
1992 |
DBLP BibTeX RDF |
|
24 | Nachum Dershowitz, Subrata Mitra |
Path Orderings for Termination of Associative-Commutative Rewriting. |
CTRS |
1992 |
DBLP DOI BibTeX RDF |
|
24 | Emmanuel Kounalis, Denis Lugiez, Loic Pottier |
A Solution of the Complement Problem in Associative-Commutative Theories. |
IWWERT |
1991 |
DBLP DOI BibTeX RDF |
|
24 | Michaël Rusinowitch, Laurent Vigneron |
Automated deduction with associative commutative operators. |
FAIR |
1991 |
DBLP DOI BibTeX RDF |
|
24 | Hantao Zhang 0001, Deepak Kapur |
Unnecessary Inferences in Associative-Commutative Completion Procedures. |
Math. Syst. Theory |
1990 |
DBLP DOI BibTeX RDF |
|
24 | Patrick Lincoln, Jim Christian |
Adventures in Associative-Commutative Unification. |
J. Symb. Comput. |
1989 |
DBLP DOI BibTeX RDF |
|
24 | Ralph W. Wilkerson, Bruce M. McMillin |
Expectations for associative-commutative unification speedups in a multicomputer environment. |
COMPSAC |
1989 |
DBLP DOI BibTeX RDF |
|
24 | Gaétan Hains |
Parallel algorithms for free and associative-commutative unification. |
|
1989 |
RDF |
|
24 | Mark E. Stickel |
A Comparison of the Variable-Abstraction and Constant-Abstraction Methods for Associative-Commutative Unification. |
J. Autom. Reason. |
1987 |
DBLP DOI BibTeX RDF |
|
24 | François Fages |
Associative-Commutative Unification. |
J. Symb. Comput. |
1987 |
DBLP DOI BibTeX RDF |
|
24 | Leo Bachmair, David A. Plaisted |
Termination Orderings for Associative-Commutative Rewriting Systems. |
J. Symb. Comput. |
1985 |
DBLP DOI BibTeX RDF |
|
24 | Nachum Dershowitz, Jieh Hsiang, N. Alan Josephson, David A. Plaisted |
Associative-Commutative Rewriting. |
IJCAI |
1983 |
DBLP BibTeX RDF |
|
24 | Mark E. Stickel |
A Unification Algorithm for Associative-Commutative Functions. |
J. ACM |
1981 |
DBLP DOI BibTeX RDF |
|
24 | Jean-Marie Hullot |
Associative Commutative Pattern Matching. |
IJCAI |
1979 |
DBLP BibTeX RDF |
|
24 | Mark E. Stickel |
A Complete Unification Algorithm for Associative-Commutative Functions. |
IJCAI |
1975 |
DBLP BibTeX RDF |
|
22 | Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch |
Unification Modulo ACUI Plus Distributivity Axioms. |
J. Autom. Reason. |
2004 |
DBLP DOI BibTeX RDF |
equational unification, counter machines, complexity, decidability, rewriting, set constraints, Post correspondence problem |
22 | Deepak Kapur, G. Sivakumar, Hantao Zhang 0001 |
A New Method for Proving Termination of AC-Rewrite Systems. |
FSTTCS |
1990 |
DBLP DOI BibTeX RDF |
|
16 | Denis Lugiez |
Forward Analysis of Dynamic Network of Pushdown Systems Is Easier without Order. |
RP |
2009 |
DBLP DOI BibTeX RDF |
|
16 | Giorgio Delzanno, Roberto Montagna |
Reachability analysis of fragments of mobile ambients in AC term rewriting. |
Formal Aspects Comput. |
2008 |
DBLP DOI BibTeX RDF |
Petri nets, Term rewriting, Reachability, Mobile ambients |
16 | Maria Paola Bonacina, Nachum Dershowitz |
Canonical Inference for Implicational Systems. |
IJCAR |
2008 |
DBLP DOI BibTeX RDF |
|
16 | Cristina Borralleras, Albert Rubio |
Orderings and Constraints: Theory and Practice of Proving Termination. |
Rewriting, Computation and Proof |
2007 |
DBLP DOI BibTeX RDF |
|
16 | Giorgio Delzanno, Roberto Montagna |
Reachability Analysis of Mobile Ambients in Fragments of AC Term Rewriting. |
ICTAC |
2006 |
DBLP DOI BibTeX RDF |
|
16 | Gregory J. Duck, Peter J. Stuckey, Sebastian Brand |
ACD Term Rewriting. |
ICLP |
2006 |
DBLP DOI BibTeX RDF |
|
16 | Martín Abadi, Véronique Cortier |
Deciding Knowledge in Security Protocols under (Many More) Equational Theories. |
CSFW |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Kumar Neeraj Verma, Helmut Seidl, Thomas Schwentick |
On the Complexity of Equational Horn Clauses. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch |
ACID-Unification Is NEXPTIME-Decidable. |
MFCS |
2003 |
DBLP DOI BibTeX RDF |
E-Unification, Dag automata, Complexity, Tree automata, Set constraints |
16 | Phokion G. Kolaitis, Thomas Raffill |
In Search of a Phase Transition in the AC-Matching Problem. |
CP |
2001 |
DBLP DOI BibTeX RDF |
|
16 | Jean-Yves Girard 0001 |
Locus Solum: From the Rules of Logic to the Logic of Rules. |
CSL |
2001 |
DBLP DOI BibTeX RDF |
|
16 | Ashish Tiwari 0001 |
Rewrite Closure for Ground and Cancellative AC Theories. |
FSTTCS |
2001 |
DBLP DOI BibTeX RDF |
|
16 | Deepak Kapur, Mahadevan Subramaniam |
Extending Decision Procedures with Induction Schemes. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
16 | Arnaud Durand 0001, Miki Hermann, Laurent Juban |
On the Complexity of Recognizing the Hilbert Basis of a Linear Diophantine System. |
MFCS |
1999 |
DBLP DOI BibTeX RDF |
|
16 | Roberto Di Cosmo, Stefano Guerrini |
Strong Normalization of Proof Nets Modulo Structural Congruences. |
RTA |
1999 |
DBLP DOI BibTeX RDF |
Linear Logic, Proof Nets, Strong Normalization |
16 | Maria C. F. Ferreira, A. L. Ribeiro |
Context-Sensitive AC-Rewriting. |
RTA |
1999 |
DBLP DOI BibTeX RDF |
|
16 | Julien Zory, Fabien Coelho |
Using Algebraic Transformations to Optimize Expression Evaluation in Scientific Codes. |
IEEE PACT |
1998 |
DBLP DOI BibTeX RDF |
Algebraic transformation, Fused multiply-add operation, Instruction-Level Parallelism, Expression evaluation |
16 | Deepak Kapur, G. Sivakumar |
A Total, Ground path Ordering for Proving Termination of AC-Rewrite Systems. |
RTA |
1997 |
DBLP DOI BibTeX RDF |
|
16 | Konrad Slind |
AC Unification in HOL90. |
HUG |
1993 |
DBLP DOI BibTeX RDF |
|
16 | Georgios Grivas, Roman Maeder |
Matching and Unification for the Object-Oriented Symbolic Computation System AlgBench. |
DISCO |
1993 |
DBLP DOI BibTeX RDF |
|
16 | Hubert Comon |
Complete Axiomatizations of Some Quotient Term Algebras. |
ICALP |
1991 |
DBLP DOI BibTeX RDF |
|
16 | Joachim Steinbach |
AC-Termination of Rewrite Systems: A Modified Knuth-Bendix Ordering. |
ALP |
1990 |
DBLP DOI BibTeX RDF |
|
16 | Ralph W. Wilkerson, Blayne E. Mayfield |
The Role of Term Symmetry in E-Completion Procedures. |
ACM Conference on Computer Science |
1990 |
DBLP DOI BibTeX RDF |
|
16 | Mohamed Adi, Claude Kirchner |
AC-Unification Race: The System Solving Approach And Its Implementation. |
DISCO |
1990 |
DBLP DOI BibTeX RDF |
|
16 | Rakesh M. Verma, I. V. Ramakrishnan |
Some Complexity Theoretic Aspects of AC Rewriting. |
STACS |
1989 |
DBLP DOI BibTeX RDF |
|
16 | Hantao Zhang 0001, Deepak Kapur |
Consider Only General Superpositions in Completion Procedures. |
RTA |
1989 |
DBLP DOI BibTeX RDF |
|
16 | Mark Franzen, Lawrence J. Henschen |
A New Approach to Universal Unification and Its Application to AC-Unification. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
16 | Barbara A. Smith, Ralph W. Wilkerson, Gerald E. Peterson |
Automated Circuit Diagnosis Using First Order Logic Tools. |
IEA/AIE (Vol. 1) |
1988 |
DBLP DOI BibTeX RDF |
|
16 | Leo Bachmair, Nachum Dershowitz |
Commutation, Transformation, and Termination. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|