Inductive definitions and rule inductions are two fundamental reasoning tools in logic and computer science. When inductive definitions involve binders, then Barendregt's variable convention is nearly always employed (explicitly or implicitly) in order to obtain simple proofs. Using this convention, one does not consider truly arbitrary bound names, as required by the rule induction principle, but rather bound names about which various freshness assumptions are made. Unfortunately, neither Barendregt nor others give a formal justification for the variable convention, which makes it hard to formalise such proofs. In this paper we identify conditions an inductive definition has to satisfy so that a form of the variable convention can be built into the rule induction principle. In practice this means we come quite close to the informal reasoning of "pencil-and-paper" proofs, while remaining completely formal. Our conditions also reveal circumstances in which Barendregt's variable convention is not applicable, and can even lead to faulty reasoning. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Urban, C., Berghofer, S., & Norrish, M. (2007). Barendregt’s variable convention in rule inductions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4603 LNAI, pp. 35–50). Springer Verlag. https://doi.org/10.1007/978-3-540-73595-3_4
Mendeley helps you to discover research relevant for your work.