Induction = I-axiomatization + first-order consistency.
type: Item
instance of: scholarly article
title: Induction = I-axiomatization + first-order consistency.
zbMATH Open document ID: 1046.68640
author: Hubert Comon
author: Robert Nieuwenhuis
published in: Information and Computation
publication date: 2003-01-14T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 1853108
zbMATH Keywords: inductive proofs
zbMATH Keywords: first-order theorem prover
describes a project that uses: RRL
describes a project that uses: Saturate
MaRDI profile type: Publication
full work available at URL: inco.2000.2875
OpenAlex ID: W2007008828
cites work: Q4000281
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: Basic paramodulation
cites work: Proof by consistency in conditional equational theories
cites work: Implicit induction in conditional theories
cites work: Syntacticness, cycle-syntacticness and shallow theories
cites work: Ground reducibility is EXPTIME-complete
cites work: Q4936127
cites work: Q4297316
cites work: Orderings for term-rewriting systems
cites work: Q4385532
cites work: Q3336735
cites work: Q3725540
cites work: Proofs by induction in equational theories with constructors
cites work: Automatic proofs by induction in theories without constructors
cites work: Proof by consistency
cites work: On ground-confluence of term rewriting systems
cites work: On sufficient-completeness and related properties of term rewriting systems
cites work: Sufficient-completeness, ground-reducibility and their complexity
cites work: Q3427354
cites work: Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7--10, 1999. Proceedings
cites work: Theorem proving with ordering and equality constrained clauses
cites work: Semantic confluence tests and completion methods
cites work: Q3477997
cites work: Q3348437
cites work: Ordered rewriting and confluence
cites work: Term rewriting induction
DOI: 10.1006/INCO.2000.2875
description: scientific article; zbMATH DE number 1853108