非表示:
キーワード:
-
要旨:
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.