Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 4, August 2002: pp. 561-581

On the Relationship between [ohgr]-automata and Temporal Logic Normal Forms

Alexander Bolotov1, Michael Fisher2 and Clare Dixon2

1Harrow School of Computer Science, University of Westminster, Harrow HA1 3TP, UK. E-mail: A.Bolotov@westminster.ac.uk
2Department of Computer Science, University of Liverpool, Liverpool L69 7ZF, UK. E-mail: {M.Fisher,C.Dixon}@csc.liv.ac.uk

We consider the relationship between [ohgr]-automata and a specific logical formulation based on a normal form for temporal logic formulae. While this normal form was developed for use with execution and clausal resolution in temporal logics, we here show how it can represent, syntactically, [ohgr]-automata in a high-level way. Technical proofs of the correctness of this representation are given.

Keywords: Temporal logics; normal forms; automata; theorem-proving; clausal resolution

Table of Contents   Full-Text PDF (232 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement