Bowman, Howard and Thompson, Simon (1997) A Tableau Method for Interval Temporal Logic. Technical report. University of Kent at Canterbury (KAR id:21432)
|
Postscript
Language: English |
|
|
Download this file (Postscript/278kB) |
Preview |
| Request a format suitable for use with assistive technology e.g. a screenreader | |
|
PDF
Language: English |
|
|
Download this file (PDF/62kB) |
Preview |
| Request a format suitable for use with assistive technology e.g. a screenreader | |
Abstract
In this paper we present a complete tableau method for interval temporal logic including the projection operator. Central to our strategy is the identification of normal forms for all the operators of our logic. In effect, these normal forms give inductive definitions of the ITL operators. Then, in the style of Wolper, we define a tableau decision procedure to check satisfiability of our logic. For simplicity of presentation we work in the propositional setting.
| Item Type: | Reports and Papers (Technical report) |
|---|---|
| Uncontrolled keywords: | tableau interval temporal logic normal form |
| Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
| Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
| Depositing User: | Mark Wheadon |
| Date Deposited: | 02 Aug 2009 20:20 UTC |
| Last Modified: | 16 Nov 2021 09:59 UTC |
| Resource URI: | https://kar.kent.ac.uk/id/eprint/21432 (The current URI for this page, for reference purposes) |
University of Kent Author Information
Bowman, Howard.
| Creator's ORCID: |
 https://orcid.org/0000-0003-4736-1869
|
|---|---|
| CReDIT Contributor Roles: |
Thompson, Simon.
| Creator's ORCID: |
https://orcid.org/0000-0002-2350-301X
|
|---|---|
| CReDIT Contributor Roles: |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):
Download Statistics
Download Statistics
