Induction = I-axiomatization + first-order consistency.

From MaRDI portal
Revision as of 12:11, 1 February 2024 by Import240129110113 (talk | contribs) (Created automatically from import240129110113)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Publication:1854350


DOI10.1006/inco.2000.2875zbMath1046.68640MaRDI 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 proofs; first-order theorem prover


Mathematics Subject Classification ID

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, Generalized rewrite theories, coherence completion, and symbolic methods, Narrowing and Rewriting Logic: from Foundations to Applications, Superposition for Fixed Domains, Deciding the Inductive Validity of ∀ ∃ * Queries


Uses Software


Cites Work

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:1854350&oldid=14238396"
Powered by MediaWiki