PV4 ⊧ cake_lprtakes a proof and checks whether it satisfies linear propagation redundancy expectations

Application domain/field

Proof checking

Type of tool

Proof checker

Expected input

A proof in LPR (Linear Propagation Redundancy)

Expected output

SAT? or VERIFIED UNSAT or resource exhaustion error

Internals

Built on top of CakeML; HOL4 The same paper has a tool to convert PR to LPR

Comments

• LPR is somewhat weaker than PR
• PR generalises RAT (Resolution Asymmetric Tautology)
• RAT is a de facto standard