TL;DR
This paper introduces the concept of coinductive validity, contrasting it with inductive validity, and explains how judgments can be validated through formal proofs, including proofs by coinduction.
Contribution
It formally defines coinductive validity and demonstrates its relation to formal proofs, expanding the understanding of proof methods in logic.
Findings
Coinductive validity is formally defined and contrasted with inductive validity.
A formal proof system for coinductive judgments is established.
Illustrations of proofs by coinduction are provided.
Abstract
This note formally defines the concept of coinductive validity of judgements, and contrasts it with inductive validity. For both notions it shows how a judgement is valid iff it has a formal proof. Finally, it defines and illustrates the notion of a proof by coinduction.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.