A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards.
Yevgeny Kazakov and Hans de Nivelle
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
Details
| Book Title |
IJCAR |
| Pages |
122−136 |
| Publisher |
Springer |
| Series |
Lecture Notes in Computer Science |
| Volume |
3097 |
| Year |
2004 |
Links
Related pages
|
People |
|
|
Activities |