Induction using term orders

DOI10.1007/BF00244458zbMath0861.03008OpenAlexW1963988272MaRDI QIDQ1915132

Robert W. Hasker, Francois Bronsard, Uday S. Reddy

Publication date: 11 June 1996

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

Full work available at URL: https://doi.org/10.1007/bf00244458

zbMATH Keywords

inductive theorem provingexplicit inductionimplicit inductioninduction schemeswell-founded orders

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Sound generalizations in mathematical induction, A general framework to build contextual cover set induction provers

Uses Software

• NQTHM
• InKa

Cites Work

• Automating inductionless induction using test sets
• Proofs by induction in equational theories with constructors
• Proof by consistency
• A strong restriction of the inductive completion procedure
• Automatic proofs by induction in theories without constructors
• Completeness of calculii for axiomatically defined classes of algebras
• Topics in termination
• Induction using term orderings
• On notions of inductive validity for first-order equational clauses
• A Machine-Oriented Logic Based on the Resolution Principle
• Reduction techniques for first-order reasoning
• Conditional rewriting in focus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item