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

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Splitting through New Proposition Symbols

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

de Nivelle,  Hans
Programming Logics, 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

de Nivelle, H. (2001). Splitting through New Proposition Symbols. In R. Nieuwenhuis, & A. Voronkov (Eds.), Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001) (pp. 172-185). Berlin, Germany: Springer.


Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-3245-A
Abstract
This paper presents ways of simulating splitting through new propositional symbols. The contribution of the paper is that the method presented here does not loose backward redundancy. We give a general method of obtaining a calculus with splitting by adjoining splitting symbols to an arbitrary resolution refinement. We then prove a relative completeness theorem: Every saturated set of clauses of the resolution calculus with adjoined proposition symbols contains a saturated set of the original resolution refinement without adjoined symbols.