2 papers
cs.LO2026
A Transfer Tactic for Lean
Zhaoxi Chen, Daniel Raggi
Rewriting in proof assistants spans a strict hierarchy. Equational rewriting substitutes based on extensional equality; subequational rewriting substitutes based on homogeneous rel…
cs.LG2025
Structure Transfer: an Inference-Based Calculus for the Transformation of Representations
Daniel Raggi, Gem Stapleton, Mateja Jamnik +3
Representation choice is of fundamental importance to our ability to communicate and reason effectively. A major unsolved problem, addressed in this paper, is how to devise represe…