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

explicit inductionimplicit inductioninduction schemesinductive theorem provingwell-founded orders

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Review text

There are two kinds of proof methods used in automating inductive theorem proving: explicit induction, which uses induction schemes, and implicit induction (sometimes called `inductionless induction'), which is based on procedures like Knuth-Bendix completion. The former offers the flexibility of induction over arbitrary well-founded orders and the latter better supports mutual induction (where a theorem and a lemma can appeal to each other in their proofs). The authors propose a proof method that combines the benefits of both by showing how explicit induction can use well-founded orders on terms that represent propositions.

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

• 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
• 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?)
• 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)

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

Describes a project that uses

Uses Software

• NQTHM
• InKa

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)