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 | |
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 |