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.
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
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⟩