Resolution is cut-free (Q972424): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1007/s10817-009-9153-6 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2096711734 / rank | |||
Normal rank |
Revision as of 23:44, 19 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Resolution is cut-free |
scientific article |
Statements
Resolution is cut-free (English)
0 references
26 May 2010
0 references
The paper proves through syntactic translation that the extension of the resolution proof system to deduction modulo is equivalent to the cut-free fragment of the sequent calculus modulo. The resolution method in deduction modulo, called ENAR, is proved to be sound with respect to the cut-free fragment of sequent calculus. However, in order to prove completeness of ENAR with respect to the original sequent calculus, extra assumptions are needed. Due to the expressiveness of deduction modulo, the results obtained in this paper can be applied to higher-order resolution, Peano arithmetic and Zermelo set theory.
0 references
classical sequent calculus
0 references
cut-free
0 references
cut rule
0 references
deduction modulo
0 references
ENAR
0 references
resolution
0 references
rewriting
0 references
Skolemization
0 references
Skolem theorem
0 references