Conference item icon

Conference item

A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards.

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

Actions


Authors


Yevgeny Kazakov More by this author
Hans de Nivelle More by this author
Publisher:
Springer
Volume:
3097
Publication date:
2004
URN:
uuid:965ca050-b8eb-46f7-93fb-001606e6a94d
Local pid:
cs:887

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP