Incorporating decision procedures in implicit induction.

DOI10.1006/jsco.2002.0549zbMath1037.68129OpenAlexW2031385999MaRDI QIDQ1404422

Alessandro Armando, Michaël Rusinowitch, Sorin Stratulat

Publication date: 21 August 2003

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

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

zbMATH Keywords

Buchberger algorithm

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Grammars and rewriting systems (68Q42)

Related Items

Formal design and verification of operational transformation algorithms for copies convergence, Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities, Mechanically certifying formula-based Noetherian induction reasoning, On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs, Automated Certification of Implicit Induction Proofs, Inductive theorem proving based on tree grammars

Uses Software

• PVS
• STeP

Cites Work

• On Fourier's algorithm for linear arithmetic constraints
• Automated theorem proving by test set induction
• Implicit induction in conditional theories
• A general framework to build contextual cover set induction provers
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item