Pith. sign in

REVIEW 3 major objections 4 minor 40 references

Towards a Certifying Grounder

T0 review · 3 major / 4 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper establishes that a certifying grounder can produce a machine-checkable proof that the grounded CNF is equivalent to the original high-level specification, closing the trust gap between user specification and solver input.

desk verdict A genuinely new piece of the proof-logging story — certifying the grounding step itself — with a clean framework and honest limitations, but the trust anchor is not yet formally pinned down. read the letter →

arxiv 2607.21199 v1 pith:2ARZKMHH submitted 2026-07-23 cs.LO cs.AI

Daimy Van Caudenberg , Alexander Ek , Carlos Cantero , Bart Bogaerts This is my paper · ORCID
classification cs.LOcs.AI
keywords proofloggingcertifyingalgorithmsgroundingmodelexpansionfirst-orderlogicSATSin-equivalencerewriterules
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper argues that the grounding step—the translation of a high-level first-order logic specification into a low-level SAT formula—can be made certifying. It introduces CertiFOX, a framework with a proof format, a certifying grounder, and an independent checker, and claims that every rule application preserves equivalence over all structures extending the input structure. If correct, a successfully checked grounding guarantees that the original theory and the grounded CNF have exactly the same models, so the solver's answer is trustworthy with respect to the user's actual problem. This matters because grounders are complex, bug-prone software, and until now no existing grounder produced a certificate of correctness for its translation. The paper also shows experimentally that the overhead of proof logging and checking is small, making certification practically feasible.

What carries the argument

The central notion is Sin-equivalence: two formulas are equivalent if they have the same models among all structures that extend the input structure Sin. The proof system's rewrite rules, most notably the IQ rule that instantiates a binary quantifier only over domain elements satisfying its guard, are the mechanism that preserves this equivalence. A positioning system identifies the exact subformula each rule targets, and the proof format logs every application; the checker replays these applications and verifies the final theory is syntactically identical to the claimed grounding.

What would settle it

Construct a concrete FOX instance where CheckFOX accepts a GroundFOX proof but the original theory and the reported grounded CNF have different models over some structure extending Sin; for example, exhaustively enumerate all small domains and compare the model sets of T and T′ for every such structure, and any mismatch with an accepted proof refutes the guarantee.

Watch

Extended reading notes

Core claim

The central claim is that CertiFOX closes the trust gap between a user's high-level FOX specification and the solver's low-level input: given an input problem ⟨V, Sin, T⟩, every rule application preserves Sin-equivalence, and if the checker successfully verifies the proof, it guarantees that the original theory T and the grounded theory T′ are Sin-equivalent. The proof system is built from a small set of rewrite rules—instantiation of binary quantifiers, simplification of conjunctions and disjunctions, and evaluation of input predicates—each argued (though not formally proven) to preserve equivalence over all structures extending Sin. The checker replays each logged step and performs a synta

Load-bearing premise

The entire guarantee rests on the unverified meta-theoretic assumption that each rewrite rule in Tables 1 and 2 preserves Sin-equivalence—the paper provides only informal arguments, not formal proofs, and the checker itself is not formally verified.

Editorial extensions

If this is right

  • Declarative solving pipelines can become certified end-to-end, so a solution is guaranteed correct with respect to the user's original specification, not just the solver's input.
  • Grounder bugs can be caught by an independent checker without requiring the grounder itself to be trusted or formally verified.
  • Domain-aware grounding—guards that skip irrelevant ground instances—remains possible while still producing a machine-checkable equivalence proof.
  • Proof checking runs in time linear in the proof size and adds only a small constant-factor overhead over grounding, so certification is practical on realistic benchmarks.
  • The framework provides a foundation for broader certified grounding of richer languages, including arbitrary first-order sentences and cardinality constraints.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the proof system is extended to full first-order logic, the same Sin-equivalence machinery could certify preprocessing steps in other high-level modeling systems, not just FOX grounding.
  • A formally verified checker would shift the trust anchor from the grounder to a small, auditable program; the paper defers this, but the design explicitly aims to make it feasible.
  • The guard-based instantiation rule suggests a general principle: any rewrite that uses input-structure knowledge can be certified as long as it preserves models on all extensions, which may apply to symmetry breaking or other domain-specific simplifications.
  • One testable extension is to generate both the grounded CNF and the original theory in solvable form and check their model sets coincide on small random instances, which would empirically stress-test the informal soundness arguments.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper presents CertiFOX, a prototype framework for certifying the grounding step in first-order logic model expansion (FOX) over finite domains. The framework comprises: (1) a proof format built from a small set of Sin-equivalence-preserving rewrite rules (Tables 1 and 2), (2) GroundFOX, a grounder that translates GNF theories into CNF while logging each rewrite, and (3) CheckFOX, a proof checker that replays the log and checks that the final theory is syntactically identical to the claimed grounding. The intended guarantee is that a successfully checked CertiFOX proof establishes Sin-equivalence between the original FOX specification and the produced CNF, thereby closing the trust gap between a user's high-level specification and the solver's low-level input. The paper also reports experiments on the DIRT benchmark suite showing that GroundFOX is broadly competitive with IDP-Z3 and pyclingo, that proof-logging overhead is small, and that CheckFOX checking overhead is within a small constant factor in most successful runs.

Significance. If fully realized, the CertiFOX approach would fill a real gap in proof logging: while SAT, SMT, MaxSAT, CP, and ASP solvers increasingly emit certificates, the grounding phase has largely escaped certification. The idea of logging grounder rewrites against a fixed, checkable rule set is natural and promising, and the introduction of GNF with guarded binary quantifiers is a reasonable way to make grounding derivations compact and domain-aware. The paper has concrete strengths: the proof rules are standard equivalence-preserving rewrites, the checker is deliberately small, the implementation is released, and the experimental comparison with two mainstream grounding pipelines gives useful evidence of feasibility. However, the central correctness guarantee is not actually delivered as a formal theorem: rule soundness is only argued informally, and CheckFOX itself is not formally verified. As a consequence, the paper's headline claim is currently an architectural promise rather than an established result.

major comments (3)
  1. [Section 3.2, Table 1 (EPRED/EPROP, IQ)] The EPRED/EPROP rules are stated as rewriting P(¯t) to t or f depending on whether Sin |= P(¯t), but no explicit groundness condition is given. If ¯t contains variables bound in the surrounding formula, the side condition Sin |= P(¯t) is not even well-defined, and the rewrite need not preserve Sin-equivalence. Section 3.3 says that GroundFOX applies EPRED only to ground atoms, but the rule definition and the checker semantics in Section 3.4 ("applies the specified rule, and rejects immediately if the rule cannot be applied") do not state that CheckFOX rejects non-ground applications. Since CheckFOX is the trust anchor, an implementation that accepted a non-ground EPRED application would invalidate the paper's headline guarantee. Please add the side condition explicitly (e.g., "¯t is a tuple of ground terms over the input vocabulary") both in Table 1 and in the checker's rule-validation l
  2. [Section 3.2, Definition 4] Sin-equivalence is defined via S |= φ and S |= ψ for structures S extending Sin. This is only meaningful for closed formulas, but the proof rules in Table 1 are applied to arbitrary (sub)formulas, which in a first-order setting may have free variables. The positioning system in Table 3 explicitly allows targeting subformulas under quantifiers, so open formulas do arise. Without a definition of equivalence for open formulas (e.g., for all structures extending Sin and all assignments into their domain), the informal soundness argument for subformula-level rules is not well-founded. Please extend the definition to cover formulas with free variables, or restrict every rule application to closed substitution instances and say so explicitly.
  3. [Section 3.2-3.4 and Abstract] The central claim—"if the checker successfully verifies the proof, it guarantees that the original theory T and the grounded theory T′ are Sin-equivalent"—depends on (i) a meta-theorem that every rule in Tables 1 and 2 preserves Sin-equivalence, and (ii) CheckFOX correctly implementing those rules. The paper explicitly says for (i) "we will not provide a formal proof of this guarantee for each rule. Instead, we provide an informal argument" (Section 3.2), and for (ii) a formally verified checker is deferred to future work (Sections 3.4 and 5). Thus the guarantee advertised in the abstract is not established by the paper. Please either provide formal soundness proofs for the rule set and a precise formal specification of CheckFOX's behavior, or soften the abstract/conclusion to state that the guarantee is conditional on the correctness of CheckFOX and on the meta-theoretic soundness of th
minor comments (4)
  1. [Section 4.2] The text says checking overhead is "within a factor of 2–3 in most cases," but CheckFOX timed out on 3 instances and ran out of memory on 66 of the 505 successfully grounded instances. Please qualify the overhead claim by these failures, or report separate overhead statistics for the instances on which checking completed.
  2. [Section 3.2, paragraph after Example 3] The text says position [0,0] refers to the guard "x ≠ y", but the displayed formula in Example 3 has the guard "y ≠ x" inside ∀y. The notation should be consistent.
  3. [Section 3.4] The sentence "formally verified becomes feasible, which is exactly what makes it a meaningful trust anchor" overstates the current state: the checker is not yet formally verified. Suggest saying that the checker is designed to be amenable to formal verification, and that this is future work.
  4. [Section 3.4] The checker's final check is described as checking that the resulting theory is "syntactically identical" to the claimed grounding. If the checker itself performs any normalization or simplification while replaying, the notion of "syntactic identity" needs to be defined relative to the proof steps; otherwise it is unclear how the comparison works.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the Sin-equivalence guarantee is conditional on an unproven rule-soundness meta-theorem, which is a proof/trust gap, not a definitional reduction.

full rationale

The derivation chain is: GroundFOX logs applications of the rewrite rules in Tables 1 and 2; CheckFOX replays each rule application, targeting the subformula by position and rejecting when the rule cannot be applied, and then checks that the final theory is syntactically identical to the claimed CNF. Semantic equivalence is supposed to follow from soundness of those rewrite rules. None of the rules is defined in terms of the target grounded theory: SNAND/SNOR/STN and TRIVIAL/UNSAT/SPLITC are Boolean/structural rewrite identities; IQ is the finite-domain expansion of the binary-quantifier definition (Definition 1); EPRED/EPROP replace input atoms by their truth values in Sin for ground instances. Thus the certificate does not assume T' as an axiom, and no fitted parameter or imported uniqueness theorem is being renamed as a prediction. The paper's self-citations in the references are related-work and experimental context (e.g., [6,8,25,26,38,39]) and are not load-bearing for the Sin-equivalence claim. The main weaknesses are correctness risks rather than circularity: Section 3.2 explicitly says 'we will not provide a formal proof of this guarantee for each rule' and instead gives an informal argument; Section 5 defers 'a formally verified checker' to future work; the GNF transformation itself is outside the certified pipeline; and the grounder, proof format, and checker are produced by the same research group. The EPRED/EPROP groundness side condition is stated in Section 3.3 but not made explicit in the checker semantics or rule table, which is a potential soundness bug in the trust anchor. These limitations affect assurance, not the structural independence of the derivation, so the circularity score is 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 2 invented entities

The central guarantee rests on standard finite-domain FOL semantics, the GNF guard restriction, informal soundness of the proof rules, and correctness of the unverified CheckFOX implementation; no numeric parameters are fitted.

assumptions (5)
  • standard math Finite-domain FOL semantics and model expansion; structures extending Sin by definition of ≥p.
    Preliminaries Section 2; the prototype only handles finite domains.
  • domain assumption Guards in GNF contain only input vocabulary symbols, so they can be evaluated in Sin during grounding.
    Definition 2/3 and Section 3.1 requirement; the IQ rule depends on it.
  • ad hoc to paper CERTIFOX proof rules (Tables 1–2) preserve Sin-equivalence.
    Section 3.2 states no formal proof is given, only informal arguments; this is the central soundness premise.
  • domain assumption CheckFOX correctly implements the proof system and replay.
    Section 3.4 claims checker is independent and simple, but formal verification is future work (Section 5).
  • standard math Every FOL formula can be transformed into an equisatisfiable GNF formula, possibly using auxiliary symbols.
    Section 3.1 note; needed to motivate the fragment, but no proof is given in the paper.
invented entities (2)
  • Grounding Normal Form (GNF)
    purpose: Restrict input theories so GroundFOX can ground to CNF without auxiliary-symbol introduction; enables guard-based compact grounding.
    New syntactic fragment introduced in Definition 3; not independently evidenced outside the paper; performance/compactness shown on DIRT benchmarks.
  • Sin-equivalence
    purpose: Weaker equivalence notion used to certify correctness relative to the fixed input structure.
    Definition 4; foundational to the proof rules, but is a definition rather than an independently evidenced empirical entity.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Towards a Certifying Grounder." pith.science (2026). https://pith.science/paper/2ARZKMHH

@misc{pith2026260721199,
  author       = {Pith},
  title        = {Pith review of: Towards a Certifying Grounder},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2ARZKMHH}},
  note         = {Machine review of arXiv:2607.21199}
}
read the original abstract

Grounding, the translation of high-level theories into equivalent quantifier-free formulas, is a crucial step in declarative solving, yet it has so far escaped the proof-logging revolution. When this grounding step is not certifying, there is no way of knowing that the obtained solutions actually correspond to the original problem specification, resulting in a trust gap. In this paper, we close the trust gap between the user's high-level specification and the solver's low-level input by introducing a novel certifying grounding framework for first-order logic model expansion (FOX) over finite domains. We present CertiFOX, a framework consisting of: (1) a proof format for grounding derivations, (2) GroundFOX, a certifying grounder operating on theories in Grounding Normal Form (GNF)--a new normal form designed for compact, domain-aware grounding--and (3) CheckFOX, an independent proof checker. Our approach guarantees that the grounder's output is equivalent to the input specification, setting the stage for trustworthy end-to-end certified solving pipelines for declarative languages. Experimental evaluation confirms that CertiFOX is a feasible approach. The GroundFOX grounder is broadly comparable with other grounders, and proof checking with CheckFOX adds overhead within a small constant factor of grounding time.

Figures

Figures reproduced from arXiv: 2607.21199 by the authors.

Figure 1
Figure 1. Architecture of the prototype. 3.1 Grounding Normal Form Our prototype of the CERTIFOX ecosystem is limited to a fragment of FOL in which sentences are ex￾pressed in grounding normal form (GNF). GNF is a normal form that allows grounding to conjunctive normal form (CNF) after quantifier instantiation and basic simplifications (without the need for the in￾troduction of auxiliary symbols by the grounder). By grounding… view at source ↗
Figure 2
Figure 2. Number of instances y with individual completion time ≤ x across grounding pipelines. 1 KiB 32 KiB 1 MiB 32 MiB 1 GiB 32 GiB 1 KiB 32 KiB 1 MiB 32 MiB 1 GiB 32 GiB Proof Log Size Input (FOL) + Output (CNF) Size Benchmark CommonItem−SAT CommonItem−UNSAT CompleteSets−SAT CompleteSets−UNSAT GraphColouring PPM RamseyNumbers stablemarriage [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗
Figure 3
Figure 3. Scatter plot of proof sizes for the different benchmarks. [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

40 extracted references · 23 canonical work pages

  1. [1]

    Gent, Christopher Jefferson, Ian Miguel & Peter Nightingale (2018): Metamorphic Testing of Constraint Solvers

    Özgür Akgün, Ian P. Gent, Christopher Jefferson, Ian Miguel & Peter Nightingale (2018): Metamorphic Testing of Constraint Solvers. In John N. Hooker, editor: Principles and Practice of Constraint Programming - 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings, Lecture Notes in Computer Science 11008, Springer, pp. 727–...

    work page doi:10.1007/978-3-319-98334-9_46 2018

  2. [2]

    Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah & Pascal Schweitzer (2011): An Intro- duction to Certifying Algorithms. it Inf. Technol. 53(6), pp. 287–293, doi:10.1524/itit.2011.0655

    arXiv 2011

  3. [3]

    Theory Pract

    Mario Alviano, Carmine Dodaro, Johannes Klaus Fichte, Markus Hecher, Tobias Philipp & Jakob Rath (2019): Inconsistency Proofs for ASP: The ASP - DRUPE Format. Theory Pract. Log. Program. 19(5-6), pp. 891–907, doi:10.1017/S1471068419000255

    work page doi:10.1017/s1471068419000255 2019

  4. [4]

    Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury & Pascal Fontaine (2020): Scalable Fine- Grained Proofs for Formula Processing. J. Autom. Reason. 64(3), pp. 485–510, doi:10.1007/s10817-018- 09502-y

    work page doi:10.1007/s10817-018- 2020

  5. [5]

    Barrett (2022): Flexible Proof Production in an Industrial-Strength SMT Solver

    Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli & Clark W. Barrett (2022): Flexible Proof Production in an Industrial-Strength SMT Solver. In Jasmin Blanchette, Laura Kovács & Dirk Pattinson, editors: Automated Reasoning ...

    2022

  6. [6]

    Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel & Dieter Vandesande (2023): Certified Core- Guided MaxSAT Solving. In Brigitte Pientka & Cesare Tinelli, editors: Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings , Lecture Notes in Computer Science 14132, Springer, pp. ...

    work page doi:10.1007/978-3-031-38499-8_1 2023

  7. [7]

    In Koenig et al

    Ignace Bleukx, Maarten Flippo, Bart Bogaerts, Emir Demirovic & Tias Guns (2026): Using Certify- ing Constraint Solvers for Generating Step-wise Explanations . In Koenig et al. [28], pp. 14192–14200, doi:10.1609/AAAI.V40I17.38432

    work page doi:10.1609/aaai.v40i17.38432 2026

  8. [8]

    Bart Bogaerts, Stephan Gocht, Ciaran McCreesh & Jakob Nordström (2023): Certified Dominance and Symmetry Breaking for Combinatorial Optimisation . J. Artif. Intell. Res. 77, pp. 1539–1589, doi:10.1613/jair.1.14296

    doi:10.1613/jair.1.14296 2023

Show all 40 references
  1. [9]

    Robert Brummayer & Armin Biere (2009): Fuzzing and Delta-Debugging SMT Solvers . In Ofer Strich- man Bruno Dutertre, editor: Proceedings of the 7th International Workshop on Satisfiability Mod- ulo Theories , SMT ’09, Association for Computing Machinery, New York, NY , USA, p....

    2009

  2. [10]

    In Ofer Strichman & Stefan Szeider, editors:Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010

    Robert Brummayer, Florian Lonsing & Armin Biere (2010): Automated Testing and Debugging of SAT and QBF Solvers. In Ofer Strichman & Stefan Szeider, editors:Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, Jul...

    2010 doi

  3. [11]

    CoRR abs/2202.00343, doi:10.48550/arXiv.2202.00343

    Pierre Carbonnelle, Simon Vandevelde, Joost Vennekens & Marc Denecker (2022): IDP-Z3: a reasoning engine for FO(·). CoRR abs/2202.00343, doi:10.48550/arXiv.2202.00343. arXiv:2202.00343

    2022 doi arXiv

  4. [12]

    Cook, Thorsten Koch, Daniel E

    William J. Cook, Thorsten Koch, Daniel E. Steffy & Kati Wolter (2013): A hybrid branch-and-bound approach for exact rational mixed-integer programming . Math. Program. Comput. 5(3), pp. 305–344, doi:10.1007/s12532-013-0055-6

    2013 doi

  5. [13]

    In Pascal Fontaine & Aaron Stump, editors: PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wrocław, Poland, August 1, 2011 , pp

    David Déharbe, Pascal Fontaine & Bruno Woltzenlogel Paleo (2011): Quantifier Inference Rules for SMT proofs. In Pascal Fontaine & Aaron Stump, editors: PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wrocław, Poland, August 1, 2011 , pp. 33–39. A...

    2011

  6. [14]

    In Laura Barbulescu, Jeremy Frank, Mausam & Stephen F

    Salomé Eriksson, Gabriele Röger & Malte Helmert (2017): Unsolvability Certificates for Classical Plan- ning. In Laura Barbulescu, Jeremy Frank, Mausam & Stephen F. Smith, editors: Proceedings of the Twenty- Seventh International Conference on Automated Planning and Scheduling,...

    2017 doi

  7. [15]

    Maarten Flippo, Konstantin Sidorov, Imko Marijnissen, Jeff Smits & Emir Demirovic (2024): A Multi- Stage Proof Logging Framework to Certify the Correctness of CP Solvers . In Paul Shaw, editor: 30th International Conference on Principles and Practice of Constraint Programming,...

    2024 doi

  8. [16]

    Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Max Ostrowski, Torsten Schaub & Philipp Wanko (2016): Theory Solving Made Easy with Clingo 5. In Manuel Carro, Andy King, Neda Saeedloei & Marina De V os, editors:Technical Communications of the 32nd International Conference o...

    2016 doi

  9. [17]

    In Chitta Baral, Gerhard Brewka & John S

    Martin Gebser, Torsten Schaub & Sven Thiele (2007): GrinGo : A New Grounder for Answer Set Program- ming. In Chitta Baral, Gerhard Brewka & John S. Schlipf, editors: Logic Programming and Nonmonotonic Reasoning, 9th International Conference, LPNMR 2007, Tempe, AZ, USA, May 15-...

    2007 doi

  10. [18]

    Xavier Gillard, Pierre Schaus & Yves Deville (2019): SolverCheck: Declarative Testing of Constraints . In Thomas Schiex & Simon de Givry, editors: Principles and Practice of Constraint Programming - 25th International Conference, CP 2019, Stamford, CT, USA, September 30 - Octo...

    2019 doi

  11. [19]

    In Kuldeep S

    Stephan Gocht, Ruben Martins, Jakob Nordström & Andy Oertel (2022): Certified CNF Translations for Pseudo-Boolean Solving. In Kuldeep S. Meel & Ofer Strichman, editors: 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 20...

    2022 doi

  12. [20]

    Stephan Gocht, Ciaran McCreesh & Jakob Nordström (2022): An Auditable Constraint Programming Solver. In Christine Solnon, editor: 28th International Conference on Principles and Practice of Constraint Program- ming, CP 2022, July 31 to August 8, 2022, Haifa, Israel , LIPIcs 23...

    2022 doi

  13. [21]

    Hunt, Jr

    Marijn Heule, Warren A. Hunt, Jr. & Nathan Wetzler (2013): Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013 , IEEE, pp. 181–188, doi:10.1109/FMCAD.2013.6679408. Available at https://ieeexplo...

    2013

  14. [22]

    Marijn Heule, Martina Seidl & Armin Biere (2014): A Unified Proof System for QBF Preprocessing . In Stéphane Demri, Deepak Kapur & Christoph Weidenbach, editors: Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, V...

    2014 doi

  15. [23]

    Hitarth, Cayden R

    S. Hitarth, Cayden R. Codel, Hanna Lachnitt & Bruno Dutertre (2024): Extending DRAT to SMT. In Nina Narodytska & Philipp Rümmer, editors:Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024, IEEE, pp. 1–11, doi:10.34727/2024/ISBN.978...

    2024 doi

  16. [24]

    Myreen & Jakob Nordström (2024): Certified MaxSAT Preprocessing

    Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen & Jakob Nordström (2024): Certified MaxSAT Preprocessing. In Christoph Benzmüller, Marijn J. H. Heule & Renate A. Schmidt, editors: Automated Reasoning - 12th International Joint Con...

    2024 doi

  17. [25]

    In Koenig et al

    Hannes Ihalainen, Dieter Vandesande, André Schidler, Jeremias Berg, Bart Bogaerts & Matti Järvisalo (2026): Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach . In Koenig et al. [28], pp. 14251–14260, doi:10.1609/AAAI.V40I17.38439

    2026 doi

  18. [26]

    Christoph Jabs, Jeremias Berg, Bart Bogaerts & Matti Järvisalo (2025): Certifying Pareto Optimality in Multi-Objective Maximum Satisfiability. In Arie Gurfinkel & Marijn Heule, editors: Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conf...

    2025

  19. [27]

    In Bernhard Gramlich, Dale Miller & Uli Sattler, editors: Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manch- ester, UK, June 26-29, 2012

    Matti Järvisalo, Marijn Heule & Armin Biere (2012): Inprocessing Rules. In Bernhard Gramlich, Dale Miller & Uli Sattler, editors: Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manch- ester, UK, June 26-29, 2012. Proceedings, Lecture Notes in Computer Sc...

    2012 doi

  20. [28]

    Sven Koenig, Chad Jenkins & Matthew E. Taylor, editors (2026): Fortieth AAAI Conference on Artificial Intelligence, Thirty-Eighth Conference on Innovative Applications of Artificial Intelligence, Sixteenth Sym- posium on Educational Advances in Artificial Intelligence, AAAI 20...

    2026

  21. [29]

    Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan & Marc Vinyals (2025): Practically Feasible Proof Logging for Pseudo-Boolean Optimization

    Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan & Marc Vinyals (2025): Practically Feasible Proof Logging for Pseudo-Boolean Optimization. In Maria Garcia de la Banda, editor: 31st International Conference on Principles and Practice...

    2025 doi

  22. [30]

    Lucas Van Laer, Simon Vandevelde & Joost Vennekens (2025): DIRT: a Literature-Based Benchmark Suite for Grounders. In Giovanni Casini, Besik Dundua & Temur Kutsia, editors:Logics in Artificial Intelligence - 19th European Conference, JELIA 2025, Kutaisi, Georgia, September 1-4...

    2025 doi

  23. [31]

    Manlove & Gregg O’Malley (2014): Paired and Altruistic Kidney Donation in the UK: Algorithms and Experimentation

    David F. Manlove & Gregg O’Malley (2014): Paired and Altruistic Kidney Donation in the UK: Algorithms and Experimentation. ACM J. Exp. Algorithmics 19(1), doi:10.1145/2670129

    2014 doi

  24. [32]

    McConnell, Kurt Mehlhorn, Stefan Näher & Pascal Schweitzer (2011): Certifying algorithms

    Ross M. McConnell, Kurt Mehlhorn, Stefan Näher & Pascal Schweitzer (2011): Certifying algorithms. Com- put. Sci. Rev. 5(2), pp. 119–161, doi:10.1016/j.cosrev.2010.09.009

    2011 doi

  25. [33]

    Michaelis Michael & A. V . Townsend (1995):Binary Quantification Systems. Notre Dame Journal of Formal Logic 36(3), pp. 382–395, doi:10.1305/ndjfl/1040149354

    1995

  26. [34]

    Mitchell & Eugenia Ternovska (2005): A Framework for Representing and Solving NP Search Problems

    David G. Mitchell & Eugenia Ternovska (2005): A Framework for Representing and Solving NP Search Problems. In Manuela M. Veloso & Subbarao Kambhampati, editors: Proceedings, The Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Application...

    2005

  27. [35]

    Nogueira, Marcello Balduccini, Michael Gelfond, Richard Watson & Matthew Barry (2001): An A-Prolog Decision Support System for the Space Shuttle

    Monica L. Nogueira, Marcello Balduccini, Michael Gelfond, Richard Watson & Matthew Barry (2001): An A-Prolog Decision Support System for the Space Shuttle . In I. V . Ramakrishnan, editor: Practical Aspects of Declarative Languages, Third International Symposium, PADL 2001, La...

    2001 doi

  28. [36]

    Barrett & Cesare Tinelli (2022): Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language

    Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett & Cesare Tinelli (2022): Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language . In: Formal Methods in Computer-Aided Design (FMCAD) , pp. 65–74, doi:10.34...

    2022 doi

  29. [37]

    Technical Report B18, Helsinki University of Technology, Finland

    Tommi Syrjänen (1998): Implementation of Local Grounding for Logic Programs with Stable Model Seman- tics. Technical Report B18, Helsinki University of Technology, Finland. 324 Towards a Certifying Grounder

    1998

  30. [38]

    In Koenig et al

    Dieter Vandesande, Jordi Coll & Bart Bogaerts (2026): Certified Branch-and-Bound MaxSAT Solving . In Koenig et al. [28], pp. 14342–14351, doi:10.1609/AAAI.V40I17.38449

    2026 doi

  31. [39]

    Dieter Vandesande, Wolf De Wulf & Bart Bogaerts (2022): QMaxSATpb: A Certified MaxSAT Solver . In Georg Gottlob, Daniela Inclezan & Marco Maratea, editors: Logic Programming and Nonmonotonic Rea- soning - 16th International Conference, LPNMR 2022, Genova, Italy, September 5-9,...

    2022 doi

  32. [40]

    Johan Wittocx, Maarten Mariën & Marc Denecker (2010): Grounding FO and FO(ID) with Bounds. J. Artif. Intell. Res. 38, pp. 223–269, doi:10.1613/jair.2980

    2010 doi

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.