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.
Cite
CITATION STYLE
Kazakov, Y., & De Nivelle, H. (2004). A resolution decision procedure for the guarded fragment with transitive guards. In Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) (Vol. 3097, pp. 122–136). Springer Verlag. https://doi.org/10.1007/978-3-540-25984-8_7
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
