Pith. sign in

REVIEW 3 cited by

Alethe: Towards a Generic SMT Proof Format (extended abstract)

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2107.02354 v1 pith:2A2LMLF5 submitted 2021-07-06 cs.LO

Hans-Jörg Schurr (University of Lorraine , CNRS , Inria , LORIA) , Mathias Fleury (Johannes Kepler University Linz) , Haniel Barbosa (Universidade Federal de Minas Gerais) , Pascal Fontaine (University of Liège) This is my paper · ORCID
classification cs.LO
keywords formatfirstotherproofproofssolverstowardsused
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

The first iteration of the proof format used by the SMT solver veriT was presented ten years ago at the first PxTP workshop. Since then the format has matured. veriT proofs are used within multiple applications, and other solvers generate proofs in the same format. We would now like to gather feedback from the community to guide future developments. Towards this, we review the history of the format, present our pragmatic approach to develop the format, and also discuss problems that might arise when other solvers use the format.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Lean-SMT: An SMT tactic for discharging proof goals in Lean

    cs.LO 2025-05 conditional novelty 7.0 of 10

    The paper presents Lean-SMT, a tactic that translates Lean proof goals into SMT-LIB, obtains cvc5 proofs, and reconstructs them as kernel-checked Lean proofs, with promising results on Sledgehammer and SMT-LIB benchmarks.

  2. Certificate-Aware Property-Directed Reachability

    cs.LO 2026-05 conditional novelty 6.0 of 10

    CAPDR guides PDR's blocker, obligation, and pushing choices with a frozen offline-learned ranker, yielding smaller invariants and faster independent checking while keeping the certificate checker as the only trusted c...

  3. SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus

    cs.LO 2025-07 conditional novelty 6.0 of 10

    The paper specifies SC-TPTP, a TPTP-compatible derivation format for sequent calculus proofs, with tools for checking proofs, unfolding high-level steps, and exporting them to Coq.

Pith tools