Barendregt's variable convention in rule inductions

Christian Urban*, Stefan Berghofer, Michael Norrish

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

39 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationAutomated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings
PublisherSpringer Verlag
Pages35-50
Number of pages16
ISBN (Print)3540735941, 9783540735946
DOIs
Publication statusPublished - 2007
Externally publishedYes
Event21st International Conference on Automated Deduction, CADE-21 2007 - Bremen, Germany
Duration: 17 Jul 200720 Jul 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4603 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st International Conference on Automated Deduction, CADE-21 2007
Country/TerritoryGermany
CityBremen
Period17/07/0720/07/07

Fingerprint

Dive into the research topics of 'Barendregt's variable convention in rule inductions'. Together they form a unique fingerprint.

Cite this