A categorical critical-pair completion algorithm

DOI10.1006/jsco.1999.0262zbMath0933.18002OpenAlexW1966642096MaRDI QIDQ1300576

Karel Stokkermans

Publication date: 8 March 2000

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/4623c0e4320f0a2bb97eaff6339aa11931e4e59a

zbMATH Keywords

Gröbner basisresolutionKnuth-Bendix procedurecritical-pair completion algorithm

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Grammars and rewriting systems (68Q42) General theory of categories and functors (18A99)

Cites Work

• Topoi. The categorial analysis of logic. Rev. ed
• Multi-valued logic and Gröbner bases with applications to modal logic
• The combinatorics of n-categorical pasting
• Equational methods in first order predicate calculus
• Rewrite method for theorem proving in first order theory with equality
• History and basic features of the critical-pair/completion procedure
• Resolution-based theorem proving for many-valued logics
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Complete Sets of Reductions for Some Equational Theories
• The term rewriting approach to automated theorem proving
• The basic algebraic structures in categories of derivations
• Simulating Buchberger's algorithm by Knuth-Bendix completion
• A categorical formulation for critical-pair/completion procedures
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item