de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Obtaining Finite Local Theory Axiomatizations via Saturation

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44642

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

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45516

Sofronie-Stokkermans,  Viorica
Automation of Logic, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
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: http://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.