Towards the implementation of first-order temporal resolution:: The expanding domain case

B. Konev; C. Dixon; A. Degtyarev; M. Fisher; U. Hustadt

doi:10.1109/TIME.2003.1214882

Towards the implementation of first-order temporal resolution: The expanding domain case

B. Konev, C. Dixon, A. Degtyarev, M. Fisher, U. Hustadt

Formal Methods

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

Abstract

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. In this paper, we develop a clausal resolution method for the monodic fragment of first-order temporal logic over expanding domains. We first define a normal form for monodic formulae and then introduce novel resolution calculi that can be applied to formulae in this normal form. We state correctness and completeness results for the method. We illustrate the method on a comprehensive example. The method is based on classical first-order resolution and can, thus, be efficiently implemented.

Original language	English
Title of host publication	Proceedings of the International Workshop on Temporal Representation and Reasoning
Publisher	IEEE
ISBN (Print)	0769519121
DOIs	https://doi.org/10.1109/TIME.2003.1214882
Publication status	Published - 2003

Access to Document

10.1109/TIME.2003.1214882

Cite this

@inproceedings{934d06c39fec40b4910dc66146ff94bf,

title = "Towards the implementation of first-order temporal resolution:: The expanding domain case",

abstract = "First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. In this paper, we develop a clausal resolution method for the monodic fragment of first-order temporal logic over expanding domains. We first define a normal form for monodic formulae and then introduce novel resolution calculi that can be applied to formulae in this normal form. We state correctness and completeness results for the method. We illustrate the method on a comprehensive example. The method is based on classical first-order resolution and can, thus, be efficiently implemented.",

author = "B. Konev and C. Dixon and A. Degtyarev and M. Fisher and U. Hustadt",

year = "2003",

doi = "10.1109/TIME.2003.1214882",

language = "English",

isbn = "0769519121",

booktitle = "Proceedings of the International Workshop on Temporal Representation and Reasoning",

publisher = "IEEE",

address = "United States",

}

TY - GEN

T1 - Towards the implementation of first-order temporal resolution:

T2 - The expanding domain case

AU - Konev, B.

AU - Dixon, C.

AU - Degtyarev, A.

AU - Fisher, M.

AU - Hustadt, U.

PY - 2003

Y1 - 2003

N2 - First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. In this paper, we develop a clausal resolution method for the monodic fragment of first-order temporal logic over expanding domains. We first define a normal form for monodic formulae and then introduce novel resolution calculi that can be applied to formulae in this normal form. We state correctness and completeness results for the method. We illustrate the method on a comprehensive example. The method is based on classical first-order resolution and can, thus, be efficiently implemented.

AB - First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. In this paper, we develop a clausal resolution method for the monodic fragment of first-order temporal logic over expanding domains. We first define a normal form for monodic formulae and then introduce novel resolution calculi that can be applied to formulae in this normal form. We state correctness and completeness results for the method. We illustrate the method on a comprehensive example. The method is based on classical first-order resolution and can, thus, be efficiently implemented.

UR - http://www.scopus.com/inward/record.url?eid=2-s2.0-84944075546&partnerID=MN8TOARS

U2 - 10.1109/TIME.2003.1214882

DO - 10.1109/TIME.2003.1214882

M3 - Conference contribution

SN - 0769519121

BT - Proceedings of the International Workshop on Temporal Representation and Reasoning

PB - IEEE

ER -

Towards the implementation of first-order temporal resolution: The expanding domain case

Abstract

Access to Document

Other files and links

Fingerprint

Cite this