Induction using term orders

DOI10.1007/BF00244458MaRDI QIDQ1915132zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• Induction using term orderings
• Induction on concurrent terms
• Induction by enumeration
• Order-Sorted Parameterization and Induction
• On induction principles for partial orders
• Term rewriting induction
• Term Rewriting and Applications
• On the number of term orders
• Recursion, induction and well-founded orders
• Generator induction in order sorted algebras

Cites work

• scientific article; zbMATH DE number 4016226 (Why is no real title available?)
• scientific article; zbMATH DE number 4164140 (Why is no real title available?)
• scientific article; zbMATH DE number 4164172 (Why is no real title available?)
• scientific article; zbMATH DE number 4074541 (Why is no real title available?)
• scientific article; zbMATH DE number 3684925 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 4776 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A strong restriction of the inductive completion procedure
• A theorem prover for a computational logic
• Automatic proofs by induction in theories without constructors
• Automating inductionless induction using test sets
• Completeness of calculii for axiomatically defined classes of algebras
• Conditional rewriting in focus
• Induction using term orderings
• On notions of inductive validity for first-order equational clauses
• Proof by consistency
• Proofs by induction in equational theories with constructors
• Reduction techniques for first-order reasoning
• Resolution of equations in algebraic structures. Volume II: Rewriting techniques
• Term rewriting induction
• Topics in termination

Cited in

(7)

• Guiding induction proofs
• Sound generalizations in mathematical induction
• Mechanizing Mathematical Reasoning
• scientific article; zbMATH DE number 2090032 (Why is no real title available?)
• scientific article; zbMATH DE number 1696825 (Why is no real title available?)
• Induction using term orderings
• A general framework to build contextual cover set induction provers

Describes a project that uses

Uses Software

• InKa
• NQTHM

This page was built for publication: Induction using term orders

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