You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: Manchester Metropolitan University » Outputs » Detail

Output details

11 - Computer Science and Informatics

Manchester Metropolitan University

Return to search Previous output Next output

Output 37 of 37 in the submission

Article title

Writing out unifiers in Linear Temporal Logic

Type

D - Journal article

DOI

10.1093/logcom/exr022

Title of journal

Journal of Logic and Computation

Article number

Volume number

Issue number

First page of article

1199

ISSN of journal

1465-363X

Year of publication

2012

URL

Number of additional authors

Additional information

<11>The paper solves an important open problem: unifiablity in Linear Temporal Logic (LTL). We describe an algorithm which recognizes formulas unifiable in LTL and constructs their unifiers, so, in particular, solving the problem of terms rewriting in LTL. This technique is of vital importance in automated reasoning, logic programming and programming language type systems implementations, and may find application in hardware engineering. Our results may also be applicable in search engines for Web Ontology (via searching for answers using equivalent request specifications).

Interdisciplinary

Cross-referral requested

Research group

B - Computational Intelligence and Reasoning

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract