Induction using term orderings

DOI10.1007/3-540-58156-1_8MaRDI QIDQ5210765zbMATH OpenOpenAlexFDO

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

Publication date 21 January 2020

Published in Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-58156-1_8

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Induction using term orders
• scientific article; zbMATH DE number 3956434
• A strong restriction of the inductive completion procedure
• Inductionless induction
• Completion procedures as semidecision procedures

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• Automatic proofs by induction in theories without constructors
• Automating inductionless induction using test sets
• Conditional rewriting in focus
• scientific article; zbMATH DE number 4164140 (Why is no real title available?)
• scientific article; zbMATH DE number 4164171 (Why is no real title available?)
• scientific article; zbMATH DE number 4164172 (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?)
• On notions of inductive validity for first-order equational clauses
• Proof by consistency
• Proof by consistency in conditional equational theories
• Proofs by induction in equational theories with constructors
• Proving Properties of Programs by Structural Induction
• Proving termination with multiset orderings
• Reduction techniques for first-order reasoning
• Term rewriting induction

Cited in

(9)

• Induction using term orders
• scientific article; zbMATH DE number 1696825 (Why is no real title available?)
• Order-Sorted Parameterization and Induction
• scientific article; zbMATH DE number 1107768 (Why is no real title available?)
• scientific article; zbMATH DE number 2090032 (Why is no real title available?)
• Mechanically certifying formula-based Noetherian induction reasoning
• Generic induction proofs
• Generating mutually inductive theorems from concise descriptions
• A unified view of induction reasoning for first-order logic

Describes a project that uses

Uses Software

• InKa
• NQTHM

This page was built for publication: Induction using term orderings

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