Proving open properties by induction

DOI10.1016/0020-0190(88)90126-3MaRDI QIDQ1112816zbMATH OpenOpenAlexFDO

Authors Jean Claude Raoult

Publication date 1988

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(88)90126-3

zbMATH Keywords

ordered setwell-quasi-ordernoetherian inductioncomplete partial ordereffective proof

Mathematics Subject Classification ID

Partial orders, general (06A06) Axiom of choice and related propositions (03E25)

Recommendations

• A calculational approach to mathematical induction
• scientific article; zbMATH DE number 5269389
• A uniform approach to inductive posets and inductive closure
• scientific article; zbMATH DE number 1841837
• Recursion, induction and well-founded orders

Cites work

• scientific article; zbMATH DE number 3706504 (Why is no real title available?)
• scientific article; zbMATH DE number 3227055 (Why is no real title available?)
• The varieties of arboreal experience
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture

Cited in

(22)

• Syntax for semantics: Krull's maximal ideal theorem
• The equivalence of bar recursion and open recursion
• The computational significance of Hausdorff's maximal chain principle
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• A Mechanized Proof of Higman’s Lemma by Open Induction
• A universal Krull-Lindenbaum theorem
• On the constructive and computational content of abstract mathematics
• Coq formalization of the higher-order recursive path ordering
• Certified Kruskal's tree theorem
• Constructing Gröbner bases for Noetherian rings
• A universal algorithm for Krull's theorem
• Lindenbaum's lemma via open induction
• Decision procedure of some relevant logics: a constructive perspective
• Programs from proofs using classical dependent choice
• Some new double induction and superinduction principles
• On induction principles for partial orders
• The Jacobson radical for an inconsistency predicate
• Well quasi-orders and the functional interpretation
• An induction principle over real numbers
• Eliminating disjunctions by disjunction elimination
• Eliminating disjunctions by disjunction elimination
• scientific article; zbMATH DE number 4033743 (Why is no real title available?)

Describes a project that uses

Uses Software

• Open Induction

This page was built for publication: Proving open properties by induction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1112816)