Conditional rewrite rule systems with built-in arithmetic and induction

DOI10.1007/3-540-51081-8_128MaRDI QIDQ5055742zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Compositionality of rewriting rules with conditions
• scientific article; zbMATH DE number 4092742
• Logicality of conditional rewrite systems
• scientific article; zbMATH DE number 4092749
• scientific article; zbMATH DE number 4090849
• scientific article; zbMATH DE number 4090846
• Publication:5749279
• scientific article; zbMATH DE number 4092758
• scientific article; zbMATH DE number 4090848
• Publication:3028335

Cites work

• A Practical Decision Procedure for Arithmetic with Function Symbols
• Automatic proofs by induction in theories without constructors
• Conditional rewrite rules
• Decidability of Second-Order Theories and Automata on Infinite Trees
• scientific article; zbMATH DE number 3827173 (Why is no real title available?)
• scientific article; zbMATH DE number 3921957 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 4183386 (Why is no real title available?)
• On the SUP-INF Method for Proving Presburger Formulas
• Proofs by induction in equational theories with constructors
• Refutational theorem proving using term-rewriting systems

Cited in

(7)

• scientific article; zbMATH DE number 1639660 (Why is no real title available?)
• FULL LAMBEK CALCULUS WITH CONTRACTION IS UNDECIDABLE
• scientific article; zbMATH DE number 4203770 (Why is no real title available?)
• scientific article; zbMATH DE number 4090849 (Why is no real title available?)
• Could orders be captured by term rewriting systems?
• A Rule-Based System for Computation and Deduction in Mathematica
• On theorem-proving in Horn theories with built-in algebras

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055742)