Automata-driven automated induction
From MaRDI portal
Publication:1854445
DOI10.1006/INCO.2001.3036zbMATH Open1008.03009OpenAlexW2120053687MaRDI QIDQ1854445FDOQ1854445
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
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
Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42) Mechanization of proofs and logical operations (03B35)
Cites Work
- Title not available (Why is that?)
- Positive and negative results for higher-order disunification
- Conditional rewrite rules
- Title not available (Why is that?)
- A rationale for conditional equational programming
- Title not available (Why is that?)
- A methodological view of constraint solving
- Implicit induction in conditional theories
- Specification and proof in membership equational logic
- Using induction and rewriting to verify and complete parameterized specifications
- Title not available (Why is that?)
- Automatic proofs by induction in theories without constructors
- Encompassment properties and automata with constraints
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Inductive proofs by specification transformations
- Equational formulae with membership constraints
- Automated theorem proving by test set induction
- Tree automata help one to solve equational formulae in AC-theories
Cited In (17)
- Automated mathematical induction
- Automating Induction with an SMT Solver
- Automata Tutor v3
- Sound generalizations in mathematical induction
- Alternating two-way AC-tree automata
- Automated Induction with Constrained Tree Automata
- Title not available (Why is that?)
- Deciding inductive validity of equations.
- Specification and proof in membership equational logic
- Deciding the Inductive Validity of ∀ ∃ * Queries
- Sufficient completeness verification for conditional and constrained TRS
- Automated Mathematical Induction
- Order-Sorted Parameterization and Induction
- On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
- Mechanically certifying formula-based Noetherian induction reasoning
- Checking Sufficient Completeness by Inductive Theorem Proving
- Automated Generation of BSP Automata
Uses Software
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)
