Temporal Resolution: Removing Irrelevant Information

The generation of too much information prohibits efficient resolution proof search in classical logics. Hence 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, for example that by Fisher (1991) for propositional linear-time temporal logics, further magnifies this problem. We provide an algorithm to efficiently remove irrelevant information prior to the application of Fisher's temporal resolution rule, show that it retains the completeness of the temporal resolution system and demonstrate its efficiency on a set of examples.

Authors

• Clare Dixon

Keywords

• Logic
• Databases
• Right-hand
• Left Side
• Negation
• Right-hand Side
• Left-hand Side
• Set Of Rules
• Hand Side
• Moment In Time
• Normal Form
• Resolution Methods
• Application Of Rules
• Breadth-first Search
• State Index
• Set Of Propositions
• Temporal Logic
• Classical Logic
• Set Of Formulas
• Unit Resolution
• Propositional Logic
• Step Resolution
• Model Checking
• Subset Of Data
• Small Problems
• Decision Problem