Mechanizable inductive proofs for a class of ∀ ∃ formulas

DOI10.1007/3-540-58156-1_9zbMath1434.03026OpenAlexW12716309MaRDI QIDQ5210766

Jacques Chazarain, Emmanuel Kounalis

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58156-1_9

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Equational logic, Mal'tsev conditions (08B05) First-order arithmetic and fragments (03F30) Equational classes, universal algebra in model theory (03C05)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Testing for the ground (co-)reducibility property in term-rewriting systems
• Rippling: A heuristic for guiding inductive proofs
• Proofs by induction in equational theories with constructors
• Termination of rewriting
• Deductive and inductive synthesis of equational programs
• Automatic proofs by induction in theories without constructors
• Proving Properties of Programs by Structural Induction

This page was built for publication: Mechanizable inductive proofs for a class of ∀ ∃ formulas