A Superposition Decision Procedure for the Guarded Fragment with Equality

Ganzinger, Harald; de Nivelle, Hans

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

A Superposition Decision Procedure for the Guarded Fragment with Equality

MPS-Authors

/persons/resource/persons44474

Ganzinger, Harald
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44298

de Nivelle, Hans
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Ganzinger, H., & de Nivelle, H. (1999). A Superposition Decision Procedure for the Guarded Fragment with Equality. In G. Longo (Ed.), Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS-99) (pp. 295-303). Los Alamitos, USA: IEEE.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-362C-2

Abstract

We give a decision procedure for the guarded fragment with equality. The procedure is based on resolution with superposition. The relevance of the guarded fragment lies in the fact that many modal logics can be translated into it. In this way the guarded fragment acts as a framework explaining some of the nice properties of these modal logics. By constructing an implementable decision procedure for the guarded fragments we define an effective procedure for deciding these modal logics. It is surprising to see that one does not need any sophisticated simplification and redundancy elimination method to make superposition terminate on the class of clauses that is obtained from the clausification of guarded formulas. Yet the decision procedure obtained is optimal with regard to time complexity.