Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
140 | Konstantin Korovin, Andrei Voronkov |
Knuth-Bendix constraint solving is NP-complete. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 6(2), pp. 361-388, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
Knuth-Bendix orders, automated deduction, Ordering constraints |
120 | Ian Wehrman, Aaron Stump, Edwin M. Westbrook |
Slothrop: Knuth-Bendix Completion with a Modern Termination Checker. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings, pp. 287-296, 2006, Springer, 3-540-36834-5. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
120 | Paliath Narendran, Jonathan Stillman |
It is Undecidable Whether the Knuth-Bendix Completion Procedure Generates a Crossed Pair. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STACS ![In: STACS 89, 6th Annual Symposium on Theoretical Aspects of Computer Science, Paderborn, FRG, February 16-18, 1989, Proceedings, pp. 348-359, 1989, Springer, 3-540-50840-6. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
|
120 | Mark E. Stickel |
A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984, Proceedings, pp. 248-258, 1984, Springer, 3-540-96022-8. The full citation details ...](Pics/full.jpeg) |
1984 |
DBLP DOI BibTeX RDF |
|
101 | Jieh Hsiang, Michaël Rusinowitch |
On Word Problems in Equational Theories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICALP ![In: Automata, Languages and Programming, 14th International Colloquium, ICALP87, Karlsruhe, Germany, July 13-17, 1987, Proceedings, pp. 54-71, 1987, Springer, 3-540-18088-5. The full citation details ...](Pics/full.jpeg) |
1987 |
DBLP DOI BibTeX RDF |
|
95 | Harald Zankl, Nao Hirokawa, Aart Middeldorp |
KBO Orientability. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 43(2), pp. 173-201, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Knuth-Bendix order, Termination, Term rewriting |
95 | Jean Goubault-Larrecq |
Well-Founded Recursive Relations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings, pp. 484-497, 2001, Springer, 3-540-42554-3. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
well-foundedness, path orderings, Knuth-Bendix orderings, higher-order path orderings, graphs, automata, Termination, calculus |
95 | Michel Ludwig, Uwe Waldmann |
An Extension of the Knuth-Bendix Ordering with LPO-Like Properties. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings, pp. 348-362, 2007, Springer, 978-3-540-75558-6. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
95 | Konstantin Korovin, Andrei Voronkov |
An AC-Compatible Knuth-Bendix Order. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, pp. 47-59, 2003, Springer, 3-540-40559-3. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
95 | Konstantin Korovin, Andrei Voronkov |
The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSTTCS ![In: FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 22nd Conference Kanpur, India, December 12-14, 2002, Proceedings, pp. 230-240, 2002, Springer, 3-540-00225-1. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
95 | Konstantin Korovin, Andrei Voronkov |
Knuth-Bendix Constraint Solving Is NP-Complete. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICALP ![In: Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001, Proceedings, pp. 979-992, 2001, Springer, 3-540-42287-0. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
95 | Konstantin Korovin, Andrei Voronkov |
A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000, pp. 291-302, 2000, IEEE Computer Society, 0-7695-0725-5. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
95 | Franz Winkler 0001 |
Knuth-Bendix Procedure and Buchberger Algorithm: A Synthesis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISSAC ![In: Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC '89, Portland, Oregon, USA, July 17-19, 1989, pp. 55-67, 1989, ACM, 0-89791-325-6. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
|
95 | Ursula Martin |
How to Choose Weights in the Knuth Bendix Ordering. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 2nd International Conference, RTA-87, Bordeaux, France, May 25-27, 1987, Proceedings, pp. 42-53, 1987, Springer, 3-540-17220-3. The full citation details ...](Pics/full.jpeg) |
1987 |
DBLP DOI BibTeX RDF |
|
88 | Christian Sternagel, René Thiemann |
Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, The Netherlands, pp. 287-302, 2013, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-939897-53-8. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
76 | Michaël Rusinowitch |
Rewriting for Deduction and Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 12th International Conference, RTA 2001, Utrecht, The Netherlands, May 22-24, 2001, Proceedings, pp. 2, 2001, Springer, 3-540-42117-3. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
70 | Bernd Löchner |
Things to Know when Implementing KBO. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 36(4), pp. 289-310, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Knuth-Bendix ordering, program transformation |
70 | Heiko Stamer |
Completion Attacks and Weak Keys of Oleshchuk's Public Key Cryptosystem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
INDOCRYPT ![In: Progress in Cryptology - INDOCRYPT 2005, 6th International Conference on Cryptology in India, Bangalore, India, December 10-12, 2005, Proceedings, pp. 209-220, 2005, Springer, 3-540-30805-9. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
completion attack, Knuth-Bendix completion, Cryptanalysis, weak keys, Church-Rosser property, string-rewriting systems |
70 | Deepak Kapur, Paliath Narendran, Hantao Zhang 0001 |
Proof by Induction Using Test Sets. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings, pp. 99-117, 1986, Springer, 3-540-16780-3. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP DOI BibTeX RDF |
Inductionless Induction, Knuth-Bendix Completion Procedure, Consistency, Induction, Equational Theory, Sufficient-Completeness, Proof by Induction |
70 | Abdelilah Kandri-Rody, Deepak Kapur, Paliath Narendran |
An Ideal-Theoretic Approach to Work Problems and Unification Problems over Finitely Presented Commutative Algebras. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, First International Conference, RTA-85, Dijon, France, May 20-22, 1985, Proceedings, pp. 345-364, 1985, Springer, 3-540-15976-2. The full citation details ...](Pics/full.jpeg) |
1985 |
DBLP DOI BibTeX RDF |
Unification Problem, Finitely Presented Algebras, Commutative Algebras, Gröbner Basis, Knuth-Bendix Completion Procedure, Term Rewriting, Word Problem, Polynomial Ideals |
69 | Georg Struth |
Knuth-Bendix Completion as a Data Structure. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RelMiCS ![In: Relational Methods in Computer Science, 8th International Seminar on Relational Methods in Computer Science, 3rd International Workshop on Applications of Kleene Algebra, and Workshop of COST Action 274: TARSKI, St. Catharines, ON, Canada, February 22-26, 2005, Selected Revised Papers, pp. 225-236, 2005, Springer, 3-540-33339-8. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
69 | Ting Zhang 0001, Henny B. Sipma, Zohar Manna |
The Decidability of the First-Order Theory of Knuth-Bendix Order. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, pp. 131-148, 2005, Springer, 3-540-28005-7. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
69 | Konstantin Korovin, Andrei Voronkov |
Orienting Equalities with the Knuth-Bendix Order. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings, pp. 75-, 2003, IEEE Computer Society, 0-7695-1884-2. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
69 | Konstantin Korovin, Andrei Voronkov |
Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 12th International Conference, RTA 2001, Utrecht, The Netherlands, May 22-24, 2001, Proceedings, pp. 137-153, 2001, Springer, 3-540-42117-3. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
69 | Andrea Sattler-Klein |
About Changing the Ordering During Knuth-Bendix Completion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STACS ![In: STACS 94, 11th Annual Symposium on Theoretical Aspects of Computer Science, Caen, France, February 24-26, 1994, Proceedings, pp. 175-186, 1994, Springer, 3-540-57785-8. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
69 | Reinhard Bündgen |
Simulation Buchberger's Algorithm by Knuth-Bendix Completion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, pp. 386-397, 1991, Springer, 3-540-53904-2. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
69 | Joachim Steinbach |
AC-Termination of Rewrite Systems: A Modified Knuth-Bendix Ordering. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ALP ![In: Algebraic and Logic Programming, Second International Conference, Nancy, France, October 1-3, 1990, Proceedings, pp. 372-386, 1990, Springer, 3-540-53162-9. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
69 | Volker Diekert |
On the Knuth-Bendix Completion for Concurrent Processes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICALP ![In: Automata, Languages and Programming, 14th International Colloquium, ICALP87, Karlsruhe, Germany, July 13-17, 1987, Proceedings, pp. 42-53, 1987, Springer, 3-540-18088-5. The full citation details ...](Pics/full.jpeg) |
1987 |
DBLP DOI BibTeX RDF |
|
69 | Miki Hermann, Igor Prívara |
On Nontermination of Knuth-Bendix Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICALP ![In: Automata, Languages and Programming, 13th International Colloquium, ICALP86, Rennes, France, July 15-19, 1986, Proceedings, pp. 146-156, 1986, Springer, 3-540-16761-7. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP DOI BibTeX RDF |
|
69 | David A. Plaisted |
A Simple Non-Termination Test for the Knuth-Bendix Method. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings, pp. 79-88, 1986, Springer, 3-540-16780-3. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP DOI BibTeX RDF |
|
50 | Aytekin Vargun |
Consistency checking for automatic software generation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISCIS ![In: The 24th International Symposium on Computer and Information Sciences, ISCIS 2009, 14-16 September 2009, North Cyprus, pp. 561-566, 2009, IEEE. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
50 | Harald Zankl, Aart Middeldorp |
Satisfying KBO Constraints. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings, pp. 389-403, 2007, Springer, 978-3-540-73447-5. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
50 | Christopher Lynch |
Unsound Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, pp. 473-487, 2004, Springer, 3-540-23024-6. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
50 | Ursula Martin |
Linear Interpretations by Counting Patterns. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 5th International Conference, RTA-93, Montreal, Canada, June 16-18, 1993, Proceedings, pp. 421-433, 1993, Springer, 3-540-56868-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
50 | Jürgen Avenhaus |
Proving Equational and Inductive Theorems by Completion and Embedding Techniques. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, pp. 361-373, 1991, Springer, 3-540-53904-2. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
45 | Dominique Michelucci |
Isometry group, words and proofs of geometric theorems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 2008 ACM Symposium on Applied Computing (SAC), Fortaleza, Ceara, Brazil, March 16-20, 2008, pp. 1821-1825, 2008, ACM, 978-1-59593-753-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Knuth-Bendix, orthogonal symmetries group, rewriting methods, groups, geometry, rewriting, words, isometry, involution |
45 | Guillaume Burel, Claude Kirchner |
Cut Elimination in Deduction Modulo by Abstract Completion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFCS ![In: Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, NY, USA, June 4-7, 2007, Proceedings, pp. 115-131, 2007, Springer, 978-3-540-72732-3. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Knuth-Bendix completion, automated deduction and interactive theorem proving, proof ordering, abstract canonical system, cut elimination, deduction modulo |
45 | Luiz M. R. Gadelha Jr., Mauricio Ayala-Rincón |
An Efficient Strategy for Word-Cycle Completion in Finitely Presented Groups. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SCCC ![In: 21st International Conference of the Chilean Computer Science Society (SCCC 2001), 6-8 November 2001, Punta Arenas, Chile, pp. 80-85, 2001, IEEE Computer Society, 0-7695-1396-4. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
Knuth-Bendix Completion, Word Problem in Finitely Presented Groups, String-Rewriting Systems |
45 | Jean H. Gallier, Paliath Narendran, Stan Raatz, Wayne Snyder |
Theorem Proving Using Equational Matings and Rigid E-Unification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 39(2), pp. 377-429, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
Knuth-Bendix procedure, matings, NP-completeness, unification, automated theorem proving, equational reasoning |
45 | Paul Walton Purdom Jr. |
Detecting Looping Simplifications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 2nd International Conference, RTA-87, Bordeaux, France, May 25-27, 1987, Proceedings, pp. 54-61, 1987, Springer, 3-540-17220-3. The full citation details ...](Pics/full.jpeg) |
1987 |
DBLP DOI BibTeX RDF |
Knuth-Bendix, Matching, Unification, Simplification, Looping, Rewrite rules |
45 | Marc Bergman, Pierre Deransart |
Abstract Data Types and Rewriting Systems: Application to the Programming of Algebraic Abstract Data Types in Prolog. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAAP ![In: CAAP '81, Trees in Algebra and Programming, 6th Colloquium, Genoa, Italy, March 5-7, 1981, Proceedings, pp. 101-116, 1981, Springer, 3-540-10828-9. The full citation details ...](Pics/full.jpeg) |
1981 |
DBLP DOI BibTeX RDF |
proof of equational properties, Knuth-Bendix algorithm, PROLOG, operational semantics, Abstract Data Type, rewriting systems |
45 | Paul Y. Gloess, Jean-Pierre H. Laurent |
Adding Dynamic Paramodulation to Rewrite Algorithms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings, pp. 195-207, 1980, Springer, 3-540-10009-1. The full citation details ...](Pics/full.jpeg) |
1980 |
DBLP DOI BibTeX RDF |
critical pairs, Knuth-Bendix algorithm, paramodulation, rewrite algorithms, theorem-proving, rewrite rules |
44 | Christian Sternagel, René Thiemann |
A Formalization of Knuth-Bendix Orders. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2020, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
44 | Ahmed Bhayat, Giles Reger |
A Knuth-Bendix-Like Ordering for Orienting Combinator Equations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR (1) ![In: Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, pp. 259-277, 2020, Springer, 978-3-030-51073-2. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
44 | Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand |
A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, pp. 432-453, 2017, Springer, 978-3-319-63045-8. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand |
Formalization of Knuth-Bendix Orders for Lambda-Free Higher-Order Terms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2016, 2016. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP BibTeX RDF |
|
44 | Grzegorz Bancerek |
Abstract Reduction Systems and Idea of Knuth-Bendix Completion Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formaliz. Math. ![In: Formaliz. Math. 22(1), pp. 37-56, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
44 | Akihisa Yamada 0002, Keiichirou Kusakari, Toshiki Sakabe |
Unifying the Knuth-Bendix, recursive path and polynomial orders. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: 15th International Symposium on Principles and Practice of Declarative Programming, PPDP '13, Madrid, Spain, September 16-18, 2013, pp. 181-192, 2013, ACM, 978-1-4503-2154-9. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Sarah Winkler, Harald Zankl, Aart Middeldorp |
Ordinals and Knuth-Bendix Orders. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings, pp. 420-434, 2012, Springer, 978-3-642-28716-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Thomas Sternagel, Harald Zankl |
KBCV - Knuth-Bendix Completion Visualizer. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, pp. 530-536, 2012, Springer, 978-3-642-31364-6. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Laura Kovács, Georg Moser, Andrei Voronkov |
On Transfinite Knuth-Bendix Orders. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, pp. 384-399, 2011, Springer, 978-3-642-22437-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
44 | Ruo Ando, Shinsuke Miwa |
Faster Log Analysis and Integration of Security Incidents Using Knuth-Bendix Completion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICONIP (2) ![In: Neural Information Processing - 18th International Conference, ICONIP 2011, Shanghai, China, November 13-17, 2011, Proceedings, Part II, pp. 28-36, 2011, Springer, 978-3-642-24957-0. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
44 | André Luiz Galdino, Mauricio Ayala-Rincón |
A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 45(3), pp. 301-325, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
44 | Guillaume Bonfante, Georg Moser |
Characterising Space Complexity Classes via Knuth-Bendix Orders. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR (Yogyakarta) ![In: Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, pp. 142-156, 2010, Springer, 978-3-642-16241-1. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
44 | Keiichirou Kusakari, Yuki Chiba |
A Higher-Order Knuth-Bendix Procedure and Its Applications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEICE Trans. Inf. Syst. ![In: IEICE Trans. Inf. Syst. 90-D(4), pp. 707-715, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
44 | Aaron Stump, Bernd Löchner |
Knuth-Bendix completion of theories of commuting group endomorphisms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Process. Lett. ![In: Inf. Process. Lett. 98(5), pp. 195-198, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
44 | Georg Moser |
Derivational Complexity of Knuth-Bendix Orders Revisited. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings, pp. 75-89, 2006, Springer, 3-540-48281-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
44 | Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio |
Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 30(1), pp. 99-120, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
44 | Konstantin Korovin, Andrei Voronkov |
Orienting rewrite rules with the Knuth-Bendix order. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Comput. ![In: Inf. Comput. 183(2), pp. 165-186, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
44 | Dieter Hofbauer |
An upper bound on the derivational complexity of Knuth-Bendix orderings. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Comput. ![In: Inf. Comput. 183(1), pp. 43-56, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
44 | Konstantin Korovin, Andrei Voronkov |
Knuth-Bendix constraint solving is NP-complete ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR cs.LO/0207068, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP BibTeX RDF |
|
44 | Ingo Lepper |
Derivation lengths and order types of Knuth-Bendix orders. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 269(1-2), pp. 433-450, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
44 | Georg Struth |
Knuth-Bendix Completion for Non-Symmetric Transitive Relations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RULE@PLI ![In: Second International Workshop on Rule-Based Programming, RULE 2001, Satellite Event of PLI 2001, Firenze, Italy, September 4, 2001, pp. 341-357, 2001, Elsevier. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
44 | David B. A. Epstein, Paul J. Sanders |
Knuth-Bendix For Groups With Infinitely Many Rules. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Algebra Comput. ![In: Int. J. Algebra Comput. 10(5), pp. 539-590, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
44 | Konstantin Korovin, Andrei Voronkov |
The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ARW ![In: Proceedings of the Seventh Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice, King's College London, UK, 20-21 July 2000., 2000, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP BibTeX RDF |
|
44 | Henrik Linnestad |
Fatal Steps of Knuth-Bendix Completion. Nordic Journal of Computing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Nord. J. Comput. ![In: Nord. J. Comput. 3(2), pp. 131-143, 1996. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP BibTeX RDF |
|
44 | Andrea Sattler-Klein |
A systematic study of infinite canonical systems generated by Knuth-Bendix completion and related problems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1996 |
RDF |
|
44 | Andrea Sattler-Klein |
Phänomene der Knuth-Bendix Vervollständigung. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Ausgezeichnete Informatikdissertationen ![In: Ausgezeichnete Informatikdissertationen 1996, pp. 95-113, 1996, Vieweg+Teubner Verlag, 978-3-519-02646-4. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
44 | Muffy Thomas, Phil Watson |
Solving Divergence in Knuth-Bendix Completion by Enriching Signatures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 112(1), pp. 145-185, 1993. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
44 | Charles C. Sims |
The Knuth-Bendix Procedure for Strings as a Substitute for Coset Enumeration. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Symb. Comput. ![In: J. Symb. Comput. 12(4/5), pp. 439-442, 1991. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
44 | David B. A. Epstein, Derek F. Holt, Sarah Rees |
The Use of Knuth-Bendix Methods to Solve the Word Problem in Automatic Groups. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Symb. Comput. ![In: J. Symb. Comput. 12(4/5), pp. 397-414, 1991. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
44 | A. J. J. Dick |
An Introduction to Knuth-Bendix Completion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. J. ![In: Comput. J. 34(1), pp. 2-15, 1991. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
44 | Muffy Thomas, Phil Watson |
Solving Divergence in Knuth-Bendix Completion by Enriching Signatures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AMAST ![In: Algebraic Methodology and Software Technology (AMAST '91), Proceedings of the Second International Conference on Methodology and Software Technology, Iowa City, USA, 22-25 May 1991, pp. 377-390, 1991, Springer, 3-540-19797-4. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP BibTeX RDF |
|
44 | Jeremy Dick, John Kalmus, Ursula Martin |
Automating the Knuth Bendix Ordering. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Acta Informatica ![In: Acta Informatica 28(2), pp. 95-119, 1990. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
44 | Jan Willem Klop |
Term Rewriting Systems: From Church-Rosser to Knuth-Bendix and Beyond. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICALP ![In: Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, UK, July 16-20, 1990, Proceedings, pp. 350-369, 1990, Springer, 3-540-52826-1. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
44 | Akihiko Ohsuga, Kô Sakai |
Complete Equational Unification Based on an Extension of the Knuth-Bendix Completion Procedure. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IWWERT ![In: Word Equations and Related Topics, First International Workshop, IWWERT '90, Tübingen, Germany, October 1-3, 1990, Proceedings, pp. 197-209, 1990, Springer, 3-540-55124-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
44 | Hubert Bertling |
Knuth-Bendix Completion of Horn Clause Programs for Restricted Linear Resolution and Paramodulation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CTRS ![In: Conditional and Typed Rewriting Systems, 2nd International CTRS Workshop, Montreal, Canada, June 11-14, 1990, Proceedings, pp. 181-193, 1990, Springer, 3-540-54317-1. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
44 | Hubert Bertling |
Knuth-Bendix completion of Horn clause programs for restricted linear resolution and paramodulation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1990 |
RDF |
|
44 | Yoshihito Toyama |
Fast Knuth-Bendix Completion with a Term Rewriting System Compiler. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Process. Lett. ![In: Inf. Process. Lett. 32(6), pp. 325-328, 1989. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
|
44 | Volker Diekert |
On the Knuth-Bendix Completion for Concurrent Processes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 66(2), pp. 117-136, 1989. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
|
44 | Alf Smith |
The Knuth-Bendix Completion Algorithm and Its Specification in Z. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Z User Workshop ![In: Proceedings of the Fourth Annual Z User Meeting, Oxford, UK, December 15, 1989, pp. 195-220, 1989, Springer, 978-3-540-19627-3. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
|
44 | Muffy Thomas, Klaus P. Jantke |
Inductive Inference for Solving Divergence in Knuth-Bendix Completion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AII ![In: Analogical and Inductive Inference, International Workshop AII '89, Reinhardsbrunn Castle, GDR, October 1-6, 1989, Proceedings, pp. 288-303, 1989, Springer, 3-540-51734-0. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
|
44 | Steffen Lange |
Towards a Set of Inference Rules for Solving Divergence in Knuth-Bendix Completion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AII ![In: Analogical and Inductive Inference, International Workshop AII '89, Reinhardsbrunn Castle, GDR, October 1-6, 1989, Proceedings, pp. 304-316, 1989, Springer, 3-540-51734-0. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
|
44 | Jim Christian |
Fast Knuth-Bendix Completion: Summary. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 3rd International Conference, RTA-89, Chapel Hill, North Carolina, USA, April 3-5, 1989, Proceedings, pp. 551-555, 1989, Springer, 3-540-51081-8. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
|
44 | Bertram Fronhöfer, Ulrich Furbach |
Transformation systems for program synthesis: Knuth-Bendix completion and fold/unfold ![Search on Bibsonomy](Pics/bibsonomy.png) |
Forschungsberichte, TU Munich ![In: Forschungsberichte, TU Munich FKI 87 88, pp. 1-17, 1988. The full citation details ...](Pics/full.jpeg) |
1988 |
RDF |
|
44 | Deepak Kapur, David R. Musser, Paliath Narendran |
Only Prime Superpositions Need be Considered in the Knuth-Bendix Completion Procedure. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Symb. Comput. ![In: J. Symb. Comput. 6(1), pp. 19-36, 1988. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
|
44 | Klaus P. Jantke |
On Solving Divergence in Knuth-Bendix Completion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ADT ![In: Proceedings of the 6st Workshop on Abstract Data Type, 1988. University of Berlin, Germany, 1988. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP BibTeX RDF |
|
44 | Isabelle Gnaedig |
Knuth-Bendix procedure and non-deterministic behaviour - An example. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Bull. EATCS ![In: Bull. EATCS 32, pp. 86-92, 1987. The full citation details ...](Pics/full.jpeg) |
1987 |
DBLP BibTeX RDF |
|
44 | Jürgen Müller 0007 |
THEOPOGLES - A Theorem Prover Based on First-Order Polynominals and a Special Knuth-Bendix Procedure. ![Search on Bibsonomy](Pics/bibsonomy.png) |
GWAI ![In: GWAI-87, 11th German Workshop on Artificial Intelligence, Geseke, Germany, September 28 - October 2, 1987, Proceedings, pp. 241-250, 1987, Springer, 3-540-18388-4. The full citation details ...](Pics/full.jpeg) |
1987 |
DBLP DOI BibTeX RDF |
|
44 | Pierre Lescanne |
Divergence of the Knuth-Bendix Completion Procedure and Termination Orderings. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Bull. EATCS ![In: Bull. EATCS 30, pp. 80-83, 1986. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP BibTeX RDF |
|
44 | Bertram Fronhöfer, Ulrich Furbach |
Knuth-Bendix Completion versus Fold/Unfold: a Comparative Study in Program Synthesis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
GWAI ![In: GWAI-86 und 2. Österreichische Artificial-Intelligence-Tagung, Ottstein/Niederösterreich, September 22-26, 1986, Proceedings, pp. 289-300, 1986, Springer, 3-540-16808-7. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP DOI BibTeX RDF |
|
44 | Harald Ganzinger |
Knuth-Bendix Completion for Parametric Specifications with Conditional Equations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ADT ![In: Proceedings of the 4st Workshop on Abstract Data Type, 1986. University of Braunschweig, Germany, 1986. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP BibTeX RDF |
|
44 | Leo Bachmair, Nachum Dershowitz |
Critical-pair criteria for the Knuth-Bendix completion procedure. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SYMSAC ![In: Proceedings of the Symposium on Symbolic and Algebraic Manipulation, SYMSAC 1986, Waterloo, Ontario, Canada, July 21-23, 1986, pp. 215-217, 1986, ACM, 0-89791-199-7. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP DOI BibTeX RDF |
|
44 | Deepak Kapur, Paliath Narendran |
The Knuth-Bendix Completion Procedure and Thue Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SIAM J. Comput. ![In: SIAM J. Comput. 14(4), pp. 1052-1072, 1985. The full citation details ...](Pics/full.jpeg) |
1985 |
DBLP DOI BibTeX RDF |
|
44 | Franz Winkler 0001 |
Reducing the Complexity of the Knuth-Bendix Completion-Algorithm: A "Unification" of Different Approaches. ![Search on Bibsonomy](Pics/bibsonomy.png) |
European Conference on Computer Algebra (2) ![In: EUROCAL '85, European Conference on Computer Algebra, Linz, Austria, April 1-3, 1985, Proceedings Volume 2: Research Contributions, pp. 378-389, 1985, Springer, 3-540-15984-3. The full citation details ...](Pics/full.jpeg) |
1985 |
DBLP DOI BibTeX RDF |
|
44 | Yves Métivier |
About the Rewriting Systems Produced by the Knuth-Bendix Completion Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Process. Lett. ![In: Inf. Process. Lett. 16(1), pp. 31-34, 1983. The full citation details ...](Pics/full.jpeg) |
1983 |
DBLP DOI BibTeX RDF |
|
44 | Franz Winkler 0001, Bruno Buchberger |
A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SIGSAM Bull. ![In: SIGSAM Bull. 17(3-4), pp. 20, 1983. The full citation details ...](Pics/full.jpeg) |
1983 |
DBLP DOI BibTeX RDF |
|
44 | Wolfgang Küchlin |
A Theorem-Proving Approach to the Knuth-Bendix Completion Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUROCAM ![In: Computer Algebra, EUROCAM '82, European Computer Algebra Conference, Marseille, France, 5-7 April, 1982, Proceedings, pp. 101-108, 1982, Springer, 3-540-11607-9. The full citation details ...](Pics/full.jpeg) |
1982 |
DBLP DOI BibTeX RDF |
|
44 | Gérard P. Huet |
A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Comput. Syst. Sci. ![In: J. Comput. Syst. Sci. 23(1), pp. 11-21, 1981. The full citation details ...](Pics/full.jpeg) |
1981 |
DBLP DOI BibTeX RDF |
|
25 | Franz Winkler 0001 |
Canonical Reduction Systems in Symbolic Mathematics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAI ![In: Algebraic Informatics, Third International Conference, CAI 2009, Thessaloniki, Greece, May 19-22, 2009, Proceedings, pp. 123-135, 2009, Springer, 978-3-642-03563-0. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|