Abstract
We show how well-known refinements of ordered resolution, in particular redundancy elimination and ordering constraints in combination with a selection function, can be used to obtain a decision procedure for the guarded fragment with transitive guards. Another contribution of the paper is a special scheme notation, that allows to describe saturation strategies and show their correctness in a concise form.
| Original language | English |
|---|---|
| Pages (from-to) | 122-136 |
| Number of pages | 15 |
| Journal | Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) |
| Volume | 3097 |
| DOIs | |
| Publication status | Published - 2004 |
| Externally published | Yes |
| Event | Second International Joint Conference, IJCAR 2004 - Cork, Ireland Duration: Jul 4 2004 → Jul 8 2004 |
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science