Induction = I-axiomatization + first-order consistency.
From MaRDI portal
Publication:1854350
DOI10.1006/inco.2000.2875zbMath1046.68640MaRDI QIDQ1854350
Robert Nieuwenhuis, Hubert Comon
Publication date: 14 January 2003
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1006/inco.2000.2875
68Q65: Abstract data types; algebraic specification
03B35: Mechanization of proofs and logical operations
68Q42: Grammars and rewriting systems
Related Items
Harald Ganzinger’s Legacy: Contributions to Logics and Programming, Narrowing Based Inductive Proof Search, Decidability Results for Saturation-Based Model Building, Predicate Completion for non-Horn Clause Sets, System Description: SPASS-FD, Attacking group protocols by refuting incorrect inductive conjectures, Inductive proof search modulo, Model building with ordered resolution: Extracting models from saturated clause sets, Narrowing and Rewriting Logic: from Foundations to Applications, Superposition for Fixed Domains, Deciding the Inductive Validity of ∀ ∃ * Queries
Uses Software
Cites Work
- Orderings for term-rewriting systems
- Proofs by induction in equational theories with constructors
- On ground-confluence of term rewriting systems
- On sufficient-completeness and related properties of term rewriting systems
- Proof by consistency
- Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7--10, 1999. Proceedings
- Syntacticness, cycle-syntacticness and shallow theories
- Automatic proofs by induction in theories without constructors
- Ground reducibility is EXPTIME-complete
- Implicit induction in conditional theories
- Theorem proving with ordering and equality constrained clauses
- Basic paramodulation
- Sufficient-completeness, ground-reducibility and their complexity
- Semantic confluence tests and completion methods
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- 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
