We introduce a new way of composing proofs in rule-based proof systems that generalizes tree-like and dag-like proofs. In the new definition, proofs are directed graphs of derived formulas, in which cycles are allowed as long as every formula is derived at least as many times as it is required as a premise. We call such proofs circular. We show that, for all sets of standard inference rules, circular proofs are sound. We first focus on the circular version of Resolution, and see that it is stronger than Resolution since, as we show, the pigeonhole principle has circular Resolution proofs of polynomial size. Surprisingly, as proof systems for deriving clauses from clauses, Circular Resolution turns out to be equivalent to Sherali-Adams, a proof system for reasoning through polynomial inequalities that has linear programming at its base. As corollaries we get: (1) polynomial-time (LP-based) algorithms that find circular Resolution proofs of constant width, (2) examples that separate circular from dag-like Resolution, such as the pigeonhole principle and its variants, and (3) exponentially hard cases for circular Resolution. Contrary to the case of circular resolution, for Frege we show that circular proofs can be converted into tree-like ones with at most polynomial overhead.

Circular (Yet Sound) Proofs / Atserias, A.; Lauria, M.. - 11628:(2019), pp. 1-18. (Intervento presentato al convegno 22nd International Conference on Theory and Applications of Satisfiability Testing, SAT 2019 tenutosi a Lisbona) [10.1007/978-3-030-24258-9_1].

Circular (Yet Sound) Proofs

Lauria M.
2019

Abstract

We introduce a new way of composing proofs in rule-based proof systems that generalizes tree-like and dag-like proofs. In the new definition, proofs are directed graphs of derived formulas, in which cycles are allowed as long as every formula is derived at least as many times as it is required as a premise. We call such proofs circular. We show that, for all sets of standard inference rules, circular proofs are sound. We first focus on the circular version of Resolution, and see that it is stronger than Resolution since, as we show, the pigeonhole principle has circular Resolution proofs of polynomial size. Surprisingly, as proof systems for deriving clauses from clauses, Circular Resolution turns out to be equivalent to Sherali-Adams, a proof system for reasoning through polynomial inequalities that has linear programming at its base. As corollaries we get: (1) polynomial-time (LP-based) algorithms that find circular Resolution proofs of constant width, (2) examples that separate circular from dag-like Resolution, such as the pigeonhole principle and its variants, and (3) exponentially hard cases for circular Resolution. Contrary to the case of circular resolution, for Frege we show that circular proofs can be converted into tree-like ones with at most polynomial overhead.
2019
22nd International Conference on Theory and Applications of Satisfiability Testing, SAT 2019
logic; proof complexity; resolution; frege; cutting planes
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
Circular (Yet Sound) Proofs / Atserias, A.; Lauria, M.. - 11628:(2019), pp. 1-18. (Intervento presentato al convegno 22nd International Conference on Theory and Applications of Satisfiability Testing, SAT 2019 tenutosi a Lisbona) [10.1007/978-3-030-24258-9_1].
File allegati a questo prodotto
File Dimensione Formato  
Atserias_Circular_2019.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 393.38 kB
Formato Adobe PDF
393.38 kB Adobe PDF   Contatta l'autore

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/1396051
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 14
  • ???jsp.display-item.citation.isi??? ND
social impact