Axiomatisation of an interval calculus for theorem proving

Antonio Cerone

doi:10.1016/S1571-0661(04)80879-X

Axiomatisation of an interval calculus for theorem proving

Antonio Cerone

University of Queensland

Результат исследований › рецензирование

6 Цитирования (Scopus)

Аннотация

We provide an axiomatisation of the Timed Interval Calculus, a set-theoretic notation for expressing properties of time intervals. We implement the axiomatisation in the Ergo theorem prover in order to allow the machine-checked proof of laws for reasoning about predicates expressed using interval operators. These laws can be then used in the machine-assisted verification of real-time applications.

Язык оригинала	English
Страницы (с-по)	67-88
Число страниц	22
Журнал	Electronic Notes in Theoretical Computer Science
Том	42
DOI	https://doi.org/10.1016/S1571-0661(04)80879-X
Состояние	Published - янв. 2001
Опубликовано для внешнего пользования	Да
Событие	Computing: The Australasian Theory Symposium (CATS 2001) - Gold Coast Продолжительность: янв. 29 2001 → янв. 30 2001

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Доступ к документу

10.1016/S1571-0661(04)80879-X

Другие файлы и ссылки

Цитировать

@article{0f9f5f0a8450498c9187a92a1af68c2c,

title = "Axiomatisation of an interval calculus for theorem proving",

abstract = "We provide an axiomatisation of the Timed Interval Calculus, a set-theoretic notation for expressing properties of time intervals. We implement the axiomatisation in the Ergo theorem prover in order to allow the machine-checked proof of laws for reasoning about predicates expressed using interval operators. These laws can be then used in the machine-assisted verification of real-time applications.",

author = "Antonio Cerone",

year = "2001",

month = jan,

doi = "10.1016/S1571-0661(04)80879-X",

language = "English",

volume = "42",

pages = "67--88",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

note = "Computing: The Australasian Theory Symposium (CATS 2001) ; Conference date: 29-01-2001 Through 30-01-2001",

}

TY - JOUR

T1 - Axiomatisation of an interval calculus for theorem proving

AU - Cerone, Antonio

PY - 2001/1

Y1 - 2001/1

N2 - We provide an axiomatisation of the Timed Interval Calculus, a set-theoretic notation for expressing properties of time intervals. We implement the axiomatisation in the Ergo theorem prover in order to allow the machine-checked proof of laws for reasoning about predicates expressed using interval operators. These laws can be then used in the machine-assisted verification of real-time applications.

AB - We provide an axiomatisation of the Timed Interval Calculus, a set-theoretic notation for expressing properties of time intervals. We implement the axiomatisation in the Ergo theorem prover in order to allow the machine-checked proof of laws for reasoning about predicates expressed using interval operators. These laws can be then used in the machine-assisted verification of real-time applications.

UR - https://www.scopus.com/pages/publications/18944392699

UR - https://www.scopus.com/pages/publications/18944392699#tab=citedBy

U2 - 10.1016/S1571-0661(04)80879-X

DO - 10.1016/S1571-0661(04)80879-X

M3 - Conference article

AN - SCOPUS:18944392699

SN - 1571-0661

VL - 42

SP - 67

EP - 88

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

T2 - Computing: The Australasian Theory Symposium (CATS 2001)

Y2 - 29 January 2001 through 30 January 2001

ER -

Axiomatisation of an interval calculus for theorem proving

Аннотация

ASJC Scopus subject areas

Доступ к документу

Другие файлы и ссылки

Fingerprint

Цитировать