@InCollection{Torre99thelogic,
  Title                    = {The Logic Of Reusable Propositional Output With The Fulfilment Constraint},
  Author                   = {Leendert van der Torre},
  Booktitle                = {Labelled Deduction, volume 17 of Applied Logic Series},
  Publisher                = {Kluwer},
  Year                     = {2000},
  Pages                    = {245--266},

  Abstract                 = {This paper shows the equivalence of three ways of expressing a certain strong consistency constraint -- called the fulfilment constraint -- on proofs of the logic of reusable propositional output: as a global requirement on proofs, as a local requirement on labels of formulas, and by phasing of proof rules. More specifically, we first show that the fulfilment constraint may be expressed either as a requirement on the historical structure of the proof tree or as a requirement on the contents of labels attached to its nodes. Second, we show that labelled proofs may be rewritten into a tightly phased form in which rules are applied in a fixed order. Third, we show that when a proof is in such a phased form, the consistency check on labels becomes redundant.},
  Bdsk-url-1               = {http://icr.uni.lu/leonvandertorre/papers/ld99.ps.Z},
  Date-modified            = {2011-12-20 17:12:43 +0100},
  Url                      = {http://icr.uni.lu/leonvandertorre/papers/ld99.ps.Z}
}