|
| << vorige |
Tijdschrift beschrijving
Alle jaargangen van het bijbehorende tijdschrift
Alle afleveringen van het bijbehorende jaargang
Alle artikelen van de bijbehorende aflevering
Details van artikel 7 van 7 gevonden artikelen
| Titel: |
Removing irrelevant information in temporal resolution proofs |
| Auteur: |
Dixon, Clare |
| Verschenen in: |
Journal of experimental & theoretical artificial intelligence |
| Paginering: | Jaargang 11 (1999) nr. 1 pagina's 95-121 |
| Jaar: |
1999-01-01 |
| Inhoud: |
The generation of too much information prohibits efficient resolution proof search in classical logics. Subsumption is used to discard redundant information and strategies have been developed to guide the proof search avoiding irrelevant information. The extension of the resolution method to temporal logics, further magnifies this problem. Here we develop an algorithm for the removal of irrelevant information during resolution proofs for a particular resolution proof system for propositional linear-time temporal logic. The resolution system operates on formulae in a normal form. Following a phase of classical style resolution, temporal resolution is carried out by detecting sets of formulae that together represent an-formula to be resolved with a-formula. It is before the application of the temporal resolution rule that the new algorithm is applied to efficiently remove irrelevant information. The completeness of the new algorithm is discussed and its complexity considered. Its practical efficiency is demonstrated by giving timings for a set of examples. |
| Uitgever: |
Taylor & Francis |
| Bronbestand: |
Elektronische Wetenschappelijke Tijdschriften |
Details van artikel 7 van 7 gevonden artikelen
| << vorige |