Trimming Pseudo-Boolean Proofs

Berhan Oumer Adame Bart Bogaerts Benjamin Bogø S. Dold Arthur Gontier Wietze Koops Ciaran McCreesh Matthew J. McIlree Jakob Nordstr¨om Andy Oertel Adrián Rebola-Pardo M. Turnbull

· 0 citations · 93 references

TL;DR

This work presents a proof trimmer for Boolean satisfiability solving, and shows how this technique can be used to reduce proof size and proof checking time for richer combinatorial paradigms.

Semantic Scholar

View source

Similar papers

Preprint Sep 2026

Exact Complexity of the Satisfiability Problem for Strategy Logic

We show that the satisfiability problem for Strategy Logic introduced by Mogavero, Murano, and Vardi is $\Pi^1_\infty$-complete, and, more strongly, computably isomorphic to true second-order arithmetic. The lower bound is established for the next-time Boolean-goal fragment of Strategy Logic. Consequently, Strategy Log...

Tikhon Pshenitsyn · 0 citations

Proof Primitives for Equality Saturation-based Automated Provers

This work presents a proof extraction algorithm for versioned e-graphs, an extension of e-graphs that supports branching reasoning contexts and proof by cases and implements it in Vegie, a lightweight automated inductive theorem prover.

George Zakhour, J. Gabriele, Cesário et al. · 0 citations

2026

A Natively Parallel Proof Framework for Clause-Sharing SAT Solving

PalRUP is introduced – an LRUP -based proof format and a bottleneck-free, decentralized parallel checking procedure that only uses the (parallel) file system and is composed of a set of small, sequential trusted components.

Ruben Götz, Michael Dörr, Dominik Schreiber · International Conference on... · 0 citations

A light-weight proof checker for TSTP refutations

A proof checker called Nörgler is introduced that builds upon and extends the established approach pioneered by GDV and supports checking propositional, (untyped and typed) first-order, and higher-order refutations represented in TSTP.

Melanie Taprogge, H. Sariyanto, Alexander Steen · 1 citation

Review Jul 2026

Verification of Provers and Solvers

This chapter reviews and compares the approaches available, and mentions several successful applications of automatic deduction tools connected to proof assistants using various approaches.

René Thiemann · arXiv.org · 0 citations

Reconstructing SMT Proofs in the λ Π / ≡ -calculus

This work develops a reconstruction pipeline from the Alethe proof format, produced by cvc5, to Lambdapi, a proof assistant for the λ Π / ≡ - calculus, and provides an encoding of the SMT-LIB logic in Lambdapi, certify a substantial fragment of the Alethe inference rules.

Coltellacci Alessio · 0 citations