Conditional rewrite rule systems with built-in arithmetic and induction

DOI10.1007/3-540-51081-8_128zbMath1503.68167OpenAlexW2107243865MaRDI QIDQ5055742

Sergey G. Vorobyov

Publication date: 9 December 2022

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-51081-8_128

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items (1)

Could orders be captured by term rewriting systems?

Cites Work

• Proofs by induction in equational theories with constructors
• Refutational theorem proving using term-rewriting systems
• Conditional rewrite rules
• Automatic proofs by induction in theories without constructors
• On the SUP-INF Method for Proving Presburger Formulas
• A Practical Decision Procedure for Arithmetic with Function Symbols
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Conditional rewrite rule systems with built-in arithmetic and induction