The Logic Of Reusable Propositional Output With The Fulfilment Constraint (bibtex)
by Leendert van der Torre
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.
Reference:
The Logic Of Reusable Propositional Output With The Fulfilment Constraint (Leendert van der Torre), Chapter in Labelled Deduction, volume 17 of Applied Logic Series, Kluwer, 2000.
Bibtex Entry:
@InCollection{Torre2000a,
  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},
  Timestamp                = {2013.07.26},
  Url                      = {http://icr.uni.lu/leonvandertorre/papers/ld99.ps.Z}
}
Powered by bibtexbrowser