TY - GEN
T1 - Barendregt's variable convention in rule inductions
AU - Urban, Christian
AU - Berghofer, Stefan
AU - Norrish, Michael
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=35148859362&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-73595-3_4
DO - 10.1007/978-3-540-73595-3_4
M3 - Conference contribution
SN - 3540735941
SN - 9783540735946
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 35
EP - 50
BT - Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings
PB - Springer Verlag
T2 - 21st International Conference on Automated Deduction, CADE-21 2007
Y2 - 17 July 2007 through 20 July 2007
ER -