Theorem proving with group presentations: Examples and questions

DOI10.1007/3-540-61511-3_100zbMath1412.68243OpenAlexW1510239582WikidataQ55393310 ScholiaQ55393310MaRDI QIDQ4647534

Ursula Martin Webb

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_100

zbMATH Keywords

symbolic computationword problemquotient groupcomplete systemnormal subgroup

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Generators, relations, and presentations of groups (20F05) Grammars and rewriting systems (68Q42) Word problems, other decision problems, connections with logic and automata (group-theoretic aspects) (20F10)

Related Items

Invariants, patterns and weights for ordering terms

Uses Software

• GAP
• Magma

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• About the descriptive power of certain classes of finite string-rewriting systems
• Computer proofs in group theory
• Termination of rewriting
• Word problems and a homological finiteness condition for monoids
• The Gröbner fan of an ideal
• Some experiments with a completion theorem prover
• The use of Knuth-Bendix methods to solve the word problem in automatic groups
• Efficient computation of zero-dimensional Gröbner bases by change of ordering
• On the problem of generating small convergent systems
• Weights for total division orderings on strings
• Tame combings, almost convexity and rewriting systems for groups
• A complete characterization of termination of \(0^p1^q\to 1^r0^s\)
• Some group theoretic examples with completion theorem provers
• Single axioms for odd exponent groups
• Soluble groups with a finite rewriting system
• The order types of termination orderings on monadic terms, strings and multisets
• Linear interpretations by counting patterns