Resolution Decision Procedures 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...
| Main Authors: | , |
|---|---|
| 格式: | Report |
| 出版: |
Max−Planck−Institut für Informatik
2015
|