Polarized Resolution Modulo - Theoretical Computer Science Access content directly
Conference Papers Year : 2010

Polarized Resolution Modulo

Gilles Dowek
  • Function : Author

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.
Fichier principal
Vignette du fichier
03230183.pdf (175.68 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01054460 , version 1 (06-08-2014)

Licence

Attribution

Identifiers

Cite

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⟩
573 View
105 Download

Altmetric

Share

Gmail Facebook X LinkedIn More