Short proofs without interference

TL;DR

This paper introduces a new proof framework inspired by propositional dynamic logic that eliminates interference in SAT proof systems, enabling shorter proofs and more reliable proof checking.

Contribution

It proposes a novel interference-free proof framework based on dynamic logic, maintaining expressive power and advancing decision procedures for proof verification.

Findings

Framework eliminates interference in proof systems

Shorter proofs for SAT inprocessing techniques

Initial decision procedures for proof checking

Abstract

Interference is a phenomenon on proof systems for SAT solving that is both counter-intuitive and bothersome when developing proof-logging techniques. However, all existing proof systems that can produce short proofs for all inprocessing techniques deployed by SAT present this feature. Based on insights from propositional dynamic logic, we propose a framework that eliminates interference while preserving the same expressive power of interference-based proofs. Furthermore, we propose a first building blocks towards RUP-like decision procedures for our dynamic logic-based frameworks, which are essential to developing effective proof checking methods.