Skip to main content

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

Book Title
IJCAR
Pages
122−136
Publisher
Springer
Series
Lecture Notes in Computer Science
Volume
3097
Year
2004