Name
Abstract | ||
|---|---|---|
Monodic first-order temporal logic is a fragment of first-order temporal logic for which sound and complete calculi have been devised. One such calculus is ordered fine-grained resolution with selection, which is implemented in the theorem prover TeMP. However, the architecture of TeMP cannot guarantee the fairness of its derivations. In this paper we present an architecture for a resolution-based monodic first-order temporal logic prover that can ensure fair derivations and we describe the implementation of this fair architecture in the theorem prover TSPASS. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.3233/AIC-2010-0457 | AI Commun. |
Keywords | DocType | Volume |
fair architecture,fair monodic temporal logic,complete calculus,first-order temporal logic,monodic first-order temporal logic,fair derivation,fine-grained resolution,theorem prover,temporal logic | Journal | 23 |
Issue | ISSN | Citations |
2-3 | 0921-7126 | 13 |
PageRank | References | Authors |
0.59 | 16 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michel Ludwig | 1 | 113 | 7.67 |
| Ullrich Hustadt | 2 | 1007 | 66.68 |