@inproceedings{14f181d6c7fa4f7e8961ca75234fcc46,
title = "Deciding Monodic Fragments by Temporal Resolution",
abstract = "In this paper we study the decidability of various fragments of monodic first-order temporal logic by temporal resolution. We focus on two resolution calculi, namely, monodic temporal resolution and fine-grained temporal resolution. For the first, we state a very general decidability result, which is independent of the particular decision procedure used to decide the first-order part of the logic. For the second, we introduce refinements using orderings and selection functions. This allows us to transfer existing results on decidability by resolution for first-order fragments to monodic first-order temporal logic and obtain new decision procedures. The latter is of immediate practical value, due to the availability of TeMP, an implementation of fine-grained temporal resolution.",
author = "U Hustadt and B Konev and Schmidt, {R A}",
year = "2005",
language = "English",
volume = "3632",
series = "Lecture Notes in Artificial Intelligence",
publisher = "Springer Nature",
pages = "204--218",
editor = "R Nieuwenhuis",
booktitle = "Proceedings of the 20th International Conference on Automated Deduction (CADE-20)",
address = "United States",
note = "Proceedings of the 20th International Conference on Automated Deduction (CADE-20) ; Conference date: 01-01-1824",
}