Skip to Main content Skip to Navigation
Conference papers

Polarized Resolution Modulo

Abstract : We present a restriction of Resolution modulo where the rewrite rules are such that clauses rewrite to clauses, so that the reduct of a clause needs not be further transformed into clause form. Restricting Resolution modulo in this way requires to extend it in another and distinguish the rules that apply to negative and positive atomic propositions. This method can be seen as a restriction of Equational resolution that mixes clause selection and literal selection restrictions. Unlike many restrictions of Resolution, it is not an instance of Ordered resolution.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Wednesday, August 6, 2014 - 4:25:53 PM
Last modification on : Friday, October 8, 2021 - 4:26:24 PM
Long-term archiving on: : Wednesday, November 26, 2014 - 1:01:07 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Gilles Dowek. Polarized Resolution Modulo. 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS) / Held as Part of World Computer Congress (WCC), Sep 2010, Brisbane, Australia. pp.182-196, ⟨10.1007/978-3-642-15240-5_14⟩. ⟨hal-01054460⟩



Record views


Files downloads