Resolution Decision Procedures 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
| Address |
Stuhlsatzenhausweg 85‚ 66123 Saarbrücken‚ Germany |
| Institution |
Max−Planck−Institut für Informatik |
| ISSN |
0946−011X |
| Month |
April |
| Number |
MPI−I−2004−2−001 |
| Year |
2004 |
Links
Related pages
|
People |
|
|
Activities |