Analysis and Mechanisation of Decidable First-Order
Temporal Logics-Related Papers
- A. Artale, C. Dixon, M. Fisher, and E. Franconi (editors)
Special Issue on Temporal Representation and Reasoning (TIME),
Journal of Logic and Computation,
volume 14, number 1, 2004. Oxford University Press. ISSN 0955-792X.
- A. Artale, E. Franconi, F. Wolter and M. Zakharyaschev.
A temporal description logic for reasoning over conceptual schemas
and queries.
In S. Flesca, S. Greco, N. Leone, and G. Ianni, editors, Proceedings of
JELIA'02, volume 2424 of LNCS, pages 98-110, Springer, 2002.
- S. Bauer, I. Hodkinson, F. Wolter and M. Zakharyaschev.
On non-local propositional and one-variable quantified
CTL*.
Proceedings of TIME 2002, pp.2-9. IEEE Computer Science Press, 2002.
- S. Bauer, I. Hodkinson, F. Wolter, and M. Zakharyaschev.
On non-local
propositional and weak monodic quantified CTL*.
Journal of Logic and Computation, volume 14, pages 3-22, 2004.
- B. Bennett, C. Dixon, M. Fisher, U. Hustadt, E. Franconi, I. Horrocks,
and M. de Rijke
Combinations of Modal Logics.
Artificial Intelligence Review, 17(1):1-20. 2002
(Preliminary
version.)
- A. Degtyarev, M. Fisher, and B. Konev
A simplified clausal resolution procedure for propositional
linear-time temporal logic
In C. Fermüller and U. Egly, editors,
Proceedings of TABLEAUX 2002: Automated Reasoning with Tableaux and Related Methods,
Lecture Notes in Computer Science,
volume 2381, pages 85-99, Springer-Verlag, July 2002.
- A. Degtyarev, M. Fisher, and B. Konev,
Monodic Temporal Resolution.
In F. Baader, editor, Proceedings of CADE'19: International Conference
on Automated Deduction, Lecture Notes in Computer Science,
Springer-Verlag, 2003.
- A. Degtyarev, M. Fisher, and B. Konev,
Monodic Temporal Resolution.
ACM Transactions on Computational Logic. To appear.
- A. Degtyarev, M. Fisher, and A. Lisitsa.
Equality and monodic first-order temporal logic.
Studia Logica, 72(2), 2002
- C. Dixon.
Using Temporal Logics of Knowledge for Specification and
Verification-a Case Study
Journal of Applied Logic, Elsevier Science, to appear.
- M. Fisher and A. Lisitsa
Monodic ASMs and Temporal Verification.
In Proc. International Workshop on Abstract State Machines (ASM
2004). Volume
3065 of Lecture Notes in Computer Science. Springer-Verlag,
2004. Version also available as Technical Report
ULCS-03-011
from Department of Computer Science at the University of Liverpool.
- D.M. Gabbay, A. Kurucz, F. Wolter and M. Zakharyaschev.
Many-Dimensional Modal Logics: Theory and Applications.
Studies in Logic and the Foundations
of Mathematics, 148. Elsevier, North-Holland. 2003.
- D. Gabelaia, R. Kontchakov, A. Kurucz, F. Wolter, and M. Zakharyaschev.
On the computational complexity of spatio-temporal logics.
Proceedings of
the Sixteenth International Florida Artificial Intelligence Research
Symposium Conference (FLAIRS 2003), AAAI Press, pp.460-464.
- M.C. Fernandez-Gago, U. Hustadt, C. Dixon, M. Fisher, and B. Konev,
First-Order Temporal Verification in Practice
Journal of Automated Reasoning, Kluver, in press.
- I. Hodkinson.
Monodic packed fragment with equality is decidable.
Studia Logica, volume 72, pages 185-197, 2002.
- I. Hodkinson.
Complexity of monodic guarded fragments over linear and real
time
Annals of Pure Applied Logic, to appear, 34 pages.
- I. Hodkinson, R. Kontchakov, A. Kurucz, F. Wolter, and
M.Zakharyaschev,
On the computational complexity of decidable fragments
of first-order linear temporal logics.
Proc. TIME-ICTL 2003 (M Reynolds and A Sattar, eds.), IEEE, 2003, pp. 91-98.
- I. Hodkinson, F. Wolter and M. Zakharyaschev.
Monodic fragments of first-order temporal
logics: 2000--2001 A.D.
In Logic for Programming, Artificial Intelligence and Reasoning, number
2250 of LNAI, Springer 2001, pp.1-23.
- I. Hodkinson, F. Wolter and M. Zakharyaschev.
Decidable and undecidable fragments of
first-order branching temporal logics.
Proceedings of the 17th Annual IEEE Symposium on Logic in Computer
Science, LICS 2002, pp.393-402.
- U. Hustadt and B.Konev
TRP++ 2.0: A Temporal Resolution Prover.
In F. Baader, editor, Proceedings of the 19th International Conference
on Automated Deduction CADE-19 (Miami Beach, USA, July/August 2003),
pp. 274-278. LNAI 2741, Springer.
- U. Hustadt, B.Konev, A. Riazanov and A. Voronkov,
TeMP: A Temporal Monodic Prover
In D.A.Basin and M. Rusinowitch, editors,
Proceedings of the Second International Joint Conference
on Automated Reasoning (IJCAR 2004), Cork, Ireland, July 2004,
LNAI 3097, pages 326--330, Springer.
Also University of Liverpool Technical Report
ULCS-04-004
- U. Hustadt and R.A. Schmidt,
Scientific Benchmarking with Temporal Logic
Decision Procedures
In D. Fensel, F. Giunchiglia, D. McGuinness and M.-A. Williams editors,
Proceedings of the Eighth International Conference
on Principles of Knowledge Representation and Reasoning (KR2002),
Toulouse, France 2002, pages 533-544, Morgan Kaufmann
- B. Konev, A. Degtyarev, C. Dixon, M. Fisher, U. Hustadt,
Towards the Implementation of First-Order Temporal Resolution: the
Expanding Domain Case
in the Proceedings of TIME-ICTL 2003, July 8-10 July 2003,
Cairns, Queensland, Australia. IEEE.
- B. Konev, A. Degtyarev, C. Dixon, M. Fisher, U. Hustadt,
Mechanizing First-Order Temporal Resolution
Information and Computation, 199(1-2), pages 55-86. Elsevier Science.
- B. Konev, A. Degtyarev, and M. Fisher.
Handling Equality in Monodic Temporal Resolution.
In M. Vardi and A. Voronkov, editors, Logic for Programming and Automated
Reasoning (LPAR 2003), Lecture Notes in Artificial Intelligence, volume
2850, Springer-Verlag, September 2003.
- R. Kontchakov, C. Lutz, F. Wolter, and M. Zakharyaschev.
Temporalising
tableaux.
Studia Logica, volume 76, pages 91-134, 2004.
- R.A. Schmidt and U. Hustadt
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae
In F. Baader editor, Automated Deduction---CADE-19,
2003, LNAI 2741, pages 412-426, Springer
- A.F.T. Winfield and J. Sa and M-C. Fernandez-Gago and C. Dixon and
M. Fisher
Using Temporal Logic to Specify Emergent Behaviours in Swarm Robotic
Systems
In Towards Autonomous Robotic Systems (TAROS), 2005
- F. Wolter and M. Zakharyaschev.
Axiomatizing the monodic fragment of first-order temporal
logic.
Annals of Pure and Applied Logic, volume 118, pages 133-145, 2002.
- F. Wolter and M. Zakharyaschev.
Qualitative spatio-temporal representation and reasoning:
a computational perspective.
"Exploring Artificial Intelligence in the New Millenium,"
Morgan Kaufmann, pages 155-215, 2003.