Automata-driven automated induction

DOI10.1006/inco.2001.3036zbMath1008.03009OpenAlexW2120053687MaRDI 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 automatainductive theorem provingcomplete axiomatizationfinite trees

Mathematics Subject Classification ID

Related Items (8)

Sound generalizations in mathematical induction ⋮ Alternating two-way AC-tree automata ⋮ Order-Sorted Parameterization and Induction ⋮ Sufficient completeness verification for conditional and constrained TRS ⋮ Automated Induction with Constrained Tree Automata ⋮ Specification and proof in membership equational logic ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ Deciding the Inductive Validity of ∀ ∃ * Queries

Uses Software

• PVS
• Maude
• NQTHM

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Automata-driven automated induction