Automata-driven automated induction

DOI10.1006/inco.2001.3036zbMath1008.03009MaRDI QIDQ1854445

Jean-Pierre Jouannaud, Adel Bouhoula

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/0fcc38871b21f3e1d574869ad39aa94d42d60200

zbMATH Keywords

tree automata; inductive theorem proving; complete axiomatization; finite trees

Mathematics Subject Classification ID

68Q45: Formal languages and automata

03B35: Mechanization of proofs and logical operations

68Q42: Grammars and rewriting systems

Related Items

Sound generalizations in mathematical induction, Specification and proof in membership equational logic, Alternating two-way AC-tree automata, Automated Induction with Constrained Tree Automata

Uses Software

• PVS
• Maude
• NQTHM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Using induction and rewriting to verify and complete parameterized specifications
• A rationale for conditional equational programming
• Conditional rewrite rules
• Equational formulae with membership constraints
• Automated theorem proving by test set induction
• Automatic proofs by induction in theories without constructors
• Implicit induction in conditional theories
• Tree automata help one to solve equational formulae in AC-theories
• Positive and negative results for higher-order disunification
• A methodological view of constraint solving
• Specification and proof in membership equational logic
• Inductive proofs by specification transformations
• Encompassment properties and automata with constraints