Paper deep dive

Towards a Certifying Grounder

Daimy Van Caudenberg, Alexander Ek, Carlos Cantero, Bart Bogaerts

Year: 2026Venue: arXiv preprintArea: cs.LOType: PreprintEmbeddings: 52

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%

Last extracted: 7/24/2026, 2:49:30 AM

Summary

The paper introduces CertiFOX, a certifying grounding framework for First-Order Logic model expansion (FOX) over finite domains. It addresses the 'trust gap' in declarative solving by ensuring the grounding step produces a proof certificate that can be independently verified. The framework consists of GroundFOX (a certifying grounder operating on Grounding Normal Form), CheckFOX (an independent proof checker), and a novel proof format. Experimental results show that CertiFOX is feasible, with proof checking overhead being small relative to grounding time.

Entities (7)

CertiFOX · framework · 98%CheckFOX · software-component · 95%GroundFOX · software-component · 95%Grounding Normal Form · logical-formalism · 92%FOX · problem-class · 90%Grounding · process · 88%Proof Logging · concept · 85%

Relation Signals (7)

CertiFOX → contains → GroundFOX

confidence 95% · We present CertiFOX, a framework consisting of: ... (2) GroundFOX

CertiFOX → contains → CheckFOX

confidence 95% · We present CertiFOX, a framework consisting of: ... and (3) CheckFOX

GroundFOX → operateson → Grounding Normal Form

confidence 92% · GroundFOX, a certifying grounder operating on theories in Grounding Normal Form (GNF)

GroundFOX → produces → CertiFOX Proof

confidence 90% · During the grounding process, each transformation step is logged in a CERTIFOX proof

CertiFOX → solves → FOX

confidence 90% · introducing a novel certifying grounding framework for first-order logic model expansion (FOX)

CheckFOX → verifies → CertiFOX Proof

confidence 90% · CheckFOX, an independent proof checker... validate the correctness of the grounding process

Grounding → bridges → Trust Gap

confidence 85% · 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

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

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.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

50,988 characters extracted from source content.

Expand or collapse full text

W. Faber, L. Giordano, R. Rocha, V. Santos Costa (Eds.): 42nd International Conference on Logic Programming (ICLP 2026) EPTCS 450, 2026, p. 309–324, doi:10.4204/EPTCS.450.24 © Van Caudenberg, Ek, Cantero, and Bogaerts This work is licensed under the Creative Commons Attribution License. Towards a Certifying Grounder * Daimy Van Caudenberg KU Leuven, Leuven, Belgium daimy.vancaudenberg@kuleuven.be Alexander Ek KU Leuven, Leuven, Belgium ARC Training Centre OPTIMA, Melbourne, Australia alexander.ek@kuleuven.be Carlos Cantero KU Leuven, Leuven, Belgium carlos.cantero@kuleuven.be Bart Bogaerts KU Leuven, Leuven, Belgium Vrije Universiteit Brussel, Brussels, Belgium bart.bogaerts@kuleuven.be 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 ground- ing 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 indepen- dent 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 GROUND- FOX grounder is broadly comparable with other grounders, and proof checking with CHECKFOX adds overhead within a small constant factor of grounding time. 1 Introduction The field of combinatorial search and optimization is concerned with solving problems that are often NP-hard. In several subfields, this is done using declarative specifications in a suitable formal language. Over the past decades, we have witnessed impressive improvements in the richness of the languages, the efficiency of solvers, and their industrial applications. Since some of these applications involve high- value and life-affecting decision-making processes (e.g., validating the correctness of plans for space shuttle operation [35], or matching donors and recipients for kidney transplants [31]), it is of utmost importance that the answers produced by the solvers be reliable. Unfortunately, the reality is different: the constant need for more efficient and advanced algorithms creates an excellent breeding ground for bugs, resulting in numerous reports of bugs in solvers and of solvers outputting faulty answers [9, 10, 27, 12, 1, 18]. The question that naturally arises is how to get stronger guarantees of correctness of a solver. More specifically, if a solver claims that a problem has no solutions, how can we know this is indeed the case? Or if a solver claims a specific solution is optimal, how can we be sure that there are no better solutions? * Funded by the European Union (ERC, CertiFOX, 101122653). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them. 310Towards a Certifying Grounder One successful way to achieve such a guarantee is the use ofcertifying algorithms[2, 32]. In the context of combinatorial search, this is also known as proof logging. The idea is that algorithms (in our case for solving decision or optimization problems) should not just output an answer, but also acertificate (orproof) that this answer is correct. The produced certificate should be sufficiently simple to be verified efficiently by an independent tool, often referred to as theproof checker. This checker is a tool of much lesser complexity than the solver. Indeed, the checker does not need any complicated heuristics or search strategies; its sole job is confirming correctness of the derivations made by the solver. Proof logging has been embraced strongly by the Boolean satisfiability (SAT) community; a wide va- riety of proof formats have been proposed, the most notable and commonly used one being DRAT [21], and proof logging has been mandatory for solvers participating in the annual SAT competition for years. Inspired by this, proof logging is now seeing adoption in other fields of combinatorial optimization, such as satisfiability modulo theories (SMT) [5], (standard and multi-objective) MaxSAT [38, 26], constraint programming [20, 15], classical planning [14] and answer set programming [3], thereby supporting ad- vanced solving techniques [8, 25]. Proofs of this form are not only useful for guaranteeing the correctness of the solver’s answer, but also for debugging and testing solvers [6], and for explainability purposes [7]. In several domains, including constraint programming and answer set programming, users often specify problems in a high-level, human-readable language, which is then translated (by a technique calledgrounding) into a low-level format that a solver can parse. One main limitation of proof logging research so far is that it has focused solely on the solving phase, meaning that the produced certificate only guarantees that the solver’s answer is correct with respect to the input it receives, but not that the input itself is correct with respect to the original problem specification, resulting in atrust gap. The goal of this paper is to bridge this gap. Concretely, we approach this problem from a logical perspective and focus on themodel expansion[34] problems for first-order logic (FOL); in brief, we will write FOX below to refer to first-order logic model expansion. A model expansion problem takes as input a theory in first-order logic, representing domain knowledge, and a structure interpreting a subset of the symbols, representing the concrete instance of the problem at hand. The goal is to expand this input structure to a model of the theory, which represents a solution to the problem. Typically, a FOX problem is solved in two phases: first, the input theory isgroundedto an equivalent quantifier-free theory, and then this grounded theory is solved using a suitable solver (e.g., a SAT solver). In practice, state-of-the-art grounders [40, 37, 17] apply sophisticated optimizations and rewrite rules to handle large domains efficiently, making them highly complex and difficult to verify. ContributionsIn this paper, we present the foundations of the CERTIFOX ecosystem, a certifying framework for the grounding of FOX specifications. The CERTIFOX ecosystem consists of three main components: the CERTIFOX proof format, the GROUNDFOX certifying grounder, and the CHECK- FOX proof checker. We focus on a fragment of first-order logic in which sentences are expressed in grounding normal form(GNF), a new normal form designed to exploit domain knowledge to produce compact groundings. The goal of the CERTIFOX ecosystem is to provide a methodology for the certifi- able grounding of FOX specifications in GNF, closing the trust gap between the user’s specification and the solver’s input. Related WorkProof logging has been studied extensively as an approach to certifying solvers, result- ing in many proof formats such as DRAT for SAT [21]; VeriPB for pseudo-Boolean solving [29, 25], MaxSAT [39, 6], and constraint programming [20]; and eDRAT for SMT solving [23]. By contrast, the grounding phase has received little attention from a verification standpoint. The certification of prepro- D. Van Caudenberg, A. Ek, C. Cantero, and B. Bogaerts311 cessing steps such as translations is the closest analogue to our work: preprocessing rewrites a formula before solving, much as grounding rewrites a high-level theory before solving. Certifying preprocessing steps has been studied for example in the context of verified translations [19], MaxSAT [24], and quan- tified Boolean formulas [22]. SMT is particularly relevant, because its preprocessing also encompasses quantifier instantiation, and dedicated proof rules exist to certify these instantiation steps [13, 4, 36]. Unlike grounding, however, SMT instantiation is non-exhaustive—it produces only enough ground in- stances to satisfy the solver, rather than an equivalent quantifier-free problem. Our work extends these certifying approaches to include the grounding of first-order logic, clos- ing the trust gap between the user’s specification and the solver’s input. This is particularly important in the context of high-level modeling languages, where users rely on the grounder to faithfully trans- late their specifications into a form suitable for solving. IDP-Z3 [11] andCLINGO[16] are high-level modeling systems that perform grounding for FO(·) and ASP respectively; neither currently produces certificates of correctness for their translations, meaning the final solutions can only be trusted insofar as the grounding process can be trusted. Because both systems are highly complex software systems with many optimizations and rewrite rules, it is difficult to fully verify their correctness, and thus there is a risk of bugs leading to incorrect groundings and, by extension, incorrect final solutions. 2 Preliminaries A combinatorial search problem asks whether there is an object, within a finite domain, that satisfies all given constraints. For example, given a CNF formula, the problem of finding a satisfying assignment is a combinatorial search problem. First-Order LogicThese preliminaries are based on [40]. AvocabularyVis a set of predicate and function symbols. Each predicate and function symbol has anarity, which is the number of arguments it takes. We denote predicate (function) symbols with aritynusingP/n(f/n:). A predicate (function) with arity 0 is called aproposition(object) symbol. We assume that every vocabulary contains the propositionstandf, representing truth and falsity, respectively. Atermis a variable or ann-ary function applied tonterms. Anatomis ann-ary predicate applied to nterms. Ifpandqare terms,p=qis also an atom. Next, we define theformulas: • an atom is a formula, • ifφis a formula, then so is¬φ, • ifφandψare formulas, then so areφ⇒ψ,φ⇐ψandφ⇔ψ, • ifφ i is a formula for alli∈1,...,n, then so are V n i=1 φ i and W n i=1 φ i , • ifφis a formula andxis a variable then∀x:φand∃x:φare formulas. Asentenceis a formula without free variables. AtheoryTover vocabularyVis a set of sentences over the symbols ofV. AstructureSover vocabularyVconsists of a domainDand an interpretation for all symbols inV, where forn-ary predicate symbols, the interpretation is a subset ofD n , forn-ary function symbols, the interpretation is a function fromD n toD. We assume that the domainDis finite. A structureSoverVexpandsa structureS ′ overV ′ ⊆Vif they have the same domain andSagrees withS ′ on all symbols inV ′ interpreted byS ′ ; this is denoted usingS≥ p S ′ (here the p indicates that the first structure is more precise than the second). A structureSsatisfiesa sentenceφifSmakes φtrue under the standard semantics of FOL; this is denoted asS|=φ. A structureSis amodelof a theoryTif it satisfies all sentences inT. 312Towards a Certifying Grounder Model ExpansionA model expansion problem is a combinatorial search problem where a structure over a subset of the vocabulary is given (that is, theinput vocabulary), and the goal is to find a structure that expands it to the full vocabulary (which includes theoutput vocabulary) and satisfies a given theory. More formally, a First-Order Logic model expansion problem is a tuple⟨V,S in ,T⟩consisting of: • a vocabularyV=V in ∪V out which is the union of the input and output vocabularies, • a structureS in overV in providing interpretations for input symbols, • a theoryToverV. TheFOL model expansion problem(FOX) consists of finding a structureSsuch that: •S≥ p S in (meaningSexpandsS in ), • andS|=T(meaning it is a model ofT). We illustrate the flexibility of FOX model specifications with two toy examples. Example 1.We now define the pigeonhole problem as a model expansion problem. First, we define the vocabularyV=Pig/1,Hol/1,Sit/2, which contains predicates that allow us to distinguish pigeons from holes, and to assign pigeons to holes. Next, we define the theory: T= ∀p:Pig(p)⇒∃h:Hol(h)∧Sit(p,h). ∀p 1 ,p 2 ,h:(Hol(h)∧Pig(p 1 )∧Pig(p 2 )∧p 1 ̸=p 2 )⇒¬Sit(p 1 ,h)∨¬Sit(p 2 ,h). The sentences ensure that each pigeon sits in a hole and that each hole can contain at most one pigeon. Given the structureS=D=P 1 ,P 2 ,H,Pig=P 1 ,P 2 ,Hol=Hwith fewer holes than pigeons, model expansion of the structureSgiven theoryTfails. Note that forS ′ =D=P 1 ,P 2 ,H,Pig= P 1 ,P 2 ,Hol=P 1 ,H, model expansion succeeds because the theory does not enforce correct typing. Example 2.The goal is to define a model expansion problem that finds a graph containing a node connected to all other nodes. First, we define the vocabularyV=V in ∪V out , where the input vocabu- laryV in =Node/1contains a predicate that represents nodes, and the output vocabulary contains a predicate for edges (V out =Edge/2). Next, we define the theoryTas follows: T= ∃x:Node(x)∧∀y:Node(y)∧y̸=x⇒Edge(x,y). The sentence ensures that there exists a node x such that for all other nodes y, there is an edge from x to y. Model expansion of the structureS=D=Node=N 1 ,N 2 ,N 3 ,N 4 and theoryTwill succeed. For instance,S ′ =D=Node=N 1 ,N 2 ,N 3 ,N 4 , Edge=(N 1 ,N 2 ),(N 1 ,N 3 ),(N 1 ,N 4 ),(N 2 ,N 3 )is a structure that satisfies the theory; indeed, it contains the node N 1 , which is connected to all other nodes. 3CERTIFOX Ecosystem The CERTIFOX ecosystem is a novel methodology for the certifiable grounding of FOX specifications. TheGROUNDFOX groundertakes as input a FOX problem (in a specific normal form defined below), and grounds it to an equivalent CNF formula. During the grounding process, each transformation step is logged in aCERTIFOX proof, producing a proof certificate that can be independently verified. The checker then uses the original FOX formula, the grounded CNF formula, and the proof to validate the correctness of the grounding process. This separation of concerns ensures that bugs cannot compromise soundness, as the checker provides an independent verification layer. The architecture is illustrated in Fig. 1, showing the data flow from input formula through grounding and certification. D. Van Caudenberg, A. Ek, C. Cantero, and B. Bogaerts313 GROUNDFOX Grounder CERTIFOX Proof CHECKFOX Proof Checker ✓/✗ Low-level specification (CNF) High-level specification (FOX) 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 ingrounding 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 directly to CNF, users can leverage the power of certifying SAT solvers without needing an additional translation step. This restriction allows us to focus our efforts on certifying the grounding process itself, as opposed to the translation from the grounded formula to conjunctive normal form. Our normal form is designed to allow for compact grounding by taking advantage of available domain knowledge. This is done by introducingbinaryquantifiers (inspired by [33]), which allow users to defineguardsfor the quantifiers. These quantifiers are calledbinarybecause they take two formulas as arguments: the first is the guard, and the second is the formula being quantified over. Definition 1(Binary Quantifiers).Given formulasφandψ, the binary quantifiers used in GNF are: ∀x[φ(x)]:ψ(x) def =∀x:φ(x)⇒ψ(x) ∃x[φ(x)]:ψ(x) def =∃x:φ(x)∧ψ(x). We callφa guard forψand write Qx:ψ(x)as an abbreviation for Qx[t]:ψ(x), where Q∈∀,∃andt is the symbol for truth. Given a FOX problem⟨V=V in ∪V out ,S in ,T⟩, it is required that guards of the quantifiers inT only contain symbols fromV in , which are interpreted by the user inS in . This allows the grounder to evaluate the guards during the grounding phase, and to skip irrelevant ground instances. We now introduce the grounding normal form (GNF), which uses these binary quantifiers. Definition 2(Grounding Disjunctive Form). •Ifψis an atom or a negated atom, thenψis in grounding disjunctive form. •Ifψandφare in grounding disjunctive form, then(ψ∨φ)is in grounding disjunctive form. •Ifψis in grounding disjunctive form andφis a FO-formula all symbols of which are inV in , then (∃x[φ]:ψ)is in grounding disjunctive form. 314Towards a Certifying Grounder Definition 3(Grounding Normal Form). •Ifψis in grounding disjunctive form, thenψis in grounding normal form (GNF). •Ifψandφare in GNF, then(φ∧ψ)is in GNF. •Ifψis in GNF andφis a FO-formula all symbols of which are inV in , then(∀x[φ]:ψ)is in GNF. Note that every FOL formula can be transformed into an equisatisfiable GNF formula. When the quantifiers in the original formula are ordered in a way that is not compatible with GNF, this transforma- tion may require the introduction of auxiliary symbols. If this is not the case, as in Example 1, then the transformation requires only the definition of binary quantifiers and logical equivalences. We illustrate this translation process by transforming the theory from Example 2 into GNF. Example 3.We transform the theory from Example 2 into GNF. The original sentence is not in GNF because it contains an existentially quantified universal quantifier. We introduce an auxiliary symbol ToAll/1, representing that a node is connected to all other nodes: ∀x:ToAll(x)⇔ ∀y:y̸=x⇒Edge(x,y) . We apply standard logical rewrites and use the definition of binary quantifiers to obtain the following equisatisfiable GNF theory: T=    ∃x:ToAll(x). ∀x:∀y y̸=x :Edge(x,y)∨¬ToAll(x). ∀x:∃y y̸=x :¬Edge(x,y)∨ToAll(x).    3.2CERTIFOX Proof Format The goal of a CERTIFOX proof is to certify that a grounder correctly transformed the FOX problem ⟨V,S in ,T⟩into an equivalent CNF formulaT ′ , by providing a machine-checkable proof of the equiv- alence betweenTandT ′ . The proof format is built on a minimal collection of sound, equivalence- preserving rewrite rules, the most important being the instantiation rules for binary quantifiers. We first discuss the rules of the proof system, and then we argue informally that each rule preserves equivalence (given the input structure), which is the key correctness guarantee of CERTIFOX. Next, we describe the syntax of the proof format, and we illustrate it with an example. CERTIFOX RulesBecause the grounder can exploit the known interpretation of input symbols pro- vided byS in , the proof system is designed to preserve a weaker notion of equivalence, calledS in - equivalence. Definition 4(S in -equivalence).Given a FOX problem⟨V=V in ∪V out ,S in ,T⟩, two formulasφandψ areS in -equivalent, writtenφ≡ S in ψif for every structureSextendingS in , it holds thatSis a model of φif and only if it is a model ofψ(i.e.,∀S≥ p S in :S|=φ⇔S|=ψ). By extension,T≡ S in T ′ means that the theoriesT,T ′ areS in -equivalent, i.e., that they have the same models among the structures that extendS in . The correctness guarantee of the CERTIFOX ecosystem is that given an input problem⟨V,S in ,T⟩, every rule application preservesS in -equivalence at the theory level, meaning that ifTis the theory before applying the rule andT ′ is the theory after applying the rule, thenT≡ S in T ′ . Because most of the rules supported by CERTIFOX are translations of well-known logical equivalences, we will not D. Van Caudenberg, A. Ek, C. Cantero, and B. Bogaerts315 V i=1...n φ i SNAND φ i ̸=ffor alli V i=1...n φ i ̸=t φ i V i=1...n φ i SNAND φ i =ffor somei f W i=1...n φ i SNOR φ i =tfor somei t W i=1...n φ i SNOR φ i ̸=tfor alli W i=1...n φ i ̸=f φ i P( ̄ t)S in |=P( ̄ t) EPRED t P( ̄ t)S in ̸|=P( ̄ t) EPRED f PS in |=P EPROP t PS in ̸|=P EPROP f ∀x[φ(x)]:ψ(x) IQ V v∈D S in |=φ(v) ψ(v) ∃x[φ(x)]:ψ(x) IQ W v∈D S in |=φ(v) ψ(v) ¬t STN f ¬f STN t Table 1: CERTIFOX formula-level proof rules provide a formal proof of this guarantee for each rule. Instead, we provide an informal argument for each rule, which should be sufficient to convince the reader of the soundness of the proof system. Tables 1 and 2 contain an overview of the rules of the CERTIFOX proof system; Table 1 contains rules that apply at the level of a single (sub)formula, while Table 2 contains rules that apply at the level of the whole theory. Table 1 contains several rules that allow for the simplification of formulas, such as SNAND,SNOR, andSTN. They are basic logical equivalences that hence also preserveS in -equivalence. The rulesEPREDandEPROPallow for the interpretation of input predicates and propositions, respec- tively, by replacing them withtorfaccording to their interpretation inS in . Because this interpretation is fixed, performing this replacement preserves all models among the structures that extendS in ; hence it preservesS in -equivalence. The last formula-level rules are the instantiation rules for binary quantifiers (IQ). Concretely, given a formula of the formQx[φ(x)]:ψ(x)withQ∈∀,∃, theIQ-rule instantiates the formula only with valuesvin the domain that satisfy the guardφaccording to the input structure S in . This is a crucial optimization, as it allows the grounder to skip irrelevant ground instances. When taking the definition of binary quantifiers into account, it is not hard to see that this rule also preserves S in -equivalence. Table 2 presents the theory-level rules of the CERTIFOX proof system. Since a theory can be viewed as the conjunction of its formulas, the rules TRIVIAL and UNSAT provide theory-level counterparts of SNAND. Concretely, a formula in the theory that reduces totmay be removed (TRIVIAL), while one that reduces tofallows early termination with unsatisfiability (UNSAT). Note that theUNSAT-rule can be used to show the unsatisfiability of the original problem, as it guarantees that there are no models among the structures that extendS in . The SPLITC rule also operates at the theory level and decomposes a conjunctive formula into its conjuncts. It is easy to see that all of these rules preserveS in -equivalence, as they are all based on well-known logical proof rules. 316Towards a Certifying Grounder T∪t TRIVIAL T T∪f UNSAT ABORT T∪φ 1 ∧...∧φ n SPLITC T∪φ 1 ,...,φ n Table 2: CERTIFOX theory-level proof rules FormulaφPositions ¬φ⟨φ,0⟩=φ φ 1 ◦φ 2 ⟨φ,0⟩=φ 1 (lhs),⟨φ,1⟩=φ 2 (rhs) ⃝(φ 0 ,...,φ n )⟨φ,i⟩=φ i fori∈[0,n] Qx[ψ]:φ⟨φ,0⟩=ψ(guard),⟨φ,1⟩=φ(body) P(t 0 ,...,t n ) ⟨φ,i⟩=t i fori∈[0,n] t 1 =t 2 ⟨φ,0⟩=t 1 ,⟨φ,1⟩=t 2 f(t 0 ,...,t n )⟨φ,i⟩=t i fori∈[0,n] 0-ary predicates and termsNo subformulas or subterms Table 3: The positioning system for referring to subformulas and subterms, where◦∈⇐,⇒,⇔, ⃝∈∧,∨, andQ∈∀,∃. Positioning SystemEach rule application targets a specific (sub)formula using a custom positioning system built around the formula’s syntax tree, ensuring that the proof is unambiguous but brief. The positioning system is crucial for the proof format, as it allows the checker to precisely identify which (sub)formula to apply each rule to. Concretely, a position is a tuple⟨N,P⟩, consisting of a formula name Nand a sequence of indicesP= [i 0 ,i 1 ,...,i n ]. The elementsi j ∈Nare called indices, and they identify a path from the root of that formula’s syntax tree to the subformula to rewrite. A tuple⟨N,P⟩can also be written asN[i 0 ,i 1 ,...,i n ]; a tuple with an empty path is written asN, referring to the formula namedN itself. Using Table 3, we illustrate how this indexing system can be used to refer to specific subformulas and subterms. In the second formula of Example 3 (assuming it is named 2), the position⟨2,[0]⟩refers to the subformula∀ x̸=y : Edge(x,y)∨¬ToAll(x). The position⟨2,[0,0]⟩refers to the guard of the quantifier inside that formula (i.e.,x̸=y), while the position⟨2,[0,1]⟩refers to the body of that quantifier (i.e., Edge(x,y)∨¬ToAll(x)). CERTIFOX SyntaxA CERTIFOX proof consists of three main parts: a header containing version in- formation, the body containing a chronological sequence of applied rewrite rules, and a footer containing identifiers for the obtained grounded formulas. The rewrite rules allow the grounder to log its reasoning in a way that is easy to understand and verify. With the positioning system in place, we can now describe the syntax of the CERTIFOX proof format. The header specifies the version of the proof format and the grounder that produced the proof. After the header, the body of the proof contains a chronological sequence of applied rewrite rules, which together form a complete record of the transformations performed by the grounder. Each line in the proof corresponds to a single rule application, and is logged as in Listing 1, where each rule application specifies the rule name, the position of the (sub)formula to target and forSPLITC, the names of the new formulas added to the theory after splitting. The footer of the proof contains identifiers for the obtained grounded formulas, which can be used by the checker to verify that the final formula is syntactically identical to the claimed grounding. It is logged usingFINAL IDS : <N>, ... <N>, listing the names of the formulas that are present in the final grounded theory in the order they appear in the D. Van Caudenberg, A. Ek, C. Cantero, and B. Bogaerts317 Listing 1: The syntax of CERTIFOX rule applications. // Rules with @ modify the targeted (sub)formula - SNAND, SNOR, STN, EPRED, IQ, UNSAT <rule name> @ <position> // Rules with - delete the targeted formula - TRIVIAL <rule name> - <position> // Rules with -> replace the targeted formula with new formulas in the theory - SPLITC <rule name> <position> -> <position>,<position>,...,<position> theory. If the final grounded theory is empty, this line is logged asFINAL IDS : -. An illustration of a syntactically correct CERTIFOX proof is given in Listing 2. 3.3GROUNDFOX Grounder The GROUNDFOX grounder is a proof-of-concept implementation that demonstrates the feasibility of certifying the grounding process, serving as a testbed for refining the proof format and supported rewrite rules defined in Section 3.2. It takes as input a FOX problem⟨V,S in ,T⟩withTin GNF and produces a CNF formulaT ′ that isS in -equivalent toT, along with a CERTIFOX proof certifying the grounding. After parsing the input using a customANTLR4parser and internalizing the theory as a vector of abstract syntax trees, the grounder processes each sentence in order. Each sentence in GNF is a (possibly nested) universal quantifier over a body in Grounding Disjunctive Form. The grounder appliesIQto instantiate the outermost universal quantifier, restricting the domain to elements satisfying the guard. Next, it appliesSPLITCto split the resulting conjunction into one top-level formula per domain element. Nested universal quantifiers in the body are handled the same way recursively. Each instantiated formula is traversed inside-out. These formulas are now all in Grounding Disjunc- tive Form, so the body is a disjunction of grounding literals, each of which is either a (possibly negated) ground atom or an existentially quantified subformula. First, existential quantifiers are instantiated via IQinto a disjunction of ground literals, after which they are processed identically to the other literals. For each (possibly negated) ground atom,EPREDorEPROPis applied to evaluate the now grounded atom againstS in and replace it withtorfaccordingly; if the atom is negated,STNis applied to flip the result- ing truth value. Once all literals are resolved,SNORcollapses the disjunction, short-circuiting totif any literal is true or droppingfliterals. If at any point a formula simplifies tof, the grounder immediately emitsUNSATand terminates without completing the remaining sentences. If a formula simplifies tot, it is dropped viaTRIVIAL. We illustrate the grounding process with a toy example. Example 4.The goal is to ground the FOX problem⟨V=V in ∪V out ,S in ,T⟩withV in =P/1,Q/1, V out =R/1,T=∀x[P(x)]:R(x)∨∃y:Q(y).andS in =D=1,2,3,P=2,3,Q=2. We illustrate the steps applied by the grounder by walking through the obtained proof in Listing 2.IQ instantiates the universal quantifier only over elements satisfying the guard P(x). AfterSPLITCseparates the two formulas, the existential subformula∃y:Q(y)is instantiated over the full domain by a secondIQ application, andEPREDevaluates each ground atom againstS in . Since Q(2)holds,SNORshort-circuits the disjunction tot, before being dropped viaTRIVIAL. For the remaining formula, the same steps apply. The grounded theory is therefore empty, certified byFINAL IDS : -. 318Towards a Certifying Grounder Listing 2: An illustration of a CERTIFOX proof for grounding. Some steps are omitted for brevity. IQ @ 1 // (1)=(R(2) | ? y : Q(y)) & (R(3) | ? y : Q(y)) SPLITC 1 -> 2,3 //(2) = (R(2) | ? y : Q(y)), (3)=(R(3) | ? y : Q(y)) IQ @ 2[1] // (2)=(R(2) | (Q(1) | Q(2) | Q(3))) EPRED @ 2[1,0] // (2)=(R(2) | (false | Q(2) | Q(3))) EPRED @ 2[1,1] // (2)=(R(2) | (false | true | Q(3))) EPRED @ 2[1,2] // (2)=(R(2) | (false | true | false)) SNOR @ 2[1] // (2)=(R(2) | true) SNOR @ 2 // (2)=true TRIVIAL - 2 // delete (2) // repeat EPRED, SNOR, TRIVIAL for (3) FINAL IDS : - // The grounded theory is empty 3.4CHECKFOX Checker The CHECKFOX checker is a proof-of-concept implementation that demonstrates the feasibility of in- dependently verifying the correctness of the grounding process using the generated CERTIFOX proofs. It takes as input the original FOX problem⟨V,S in ,T⟩, the grounded CNF formulaT ′ produced by the grounder, and the CERTIFOX proof emitted by the grounder. It validates the correctness of the grounding process by replaying each logged transformation step and checking that the final theory is syntactically identical to the claimed grounding. Given that all rules of the CERTIFOX proof system preserveS in -equivalence, if the checker suc- cessfully verifies the proof, it guarantees that the original theoryTand the grounded theoryT ′ are S in -equivalent, which is the key correctness guarantee of CERTIFOX. The checker replays the proof sequentially: for each step, it identifies the target subformula by position, applies the specified rule, and rejects immediately if the rule cannot be applied. If all steps succeed, it verifies that the resulting theory is syntactically identical to the claimed grounding, accepting if they match and rejecting otherwise. Each rule application requires at most a single traversal of the targeted subformula tree, so the checker runs in time linear in the size of the proof (and the formula). Crucially, this means the checker can be kept intentionally simple and small enough that formal verification becomes feasible, which is exactly what makes it a meaningful trust anchor. 4 Experimental Validation We use the DIRT benchmark suite [30] and select all benchmarks that can be translated into GNF without introducing auxiliary predicates, allowing a fair comparison between the different grounders involved. Concretely, the eight problem sets we use are (1) CommonItem-SAT, (2) CommonItem-UNSAT, (3) CompleteSets-SAT, (4) CompleteSets-UNSAT, (5) GraphColouring, (6) PPM, (7) RamseyNumbers, and (8) stablemarriage. For all of these benchmarks, we created a GNF encoding by directly translating (with minimal changes) an existing (IDP) encoding to our syntax. For one of the problems (stablemarriage), there were multiple IDP encodings; here, we used the encoding on which IDP-Z3 was the most efficient. D. Van Caudenberg, A. Ek, C. Cantero, and B. Bogaerts319 0 100 200 300 400 500 10 −3 10 −2 10 −1 10 0 10 1 10 2 10 3 Grounding (s) # Instances Grounding Pipeline pyclingo GroundFOX−nolog GroundFOX+CheckFOX GroundFOX IDP−Z3 Figure 2: Number of instancesywith individual completion time≤xacross grounding pipelines. 1 KiB 32 KiB 1 MiB 32 MiB 1 GiB 32 GiB 1 KiB32 KiB1 MiB32 MiB1 GiB32 GiB Proof Log Size Input (FOL) + Output (CNF) Size Benchmark CommonItem−SAT CommonItem−UNSAT CompleteSets−SAT CompleteSets−UNSAT GraphColouring PPM RamseyNumbers stablemarriage Figure 3: Scatter plot of proof sizes for the different benchmarks. 4.1 Setup Because of time constraints, we could not compare against all available grounders. Instead, we compare only against IDP-Z3 (0.12.0) andPYCLINGO(5.8.0), which are state-of-the-art solving frameworks for problems expressed in FO(·) and ASP, respectively. These frameworks follow a ground-and-solve approach and therefore contain highly optimized grounders. We consider three versions of our tool: 1 the grounder (GROUNDFOX 0.1.0) without proof logging, the grounder with proof logging, the grounder with proof logging and checking (CHECKFOX 0.1.0). Experiments were conducted on an Intel Xeon Platinum 8468 CPU cluster running Rocky Linux 8.10. Each run was executed as a single-core job with 8 GiB RAM, with multiple runs scheduled concurrently across the cluster. Each instance was grounded and then solved with a 1-hour time limit. 1 The source code is available athttps://gitlab.kuleuven.be/krr/software/groundfox-checkfox 320Towards a Certifying Grounder 4.2 Runtime Results First, we compare the runtime of the grounders. Fig. 2 shows grounding runtimes for the benchmark in- stances across grounding pipelines. Compared toPYCLINGOand IDP-Z3, the performance of GROUND- FOX grounder is respectable overall, although it is outperformed byPYCLINGOon all benchmarks and by IDP-Z3 on about half. IDP-Z3 plateaus after solving around 200 instances: it performs particularly well on the PPM benchmark but struggles with the remaining benchmarks. We believe this is because the PPM instances involve a small typed integer domain with arithmetic constraints that the underlying Z3 SMT solver handles efficiently. The plot also shows that the overhead of proof logging is minimal in GROUNDFOX, and the overhead of checking is within a factor of 2–3 in most cases. Interestingly, GROUNDFOX was able to ground most instances given the memory and time limits. In particular,PYCLINGOruns out of memory on 30 instances of PPM and runs out of time on 2 instances of stablemarriage, while GROUNDFOX grounds all stablemarriage instances successfully and runs out of memory on only 4 instances of PPM. We note that the tools are not equally affected by the memory and time constraints. As mentioned, out of a total of 515 instances,PYCLINGOhit the time limit on 2 and the memory limit on 30, while IDP-Z3 timed out on 117 and ran out of memory on 112 instances. GROUNDFOX (with and without proof logging) timed out on 6 and ran out of memory on only 4 instances. CHECKFOX timed out on 3 instances and ran out of memory on 66 of the 505 successfully grounded instances, making it the most memory-intensive step; addressing this remains future work. 4.3 Proof Size Results We are also interested in the size of the generated proofs, as this is an important factor for the feasibility of proof checking. Fig. 3 presents a scatter plot of the proof sizes for the different benchmarks. This figure shows that the proof sizes vary widely across benchmarks, with some proofs being relatively small (a few hundred lines) and others being quite large (millions of lines). This variation in proof size makes sense given the large variation in domains. When comparing the proof size against the size of the input and obtained output, we see that the RamseyNumbers proofs are larger. In the GNF encoding for the RamseyNumbers problems, no guards are used for the quantifiers, which in combination with the deeply nested quantifiers leads to an exponential number of formulas to simplify in the proof. This stands in contrast to the other problem families: IDP is a typed system supporting multi-sorted logic, and types in an IDP encoding translate directly into guards on the quantifiers in the corresponding GNF encoding. RamseyNumbers is the only problem family whose IDP encoding does not use types, and therefore yields unguarded quantifiers in the GNF encoding. 5 Conclusion We presented CERTIFOX, a certifying framework for grounding FOX problems, comprising GROUND- FOX, a certifying grounder for GNF problems producing compact groundings via domain knowledge; the CERTIFOX proof format; and CHECKFOX, an independent proof checker. Experiments show that GROUNDFOX is broadly comparable to IDP-Z3 andPYCLINGO, with negligible proof-logging over- head, while CHECKFOX verifies proofs within a constant factor of grounding time. Future work in- cludes broader language coverage (arbitrary FOL sentences, cardinality constraints), a formally verified checker, and seamless integration into high-level solving pipelines, as well as extending the proof system with more complex reasoning. D. Van Caudenberg, A. Ek, C. Cantero, and B. Bogaerts321 References [1] Ö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 Science11008, Springer, p. 727–736, doi:10.1007/978-3-319-98334-9_46. [2] Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah & Pascal Schweitzer (2011):An Intro- duction to Certifying Algorithms.it Inf. Technol.53(6), p. 287–293, doi:10.1524/itit.2011.0655. [3] 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), p. 891–907, doi:10.1017/S1471068419000255. [4] Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury & Pascal Fontaine (2020):Scalable Fine- Grained Proofs for Formula Processing.J. Autom. Reason.64(3), p. 485–510, doi:10.1007/s10817-018- 09502-y. [5] 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 - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings,Lecture Notes in Computer Science13385, Springer, p. 15–35, doi:10.1007/978-3-031-10769-6_3. [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 Science14132, Springer, p. 1–22, doi:10.1007/978-3-031-38499-8_1. [7] 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], p. 14192–14200, doi:10.1609/AAAI.V40I17.38432. [8] Bart Bogaerts, Stephan Gocht, Ciaran McCreesh & Jakob Nordström (2023):Certified Dominance and Symmetry Breaking for Combinatorial Optimisation.J. Artif. Intell. Res.77, p. 1539–1589, doi:10.1613/jair.1.14296. [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. 1–5, doi:10.1145/1670412.1670413. [10] 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, July 11-14, 2010. Proceedings,Lecture Notes in Computer Science6175, Springer, p. 44–57, doi:10.1007/978-3-642-14186-7_6. [11] Pierre Carbonnelle, Simon Vandevelde, Joost Vennekens & Marc Denecker (2022):IDP-Z3: a reasoning engine for FO(·).CoRRabs/2202.00343, doi:10.48550/arXiv.2202.00343. arXiv:2202.00343. [12] 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), p. 305–344, doi:10.1007/s12532-013-0055-6. [13] 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, p. 33–39. Available athttps:// inria.hal.science/hal-00642535. 322Towards a Certifying Grounder [14] 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, ICAPS 2017, Pittsburgh, Penn- sylvania, USA, June 18-23, 2017, AAAI Press, p. 88–97, doi:10.1609/icaps.v27i1.13818. Available at https://aaai.org/ocs/index.php/ICAPS/ICAPS17/paper/view/15734. [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, CP 2024, September 2- 6, 2024, Girona, Spain,LIPIcs307, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, p. 11:1–11:20, doi:10.4230/LIPICS.CP.2024.11. [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 Vos, editors:Technical Communications of the 32nd International Conference on Logic Programming, ICLP 2016 TCs, October 16-21, 2016, New York City, USA,OASIcs52, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, p. 2:1–2:15, doi:10.4230/OASIcs.ICLP.2016.2. [17] 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-17, 2007, Proceedings, Lecture Notes in Computer Science4483, Springer, p. 266–271, doi:10.1007/978-3-540-72200-7_24. [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 - October 4, 2019, Proceedings, Lecture Notes in Computer Science11802, Springer, p. 565–582, doi:10.1007/978-3-030-30048-7_33. [19] 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, 2022, Haifa, Israel,LIPIcs236, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, p. 16:1–16:25, doi:10.4230/LIPIcs.SAT.2022.16. [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,LIPIcs235, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, p. 25:1–25:18, doi:10.4230/LIPIcs.CP.2022.25. [21] 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, p. 181–188, doi:10.1109/FMCAD.2013.6679408. Available athttps://ieeexplore.ieee.org/ document/6679408/. [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, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings,Lecture Notes in Computer Science8562, Springer, p. 91–106, doi:10.1007/978- 3-319-08587-6_7. [23] 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, p. 1–11, doi:10.34727/2024/ISBN.978-3-85448-065-5_8. [24] 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 Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I,Lecture Notes in Computer Science14739, Springer, p. 396–418, doi:10.1007/978-3-031-63498-7_24. D. Van Caudenberg, A. Ek, C. Cantero, and B. Bogaerts323 [25] 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], p. 14251–14260, doi:10.1609/AAAI.V40I17.38439. [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 Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part I,Lecture Notes in Computer Science15697, Springer, p. 108– 129, doi:10.1007/978-3-031-90653-4_6. [27] 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 Science7364, Springer, p. 355–370, doi:10.1007/978-3-642-31365-3_28. [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 2026, Singapore, January 20-27, 2026. AAAI Press. Available athttps://aaai.org/proceeding/aaai-40-2026/. [29] 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 of Constraint Programming, CP 2025, August 10-15, 2025, Glasgow, Scotland,LIPIcs340, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, p. 21:1–21:27, doi:10.4230/LIPICS.CP.2025.21. [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, Proceedings, Part I,Lecture Notes in Computer Science16093, Springer, p. 343–356, doi:10.1007/978-3-032-04587-4_21. [31] David F. Manlove & Gregg O’Malley (2014):Paired and Altruistic Kidney Donation in the UK: Algorithms and Experimentation.ACM J. Exp. Algorithmics19(1), doi:10.1145/2670129. [32] Ross M. McConnell, Kurt Mehlhorn, Stefan Näher & Pascal Schweitzer (2011):Certifying algorithms.Com- put. Sci. Rev.5(2), p. 119–161, doi:10.1016/j.cosrev.2010.09.009. [33] Michaelis Michael & A. V. Townsend (1995):Binary Quantification Systems.Notre Dame Journal of Formal Logic36(3), p. 382–395, doi:10.1305/ndjfl/1040149354. [34] 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 Applications of Artificial Intelligence Conference, July 9-13, 2005, Pittsburgh, Pennsylvania, USA, AAAI Press / The MIT Press, p. 430–435. Available athttp://w.aaai.org/Library/AAAI/2005/aaai05-068.php. [35] 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, Las Vegas, Nevada, USA, March 11-12, 2001, Proceedings,Lecture Notes in Computer Science1990, Springer, p. 169–183, doi:10.1007/3- 540-45241-9_12. [36] 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), p. 65–74, doi:10.34727/2022/isbn.978-3-85448- 053-2_10. [37] Tommi Syrjänen (1998):Implementation of Local Grounding for Logic Programs with Stable Model Seman- tics. Technical Report B18, Helsinki University of Technology, Finland. 324Towards a Certifying Grounder [38] Dieter Vandesande, Jordi Coll & Bart Bogaerts (2026):Certified Branch-and-Bound MaxSAT Solving. In Koenig et al. [28], p. 14342–14351, doi:10.1609/AAAI.V40I17.38449. [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, Proceedings, Lecture Notes in Computer Science13416, Springer, p. 429–442, doi:10.1007/978-3-031-15707-3_33. [40] Johan Wittocx, Maarten Mariën & Marc Denecker (2010):Grounding FO and FO(ID) with Bounds.J. Artif. Intell. Res.38, p. 223–269, doi:10.1613/jair.2980.

Instant research discovery