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
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