The set of support strategy in temporal resolution

C. Dixon; M. Fisher

doi:10.1109/TIME.1998.674140

The set of support strategy in temporal resolution

C. Dixon, M. Fisher

Formal Methods

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

A variety of proof methods have been developed to support the effective mechanisation of temporal logic. While clausal temporal resolution has been successfully employed for a range of problems, a number of improvements are still required. In particular, as there is no consistent control strategy underlying the method, a large amount of irrelevant information may sometimes be generated.Following on from classical resolution, where the Set of Support strategy has been used very successfully, we here introduce, justify and apply a temporal version of this strategy, thus allowing the supporting set to be carried over between the different phases of the resolution method. This not only restricts the production of irrelevant information but, under certain conditions, retains the completeness of the refutation process.

Original language	English
Title of host publication	Proceedings of the International Workshop on Temporal Representation and Reasoning
Publisher	IEEE
Pages	113-120
Number of pages	8
ISBN (Print)	0818684739
DOIs	https://doi.org/10.1109/TIME.1998.674140
Publication status	Published - 17 May 1998

Keywords

Logic Programming
Mathematics
Production
Database languages

Access to Document

10.1109/TIME.1998.674140

Cite this

@inproceedings{65ae55d49b8f4053902e315e431becd1,

title = "The set of support strategy in temporal resolution",

abstract = "A variety of proof methods have been developed to support the effective mechanisation of temporal logic. While clausal temporal resolution has been successfully employed for a range of problems, a number of improvements are still required. In particular, as there is no consistent control strategy underlying the method, a large amount of irrelevant information may sometimes be generated.Following on from classical resolution, where the Set of Support strategy has been used very successfully, we here introduce, justify and apply a temporal version of this strategy, thus allowing the supporting set to be carried over between the different phases of the resolution method. This not only restricts the production of irrelevant information but, under certain conditions, retains the completeness of the refutation process.",

keywords = "Logic Programming, Mathematics, Production, Database languages",

author = "C. Dixon and M. Fisher",

year = "1998",

month = may,

day = "17",

doi = "10.1109/TIME.1998.674140",

language = "English",

isbn = "0818684739",

pages = "113--120",

booktitle = "Proceedings of the International Workshop on Temporal Representation and Reasoning",

publisher = "IEEE",

address = "United States",

}

TY - GEN

T1 - The set of support strategy in temporal resolution

AU - Dixon, C.

AU - Fisher, M.

PY - 1998/5/17

Y1 - 1998/5/17

N2 - A variety of proof methods have been developed to support the effective mechanisation of temporal logic. While clausal temporal resolution has been successfully employed for a range of problems, a number of improvements are still required. In particular, as there is no consistent control strategy underlying the method, a large amount of irrelevant information may sometimes be generated.Following on from classical resolution, where the Set of Support strategy has been used very successfully, we here introduce, justify and apply a temporal version of this strategy, thus allowing the supporting set to be carried over between the different phases of the resolution method. This not only restricts the production of irrelevant information but, under certain conditions, retains the completeness of the refutation process.

AB - A variety of proof methods have been developed to support the effective mechanisation of temporal logic. While clausal temporal resolution has been successfully employed for a range of problems, a number of improvements are still required. In particular, as there is no consistent control strategy underlying the method, a large amount of irrelevant information may sometimes be generated.Following on from classical resolution, where the Set of Support strategy has been used very successfully, we here introduce, justify and apply a temporal version of this strategy, thus allowing the supporting set to be carried over between the different phases of the resolution method. This not only restricts the production of irrelevant information but, under certain conditions, retains the completeness of the refutation process.

KW - Logic Programming

KW - Mathematics

KW - Production

KW - Database languages

UR - http://www.scopus.com/inward/record.url?eid=2-s2.0-84949958617&partnerID=MN8TOARS

U2 - 10.1109/TIME.1998.674140

DO - 10.1109/TIME.1998.674140

M3 - Conference contribution

SN - 0818684739

SP - 113

EP - 120

BT - Proceedings of the International Workshop on Temporal Representation and Reasoning

PB - IEEE

ER -

The set of support strategy in temporal resolution

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this