Labelled Natural Deduction for Interval Logics

Thomas Marthedal Rasmussen

doi:10.1007/3-540-44802-0_22

Labelled Natural Deduction for Interval Logics

Thomas Marthedal Rasmussen

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Abstract

We develop a Labelled Natural Deduction framework for a certain class of interval logics. With emphasis on Signed Interval Logic we consider normalization properties and show that normal derivations satisfy a subformula property. We have encoded our framework in the generic theorem proving system Isabelle. The labelled formalism turns out very convenient for conducting proofs and seems much closer to informal “pen and paper” reasoning than other proof systems. We give an example which supports this claim. We also sketch how the results are applicable to (non-signed) interval logic and Duration Calculus.

Original language	English
Title of host publication	Computer Science Logic: 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings : Lecture Notes in Computer Science, 2142
Publisher	Springer
Publication date	2001
Pages	308-323
DOIs	https://doi.org/10.1007/3-540-44802-0_22
Publication status	Published - 2001
Event	15th International Workshop on Computer Science Logic - Paris, France Duration: 10 Sept 2001 → 13 Sept 2001 Conference number: 15

Workshop

Workshop	15th International Workshop on Computer Science Logic
Number	15
Country/Territory	France
City	Paris
Period	10/09/2001 → 13/09/2001

Access to Document

10.1007/3-540-44802-0_22

OpenUrl availability

Check availability in DTU Findit

Cite this

@inproceedings{7231e38f069c4e7b93c44878782efa42,

title = "Labelled Natural Deduction for Interval Logics",

abstract = "We develop a Labelled Natural Deduction framework for a certain class of interval logics. With emphasis on Signed Interval Logic we consider normalization properties and show that normal derivations satisfy a subformula property. We have encoded our framework in the generic theorem proving system Isabelle. The labelled formalism turns out very convenient for conducting proofs and seems much closer to informal “pen and paper” reasoning than other proof systems. We give an example which supports this claim. We also sketch how the results are applicable to (non-signed) interval logic and Duration Calculus.",

author = "Rasmussen, \{Thomas Marthedal\}",

year = "2001",

doi = "10.1007/3-540-44802-0\_22",

language = "English",

pages = "308--323",

booktitle = "Computer Science Logic: 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings",

publisher = "Springer",

note = "15th International Workshop on Computer Science Logic, CSL 2001 ; Conference date: 10-09-2001 Through 13-09-2001",

}

Rasmussen, TM 2001, Labelled Natural Deduction for Interval Logics. in Computer Science Logic: 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings: Lecture Notes in Computer Science, 2142. Springer, pp. 308-323, 15th International Workshop on Computer Science Logic, Paris, France, 10/09/2001. https://doi.org/10.1007/3-540-44802-0_22

Labelled Natural Deduction for Interval Logics. / Rasmussen, Thomas Marthedal.
Computer Science Logic: 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings: Lecture Notes in Computer Science, 2142. Springer, 2001. p. 308-323.

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Labelled Natural Deduction for Interval Logics

AU - Rasmussen, Thomas Marthedal

N1 - Conference code: 15

PY - 2001

Y1 - 2001

N2 - We develop a Labelled Natural Deduction framework for a certain class of interval logics. With emphasis on Signed Interval Logic we consider normalization properties and show that normal derivations satisfy a subformula property. We have encoded our framework in the generic theorem proving system Isabelle. The labelled formalism turns out very convenient for conducting proofs and seems much closer to informal “pen and paper” reasoning than other proof systems. We give an example which supports this claim. We also sketch how the results are applicable to (non-signed) interval logic and Duration Calculus.

AB - We develop a Labelled Natural Deduction framework for a certain class of interval logics. With emphasis on Signed Interval Logic we consider normalization properties and show that normal derivations satisfy a subformula property. We have encoded our framework in the generic theorem proving system Isabelle. The labelled formalism turns out very convenient for conducting proofs and seems much closer to informal “pen and paper” reasoning than other proof systems. We give an example which supports this claim. We also sketch how the results are applicable to (non-signed) interval logic and Duration Calculus.

U2 - 10.1007/3-540-44802-0_22

DO - 10.1007/3-540-44802-0_22

M3 - Article in proceedings

SP - 308

EP - 323

BT - Computer Science Logic: 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings

PB - Springer

T2 - 15th International Workshop on Computer Science Logic

Y2 - 10 September 2001 through 13 September 2001

ER -

Labelled Natural Deduction for Interval Logics

Abstract

Workshop

Access to Document

OpenUrl availability

Fingerprint

Cite this