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

https://hal.inria.fr/hal-01054460
Contributor : Hal Ifip <>
Submitted on : Wednesday, August 6, 2014 - 4:25:53 PM
Last modification on : Tuesday, March 17, 2020 - 2:56:02 AM
Long-term archiving on: : Wednesday, November 26, 2014 - 1:01:07 AM

File

03230183.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

975

Files downloads

343