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