A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards

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.

• Type: Conference
• Year: 2004
• Where: CADE
• Authors: Yevgeny Kazakov, Hans de Nivelle
• Keywords: Automated Reasoning, CADE 2004, Particular Redundancy Elimination, Special Scheme Notation, Well-known Refinements