Automata-driven automated induction

DOI10.1006/INCO.2001.3036MaRDI QIDQ1854445zbMATH OpenOpenAlexFDO

Authors Adel Bouhoula, Jean-Pierre Jouannaud

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 automatacomplete axiomatizationfinite treesinductive theorem proving

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42) Mechanization of proofs and logical operations (03B35)

Recommendations

• Automated Mathematical Induction
• Automated mathematical induction
• scientific article; zbMATH DE number 3880144
• Automated Induction with Constrained Tree Automata
• Automating Inductive Proofs Using Theory Exploration
• Automating Induction with an SMT Solver
• Publication:4934147
• Automated theorem proving by test set induction
• Automated Reasoning with Analytic Tableaux and Related Methods

Cites work

• scientific article; zbMATH DE number 4164171 (Why is no real title available?)
• scientific article; zbMATH DE number 3949706 (Why is no real title available?)
• scientific article; zbMATH DE number 4074540 (Why is no real title available?)
• scientific article; zbMATH DE number 4074541 (Why is no real title available?)
• scientific article; zbMATH DE number 3688776 (Why is no real title available?)
• scientific article; zbMATH DE number 1231537 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• A methodological view of constraint solving
• A rationale for conditional equational programming
• Automated theorem proving by test set induction
• Automatic proofs by induction in theories without constructors
• Conditional rewrite rules
• Encompassment properties and automata with constraints
• Equational formulae with membership constraints
• Implicit induction in conditional theories
• Inductive proofs by specification transformations
• Positive and negative results for higher-order disunification
• Specification and proof in membership equational logic
• Tree automata help one to solve equational formulae in AC-theories
• Using induction and rewriting to verify and complete parameterized specifications

Cited in

(17)

• Order-Sorted Parameterization and Induction
• On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
• Checking Sufficient Completeness by Inductive Theorem Proving
• Automata Tutor v3
• Alternating two-way AC-tree automata
• Automated Mathematical Induction
• Automating Induction with an SMT Solver
• Deciding the Inductive Validity of ∀ ∃ * Queries
• Specification and proof in membership equational logic
• Automated Induction with Constrained Tree Automata
• Deciding inductive validity of equations.
• scientific article; zbMATH DE number 1765694 (Why is no real title available?)
• Mechanically certifying formula-based Noetherian induction reasoning
• Automated mathematical induction
• Sufficient completeness verification for conditional and constrained TRS
• Automated Generation of BSP Automata
• Sound generalizations in mathematical induction

Describes a project that uses

Uses Software

• PVS
• Maude
• NQTHM

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

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