Induction = I-axiomatization + first-order consistency.

DOI10.1006/inco.2000.2875zbMath1046.68640OpenAlexW2007008828MaRDI QIDQ1854350

Hubert Comon, Robert Nieuwenhuis

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

zbMATH Keywords

inductive proofsfirst-order theorem prover

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items

Attacking group protocols by refuting incorrect inductive conjectures, Model building with ordered resolution: Extracting models from saturated clause sets, Superposition for Fixed Domains, 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, Generalized rewrite theories, coherence completion, and symbolic methods, Deciding the Inductive Validity of ∀ ∃ * Queries, Inductive proof search modulo, Narrowing and Rewriting Logic: from Foundations to Applications

Uses Software

• Saturate
• RRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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