Obtaining Finite Local Theory Axiomatizations via Saturation

Horbach, Matthias; Sofronie-Stokkermans, Viorica

doi:10.1007/978-3-642-40885-4_14

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Obtaining Finite Local Theory Axiomatizations via Saturation

MPS-Authors

/persons/resource/persons44642

Horbach, Matthias
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons45516

Sofronie-Stokkermans, Viorica
Automation of Logic, 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

Horbach, M., & Sofronie-Stokkermans, V. (2013). Obtaining Finite Local Theory Axiomatizations via Saturation. In P. Fontaine, C. Ringeissen, & R. A. Schmidt (Eds.), Frontiers of Combining Systems (pp. 198-213). Berlin: Springer. doi:10.1007/978-3-642-40885-4_14.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0015-797C-8

Abstract

In this paper we present a method for obtaining local sets of clauses from possibly non-local ones. For this, we follow the work of Basin and Ganzinger and use saturation under a version of ordered resolution. In order to address the fact that saturation can generate infinite sets of clauses, we use constrained clauses and show that a link can be established between saturation and locality also for constrained clauses: This often allows us to give a finite representation of possibly infinite saturated sets of clauses.