Induction using term orderings
From MaRDI portal
Publication:5210765
DOI10.1007/3-540-58156-1_8zbMath1433.68537OpenAlexW1484343045MaRDI QIDQ5210765
Francois Bronsard, Robert W. Hasker, Uday S. Reddy
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
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Uses Software
Cites Work
- Automating inductionless induction using test sets
- Proofs by induction in equational theories with constructors
- Proof by consistency
- Automatic proofs by induction in theories without constructors
- Proving termination with multiset orderings
- On notions of inductive validity for first-order equational clauses
- A Machine-Oriented Logic Based on the Resolution Principle
- Proving Properties of Programs by Structural Induction
- Reduction techniques for first-order reasoning
- Conditional rewriting in focus
- Proof by consistency in conditional equational theories
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item