Automated Proof Support for Interval Logics

Thomas Marthedal Rasmussen

doi:10.1007/3-540-45653-8_22

Automated Proof Support for Interval Logics

Thomas Marthedal Rasmussen

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

Abstract

We outline the background and motivation for the use of interval logics and consider some initial attempts toward proof support and automation. The main focus, though, is on recent work on these subjects. We compare different proof theoretical formalisms, in particular a "classical" versus a "labelled" one. We discuss encodings of these in the generic proof assistant Isabelle and consider some examples which show that in some cases the labelled formalism gives an order of magnitude improvement in proof length compared to a classical approach.

Original language	English
Title of host publication	Logic for Programming, Artificial Intelligence, and Reasoning
Volume	2250
Publisher	Springer Verlag
Publication date	2001
Pages	320-329
ISBN (Print)	978-354042957-9
DOIs	https://doi.org/10.1007/3-540-45653-8_22
Publication status	Published - 2001
Event	8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning - Havana, Cuba Duration: 3 Dec 2001 → 7 Dec 2001 Conference number: 8

Conference

Conference	8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Number	8
Country/Territory	Cuba
City	Havana
Period	03/12/2001 → 07/12/2001

Access to Document

10.1007/3-540-45653-8_22

OpenUrl availability

Full text

Cite this

@inproceedings{c1f35f2fc97346eaad8acb4698701d4f,

title = "Automated Proof Support for Interval Logics",

abstract = "We outline the background and motivation for the use of interval logics and consider some initial attempts toward proof support and automation. The main focus, though, is on recent work on these subjects. We compare different proof theoretical formalisms, in particular a {"}classical{"} versus a {"}labelled{"} one. We discuss encodings of these in the generic proof assistant Isabelle and consider some examples which show that in some cases the labelled formalism gives an order of magnitude improvement in proof length compared to a classical approach.",

author = "Rasmussen, {Thomas Marthedal}",

year = "2001",

doi = "10.1007/3-540-45653-8_22",

language = "English",

isbn = "978-354042957-9",

volume = "2250",

pages = "320--329",

booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning",

publisher = "Springer Verlag",

address = "Germany",

note = "8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2001 ; Conference date: 03-12-2001 Through 07-12-2001",

}

TY - GEN

T1 - Automated Proof Support for Interval Logics

AU - Rasmussen, Thomas Marthedal

N1 - Conference code: 8

PY - 2001

Y1 - 2001

N2 - We outline the background and motivation for the use of interval logics and consider some initial attempts toward proof support and automation. The main focus, though, is on recent work on these subjects. We compare different proof theoretical formalisms, in particular a "classical" versus a "labelled" one. We discuss encodings of these in the generic proof assistant Isabelle and consider some examples which show that in some cases the labelled formalism gives an order of magnitude improvement in proof length compared to a classical approach.

AB - We outline the background and motivation for the use of interval logics and consider some initial attempts toward proof support and automation. The main focus, though, is on recent work on these subjects. We compare different proof theoretical formalisms, in particular a "classical" versus a "labelled" one. We discuss encodings of these in the generic proof assistant Isabelle and consider some examples which show that in some cases the labelled formalism gives an order of magnitude improvement in proof length compared to a classical approach.

U2 - 10.1007/3-540-45653-8_22

DO - 10.1007/3-540-45653-8_22

M3 - Article in proceedings

SN - 978-354042957-9

VL - 2250

SP - 320

EP - 329

BT - Logic for Programming, Artificial Intelligence, and Reasoning

PB - Springer Verlag

T2 - 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning

Y2 - 3 December 2001 through 7 December 2001

ER -

Automated Proof Support for Interval Logics

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this