Automated Induction with Constrained Tree Automata

DOI10.1007/978-3-540-71070-7_44zbMath1165.68452OpenAlexW1556936708MaRDI QIDQ3541728

Adel Bouhoula, Florent Jacquemard

Publication date: 27 November 2008

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_44

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Verifying Procedural Programs via Constrained Rewriting Induction, Rewriting modulo SMT and open system analysis, Sufficient completeness verification for conditional and constrained TRS, Automated Induction with Constrained Tree Automata, On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs

Cites Work

• Unnamed Item
• Automated theorem proving by test set induction
• Automata-driven automated induction
• Ground reducibility is EXPTIME-complete
• Implicit induction in conditional theories
• Specification and proof in membership equational logic
• Tree automata with equality constraints modulo equational theories
• Automated Induction with Constrained Tree Automata
• Tree Automata with Memory, Visibility and Structural Constraints
• Implementing contextual rewriting
• A general framework to build contextual cover set induction provers