Search results for "Knuth-Bendix"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
140	Konstantin Korovin, Andrei Voronkov	Knuth-Bendix constraint solving is NP-complete.	ACM Trans. Comput. Log.	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.	RTA	2006	DBLP DOI BibTeX RDF
120	Paliath Narendran, Jonathan Stillman	It is Undecidable Whether the Knuth-Bendix Completion Procedure Generates a Crossed Pair.	STACS	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.	CADE	1984	DBLP DOI BibTeX RDF
101	Jieh Hsiang, Michaël Rusinowitch	On Word Problems in Equational Theories.	ICALP	1987	DBLP DOI BibTeX RDF
95	Harald Zankl, Nao Hirokawa, Aart Middeldorp	KBO Orientability.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Knuth-Bendix order, Termination, Term rewriting
95	Jean Goubault-Larrecq	Well-Founded Recursive Relations.	CSL	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.	LPAR	2007	DBLP DOI BibTeX RDF
95	Konstantin Korovin, Andrei Voronkov	An AC-Compatible Knuth-Bendix Order.	CADE	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.	FSTTCS	2002	DBLP DOI BibTeX RDF
95	Konstantin Korovin, Andrei Voronkov	Knuth-Bendix Constraint Solving Is NP-Complete.	ICALP	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.	LICS	2000	DBLP DOI BibTeX RDF
95	Franz Winkler 0001	Knuth-Bendix Procedure and Buchberger Algorithm: A Synthesis.	ISSAC	1989	DBLP DOI BibTeX RDF
95	Ursula Martin	How to Choose Weights in the Knuth Bendix Ordering.	RTA	1987	DBLP DOI BibTeX RDF
88	Christian Sternagel, René Thiemann	Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion.	RTA	2013	DBLP DOI BibTeX RDF
76	Michaël Rusinowitch	Rewriting for Deduction and Verification.	RTA	2001	DBLP DOI BibTeX RDF
70	Bernd Löchner	Things to Know when Implementing KBO.	J. Autom. Reason.	2006	DBLP DOI BibTeX RDF	Knuth-Bendix ordering, program transformation
70	Heiko Stamer	Completion Attacks and Weak Keys of Oleshchuk's Public Key Cryptosystem.	INDOCRYPT	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.	CADE	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.	RTA	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.	RelMiCS	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.	CADE	2005	DBLP DOI BibTeX RDF
69	Konstantin Korovin, Andrei Voronkov	Orienting Equalities with the Knuth-Bendix Order.	LICS	2003	DBLP DOI BibTeX RDF
69	Konstantin Korovin, Andrei Voronkov	Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order.	RTA	2001	DBLP DOI BibTeX RDF
69	Andrea Sattler-Klein	About Changing the Ordering During Knuth-Bendix Completion.	STACS	1994	DBLP DOI BibTeX RDF
69	Reinhard Bündgen	Simulation Buchberger's Algorithm by Knuth-Bendix Completion.	RTA	1991	DBLP DOI BibTeX RDF
69	Joachim Steinbach	AC-Termination of Rewrite Systems: A Modified Knuth-Bendix Ordering.	ALP	1990	DBLP DOI BibTeX RDF
69	Volker Diekert	On the Knuth-Bendix Completion for Concurrent Processes.	ICALP	1987	DBLP DOI BibTeX RDF
69	Miki Hermann, Igor Prívara	On Nontermination of Knuth-Bendix Algorithm.	ICALP	1986	DBLP DOI BibTeX RDF
69	David A. Plaisted	A Simple Non-Termination Test for the Knuth-Bendix Method.	CADE	1986	DBLP DOI BibTeX RDF
50	Aytekin Vargun	Consistency checking for automatic software generation.	ISCIS	2009	DBLP DOI BibTeX RDF
50	Harald Zankl, Aart Middeldorp	Satisfying KBO Constraints.	RTA	2007	DBLP DOI BibTeX RDF
50	Christopher Lynch	Unsound Theorem Proving.	CSL	2004	DBLP DOI BibTeX RDF
50	Ursula Martin	Linear Interpretations by Counting Patterns.	RTA	1993	DBLP DOI BibTeX RDF
50	Jürgen Avenhaus	Proving Equational and Inductive Theorems by Completion and Embedding Techniques.	RTA	1991	DBLP DOI BibTeX RDF
45	Dominique Michelucci	Isometry group, words and proofs of geometric theorems.	SAC	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.	LFCS	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.	SCCC	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.	J. ACM	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.	RTA	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.	CAAP	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.	CADE	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.	Arch. Formal Proofs	2020	DBLP BibTeX RDF
44	Ahmed Bhayat, Giles Reger	A Knuth-Bendix-Like Ordering for Orienting Combinator Equations.	IJCAR (1)	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.	CADE	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.	Arch. Formal Proofs	2016	DBLP BibTeX RDF
44	Grzegorz Bancerek	Abstract Reduction Systems and Idea of Knuth-Bendix Completion Algorithm.	Formaliz. Math.	2014	DBLP DOI BibTeX RDF
44	Akihisa Yamada 0002, Keiichirou Kusakari, Toshiki Sakabe	Unifying the Knuth-Bendix, recursive path and polynomial orders.	PPDP	2013	DBLP DOI BibTeX RDF
44	Sarah Winkler, Harald Zankl, Aart Middeldorp	Ordinals and Knuth-Bendix Orders.	LPAR	2012	DBLP DOI BibTeX RDF
44	Thomas Sternagel, Harald Zankl	KBCV - Knuth-Bendix Completion Visualizer.	IJCAR	2012	DBLP DOI BibTeX RDF
44	Laura Kovács, Georg Moser, Andrei Voronkov	On Transfinite Knuth-Bendix Orders.	CADE	2011	DBLP DOI BibTeX RDF
44	Ruo Ando, Shinsuke Miwa	Faster Log Analysis and Integration of Security Incidents Using Knuth-Bendix Completion.	ICONIP (2)	2011	DBLP DOI BibTeX RDF
44	André Luiz Galdino, Mauricio Ayala-Rincón	A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem.	J. Autom. Reason.	2010	DBLP DOI BibTeX RDF
44	Guillaume Bonfante, Georg Moser	Characterising Space Complexity Classes via Knuth-Bendix Orders.	LPAR (Yogyakarta)	2010	DBLP DOI BibTeX RDF
44	Keiichirou Kusakari, Yuki Chiba	A Higher-Order Knuth-Bendix Procedure and Its Applications.	IEICE Trans. Inf. Syst.	2007	DBLP DOI BibTeX RDF
44	Aaron Stump, Bernd Löchner	Knuth-Bendix completion of theories of commuting group endomorphisms.	Inf. Process. Lett.	2006	DBLP DOI BibTeX RDF
44	Georg Moser	Derivational Complexity of Knuth-Bendix Orders Revisited.	LPAR	2006	DBLP DOI BibTeX RDF
44	Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio	Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF
44	Konstantin Korovin, Andrei Voronkov	Orienting rewrite rules with the Knuth-Bendix order.	Inf. Comput.	2003	DBLP DOI BibTeX RDF
44	Dieter Hofbauer	An upper bound on the derivational complexity of Knuth-Bendix orderings.	Inf. Comput.	2003	DBLP DOI BibTeX RDF
44	Konstantin Korovin, Andrei Voronkov	Knuth-Bendix constraint solving is NP-complete	CoRR	2002	DBLP BibTeX RDF
44	Ingo Lepper	Derivation lengths and order types of Knuth-Bendix orders.	Theor. Comput. Sci.	2001	DBLP DOI BibTeX RDF
44	Georg Struth	Knuth-Bendix Completion for Non-Symmetric Transitive Relations.	RULE@PLI	2001	DBLP DOI BibTeX RDF
44	David B. A. Epstein, Paul J. Sanders	Knuth-Bendix For Groups With Infinitely Many Rules.	Int. J. Algebra Comput.	2000	DBLP DOI BibTeX RDF
44	Konstantin Korovin, Andrei Voronkov	The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable.	ARW	2000	DBLP BibTeX RDF
44	Henrik Linnestad	Fatal Steps of Knuth-Bendix Completion. Nordic Journal of Computing.	Nord. J. Comput.	1996	DBLP BibTeX RDF
44	Andrea Sattler-Klein	A systematic study of infinite canonical systems generated by Knuth-Bendix completion and related problems.		1996	RDF
44	Andrea Sattler-Klein	Phänomene der Knuth-Bendix Vervollständigung.	Ausgezeichnete Informatikdissertationen	1996	DBLP DOI BibTeX RDF
44	Muffy Thomas, Phil Watson	Solving Divergence in Knuth-Bendix Completion by Enriching Signatures.	Theor. Comput. Sci.	1993	DBLP DOI BibTeX RDF
44	Charles C. Sims	The Knuth-Bendix Procedure for Strings as a Substitute for Coset Enumeration.	J. Symb. Comput.	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.	J. Symb. Comput.	1991	DBLP DOI BibTeX RDF
44	A. J. J. Dick	An Introduction to Knuth-Bendix Completion.	Comput. J.	1991	DBLP DOI BibTeX RDF
44	Muffy Thomas, Phil Watson	Solving Divergence in Knuth-Bendix Completion by Enriching Signatures.	AMAST	1991	DBLP BibTeX RDF
44	Jeremy Dick, John Kalmus, Ursula Martin	Automating the Knuth Bendix Ordering.	Acta Informatica	1990	DBLP DOI BibTeX RDF
44	Jan Willem Klop	Term Rewriting Systems: From Church-Rosser to Knuth-Bendix and Beyond.	ICALP	1990	DBLP DOI BibTeX RDF
44	Akihiko Ohsuga, Kô Sakai	Complete Equational Unification Based on an Extension of the Knuth-Bendix Completion Procedure.	IWWERT	1990	DBLP DOI BibTeX RDF
44	Hubert Bertling	Knuth-Bendix Completion of Horn Clause Programs for Restricted Linear Resolution and Paramodulation.	CTRS	1990	DBLP DOI BibTeX RDF
44	Hubert Bertling	Knuth-Bendix completion of Horn clause programs for restricted linear resolution and paramodulation.		1990	RDF
44	Yoshihito Toyama	Fast Knuth-Bendix Completion with a Term Rewriting System Compiler.	Inf. Process. Lett.	1989	DBLP DOI BibTeX RDF
44	Volker Diekert	On the Knuth-Bendix Completion for Concurrent Processes.	Theor. Comput. Sci.	1989	DBLP DOI BibTeX RDF
44	Alf Smith	The Knuth-Bendix Completion Algorithm and Its Specification in Z.	Z User Workshop	1989	DBLP DOI BibTeX RDF
44	Muffy Thomas, Klaus P. Jantke	Inductive Inference for Solving Divergence in Knuth-Bendix Completion.	AII	1989	DBLP DOI BibTeX RDF
44	Steffen Lange	Towards a Set of Inference Rules for Solving Divergence in Knuth-Bendix Completion.	AII	1989	DBLP DOI BibTeX RDF
44	Jim Christian	Fast Knuth-Bendix Completion: Summary.	RTA	1989	DBLP DOI BibTeX RDF
44	Bertram Fronhöfer, Ulrich Furbach	Transformation systems for program synthesis: Knuth-Bendix completion and fold/unfold	Forschungsberichte, TU Munich	1988	RDF
44	Deepak Kapur, David R. Musser, Paliath Narendran	Only Prime Superpositions Need be Considered in the Knuth-Bendix Completion Procedure.	J. Symb. Comput.	1988	DBLP DOI BibTeX RDF
44	Klaus P. Jantke	On Solving Divergence in Knuth-Bendix Completion.	ADT	1988	DBLP BibTeX RDF
44	Isabelle Gnaedig	Knuth-Bendix procedure and non-deterministic behaviour - An example.	Bull. EATCS	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.	GWAI	1987	DBLP DOI BibTeX RDF
44	Pierre Lescanne	Divergence of the Knuth-Bendix Completion Procedure and Termination Orderings.	Bull. EATCS	1986	DBLP BibTeX RDF
44	Bertram Fronhöfer, Ulrich Furbach	Knuth-Bendix Completion versus Fold/Unfold: a Comparative Study in Program Synthesis.	GWAI	1986	DBLP DOI BibTeX RDF
44	Harald Ganzinger	Knuth-Bendix Completion for Parametric Specifications with Conditional Equations.	ADT	1986	DBLP BibTeX RDF
44	Leo Bachmair, Nachum Dershowitz	Critical-pair criteria for the Knuth-Bendix completion procedure.	SYMSAC	1986	DBLP DOI BibTeX RDF
44	Deepak Kapur, Paliath Narendran	The Knuth-Bendix Completion Procedure and Thue Systems.	SIAM J. Comput.	1985	DBLP DOI BibTeX RDF
44	Franz Winkler 0001	Reducing the Complexity of the Knuth-Bendix Completion-Algorithm: A "Unification" of Different Approaches.	European Conference on Computer Algebra (2)	1985	DBLP DOI BibTeX RDF
44	Yves Métivier	About the Rewriting Systems Produced by the Knuth-Bendix Completion Algorithm.	Inf. Process. Lett.	1983	DBLP DOI BibTeX RDF
44	Franz Winkler 0001, Bruno Buchberger	A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm.	SIGSAM Bull.	1983	DBLP DOI BibTeX RDF
44	Wolfgang Küchlin	A Theorem-Proving Approach to the Knuth-Bendix Completion Algorithm.	EUROCAM	1982	DBLP DOI BibTeX RDF
44	Gérard P. Huet	A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm.	J. Comput. Syst. Sci.	1981	DBLP DOI BibTeX RDF
25	Franz Winkler 0001	Canonical Reduction Systems in Symbolic Mathematics.	CAI	2009	DBLP DOI BibTeX RDF