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
- Publisher:
- Springer
- Host title:
- IJCAR
- Volume:
- 3097
- Publication date:
- 2004-01-01
- UUID:
-
uuid:965ca050-b8eb-46f7-93fb-001606e6a94d
- Local pid:
-
cs:887
- Deposit date:
-
2015-03-31
- ARK identifier:
Terms of use
- Copyright date:
- 2004
If you are the owner of this record, you can report an update to it here: Report update to this record