Introduces token-sensitive enclosure semantics where each measurement carries an interval and an observation token, defining warranted enclosures as sets of consistent values, with proofs that token-erased summaries cannot recover correct rewrite classes, all mechanized in Lean 4.
Term Rewriting and All That
4 Pith papers cite this work. Polarity classification is still indexing.
4
Pith papers citing it
representative citing papers
The Confluence Framework provides a modular strategy to automatically prove and disprove confluence for a broad class of generalized term rewriting systems.
The authors perform and analyze three reformalizations of the Jordan Curve Theorem from Mizar to Lean, HOL Light to Lean, and HOL Light to Agda.
A template-based lemma generation method integrated into bounded rewriting induction for higher-order LCSTRSs enables proving program equivalences previously out of reach.
citing papers explorer
-
Token-Sensitive Enclosure Semantics for Measurement-Bearing Expressions
Introduces token-sensitive enclosure semantics where each measurement carries an interval and an observation token, defining warranted enclosures as sets of consistent values, with proofs that token-erased summaries cannot recover correct rewrite classes, all mechanized in Lean 4.
-
Proving Confluence in the Confluence Framework with CONFident
The Confluence Framework provides a modular strategy to automatically prove and disprove confluence for a broad class of generalized term rewriting systems.
-
Reformalization of the Jordan Curve Theorem
The authors perform and analyze three reformalizations of the Jordan Curve Theorem from Mizar to Lean, HOL Light to Lean, and HOL Light to Agda.
-
Templates in Rewriting Induction
A template-based lemma generation method integrated into bounded rewriting induction for higher-order LCSTRSs enables proving program equivalences previously out of reach.