TLDR
- A theory is not a procedure. IDP treats logic as a declarative description of possible states, rather than an algorithm or one encoded computational task.
- Definitions deserve their own semantics. Rule sets under well-founded semantics express recursive and non-monotone definitions that ordinary first-order logic cannot generally capture.
- The language is deliberately rich. FO(ID,AGG,PF,T) combines first-order logic with definitions, aggregates, partial functions and types.
- One knowledge base supports many inferences. Model expansion, checking, propagation, optimisation, querying, deduction and explanation can reuse the same domain theory.
- Execution is a separate layer. Lua procedures compose inference calls, while preprocessing, grounding and a hybrid solver carry the operational burden beneath the model.
Break the link between describing a domain and prescribing a computation
Kowalski’s procedural reading made Horn-clause logic executable. The IDP chapter keeps logic programming’s declarative achievement: especially rule-based definitions: but refuses to identify a theory with the order of steps used to answer one question.
In a conventional program, domain knowledge is woven into control flow. A loop, data structure and branch may jointly encode facts about scheduling, reachability or configuration. This can support highly tuned execution, yet the knowledge is difficult to inspect independently and usually serves one task. The chapter’s alternative is a knowledge-base system: represent the domain once, then apply generic inferences to it.
An IDP theory is a “bag of information” in the authors’ phrase: a description of the possible states of affairs. It does not say “run model expansion” or “minimise this term”. Those choices belong to the inference and procedural layers. The same course-allocation theory can propagate consequences of a student’s partial choices, generate a complete schedule, minimise conflicts, check a manual revision, answer a query and help explain inconsistency.
This is not a claim that control disappears. Control moves. Generic algorithms implement model expansion and optimisation, while Lua code sequences calls, handles input and output, and composes a workflow. The separation is architectural: declarative components state what the domain permits; an inference method states the logical task; procedural integration determines when and how tasks are invoked.
The chapter also resists making the modelling language weak solely for tractability. Decidability depends on the inference and the input setting. First-order deduction can be undecidable, while finite-domain model expansion is decidable. A rich statement may expose types, functions or symmetries that a lower-level encoding would hide, giving the system more structure to exploit.
Worked example 1 · one timetable, six questions
A university theory states course prerequisites, room capacities, availability and collision rules. A student interface propagates forced choices; an administrator expands a partial structure into schedules; an optimiser reduces clashes; a checker validates a manual edit; a query lists overlaps; an explanation identifies the incompatible constraints. The domain statement remains shared.
Causal probe 1 · if Lua invokes the inferences, is IDP still declarative?
Yes at the theory boundary. The procedure decides which inference to call and how to combine results, but it does not change the denotation of the theory. Declarativity is preserved by keeping domain truth conditions separate from workflow control.
First-order logic, extended where modelling repeatedly needs more
IDP’s base language is written FO(ID,AGG,PF,T): first-order logic plus inductive definitions, aggregates, partial functions and types. Each extension addresses a concrete modelling gap without abandoning model-theoretic meaning.
First-order logic contributes vocabularies of predicate and function symbols, formulas built with Boolean connectives and quantifiers, and structures interpreting those symbols over a domain. A theory is a set of sentences. A two-valued structure is a model when every sentence evaluates true. This familiar centre makes conjunction, disjunction, existence and universality read naturally.
Types make domains explicit. A scheduling vocabulary can distinguish students, instructors, courses, rooms and times. Subtype relations form a hierarchy, typed quantifiers range only over the appropriate domain, and function signatures specify the result type. Besides detecting errors, types shrink the combinations that a grounder must consider.
Partial functions acknowledge that many mappings are not total. A spouse function is undefined for a single person; division is undefined at zero; an action-at-time function may not denote when no action occurs. IDP adopts a relational treatment: an atom containing an undefined direct subterm evaluates false. A modeller who wants a conditional reading must write the condition explicitly.
Aggregates supply cardinality, sum, product, minimum and maximum over set expressions. They can state exactly one assignment, count selected edges or sum costs without an elaborate first-order expansion. The functions remain partial where mathematics demands it: minimum and maximum are undefined on an empty set, and numerical aggregates are undefined on inappropriate or infinite inputs.
Worked example 2 · counting edges
The term #{x y : Edge(x,y)} counts ordered pairs in the edge relation. Passed to optimisation, it ranks models of the graph theory by edge count. The constraint theory still says what connected legal graphs are; the term supplies an objective for a separate inference.
Causal probe 2 · why not encode every extension in plain FO?
Some conveniences could be expanded at considerable cost, but general inductive definitions cannot be captured in ordinary first-order logic because of compactness. Types, aggregates and partial functions also preserve domain structure that a flattened encoding would obscure from readers and solvers.
Unknown is less precise than true or false
Model expansion begins with incomplete information. IDP therefore interprets predicates over three values: certainly true, certainly false and unknown: and orders structures by how much they resolve.
A two-valued predicate partitions its tuples into true and false. A partial predicate adds an unknown region. For takes(student,course), a structure may state that John certainly takes Logic, Bob certainly does not take Mathematics and leave every other pair open. Supplying two of the three regions determines the third.
The precision order places unknown below both true and false. True and false are not ordered by precision relative to one another: each resolves the uncertainty in a different direction. A structure I is no more precise than I′ when every tuple certainly true in I remains certainly true in I′ and every tuple certainly false remains certainly false. A two-valued expansion is maximally precise.
Partial functions use relations over input-output tuples. A certainly true tuple fixes an output; all alternative outputs for that input are then certainly false. A function can also be undefined. These conditions require consistency checks, especially after type-domain autocompletion.
Model expansion searches for two-valued models of the theory that refine the supplied partial structure. Propagation moves in the same precision direction but need not complete the structure: it derives literals shared by all expansions and leaves disputed ones unknown. The distinction is operationally useful. Expansion chooses solutions; propagation reports what every solution already forces.
Worked example 3 · a forced edge and an open edge
In the chapter’s four-node graph, every connected legal expansion includes A→D and D→C. Propagation can mark those edges certainly true. Edge D→B appears in some models and not others, so it remains unknown until a particular expansion is selected.
Causal probe 3 · is unknown halfway between true and false?
Not in the precision order. Unknown contains less information and can be refined in either direction. It is not a probabilistic value of one half, nor a compromise truth value. The order tracks information, not likelihood.
A rule set can mean a construction, not material implication
IDP’s most distinctive construct is the definition. Rules identify defined symbols and open parameters, and the well-founded semantics determines the defined relation from the parameters: even for recursive and suitably non-monotone inductions.
The rule T(a,b) ← E(a,b) plus T(a,b) ← ∃c: T(a,c) ∧ T(c,b) defines transitive closure. E is an open parameter supplied by the surrounding structure; T is the relation being defined. The direction of the arrow marks definitional dependence, not a command to execute the rules in textual order.
For monotone definitions, repeatedly adding supported elements reaches the least fixed point. Non-monotone definitions need more care. The chapter’s even-number example alternates membership using a negative condition. Merely asking for a minimal set satisfying the implications admits unintended sets; an induction order must prevent a negative premise from firing before its dependency has settled.
Well-founded induction operates on partial structures of increasing precision. One refinement derives what rule bodies support; another identifies an unfounded set whose members could become true only by circular self-support and marks them false. All terminal well-founded inductions converge to the same limit. For logic-program-shaped definitions over Herbrand structures, the construction coincides with the familiar well-founded model.
Definitions are separate propositions inside a theory. Two rules in one definition may mutually define p and q; placing them in two definitions changes which symbol is open for each proposition and can change the models. Completion supplies consequences useful to the solver, but it is not always equivalent to the inductive definition. Transitive closure is stronger than its completion.
Worked example 4 · reachability grows from a root
Start with Reachable(A). Whenever Reachable(y) and Edge(y,x) hold, derive Reachable(x). On edges A→D, D→C and C→B, the construction adds D, then C, then B. The result depends on Edge, but the same definition works regardless of which legal Edge relation model expansion chooses.
Causal probe 4 · why not read ← as ordinary implication?
Material implication says only that true bodies require true heads; it does not prohibit unsupported head atoms. A definition says which objects belong to the defined concept through a construction. Well-founded semantics supplies that stronger, directional meaning.
Language, inference and procedure have different jobs
IDP adds a procedural integration tier to the usual knowledge-base pair of representation language and inference engines. This makes logical components first-class inputs to a controllable application workflow.
The language tier stores vocabularies, structures, theories, terms and queries. Its concern is meaning: symbols, partial data, constraints, definitions and objectives. The inference tier supplies general operations such as model expansion, checking, propagation, optimisation, deduction and unsatisfiable-core extraction.
The procedural tier embeds Lua. The system calls main(); the procedure can configure options, select logical components, invoke inference and process results. It may load external data, iterate over cases and assemble reports. Because theories and structures are first-class values, a procedure can build or combine them without rewriting their internal knowledge as control flow.
Modularity appears at both the language and implementation levels. Namespaces organise components produced by different teams. A vocabulary can import another vocabulary or selected symbols. Output vocabularies project models onto symbols of interest, so internal auxiliaries need not make two solutions appear different.
On the inference side, shared grounders, solvers and preprocessors mean an improvement can benefit several operations. The authors present this reuse as a system design objective rather than a guarantee that every inference reduces identically. Some tasks use specialised technology: a definition whose parameters are completely interpreted can be evaluated through XSB rather than sent through general search.
Worked example 5 · a two-line procedure changes the question
Calling modelexpand(T,S) returns models of theory T extending partial structure S. Calling minimize(T,S,t) uses the same T and S but adds an objective term. The declarative components do not acquire procedural meaning; the procedure selects which inference relation to compute.
Causal probe 5 · why call the system Imperative–Declarative Programming?
The name marks composition rather than compromise. Declarative objects retain model-theoretic semantics, while imperative code handles sequencing, data movement and control between inference calls: tasks for which an explicit procedure is often the clearest tool.
Vocabulary names the world; structure supplies data; theory constrains models
The concrete IDP language mirrors the formal separation. A vocabulary declares typed symbols, a structure partially interprets them, a theory states formulas and definitions, a term states an objective, and a procedure invokes an inference.
In the graph example, vocabulary V declares a Node type, Forbidden and Edge relations, the defined Reachable predicate and a Root constant. Structure S supplies four nodes A through D, a set of forbidden ordered pairs and Root=A. It does not interpret Edge; model expansion must choose it. Reachable is not input either, because the theory defines it.
The theory groups the recursive Reachable rules in one definition. A sentence requires every node to be reachable, and another forbids every selected edge listed in Forbidden. Type inference can infer the Node type of variables from argument positions. The resulting statement stays close to “choose a legal directed graph in which everything is reachable from A”.
The structure syntax can assign certainly true, certainly false and unknown tuples separately. User-defined domain identifiers such as A are values, not necessarily constant symbols available inside the theory. Constructed types provide a compact alternative when unique names and domain closure are wanted: a type can be declared as constructed from named constructors.
A procedure sets the number of desired models and calls modelexpand(T,S). The chapter reports 24 models for its graph instance. Adding the cardinality term for Edge and calling minimise returns optimal models at cost three. An output vocabulary can restrict which symbol interpretations distinguish outputs, an important detail when auxiliary relations vary.
Worked example 6 · parameters run “backwards”
A Prolog reader might expect known Edge facts to compute Reachable. Here Reachable is constrained to contain all nodes, while Edge is unknown. Model expansion searches for Edge interpretations whose defined transitive closure satisfies that requirement. The definition describes a relation; it is not tied to one input-output direction.
Causal probe 6 · why keep data out of the theory?
Theory reuse. The reachability definition and constraints can govern another graph merely by supplying another structure. Separating instance interpretation from domain law also lets propagation and expansion preserve exactly the partial facts supplied by the caller.
Expansion finds models; propagation finds what they share
The system’s inferences differ in inputs, outputs and guarantees. Treating them as interchangeable “solver calls” would erase the central knowledge-base claim.
Model expansion accepts a theory and partial structure and returns two-valued models extending that structure. Model checking is the limiting case where the input is already two-valued. Satisfiability checking asks only whether some expansion exists. Optimisation further ranks expansions by a term and reports models at the best value found, with a flag indicating whether optimality was proved.
Query inference evaluates a set expression against a two-valued structure and returns its tuples. Propagation returns a more precise partial structure without discarding any solution. Optimal propagation fixes exactly those atoms having the same truth value in every model, while cheaper methods approximate this ideal.
Deduction asks whether one theory entails another. The implementation described is sound but incomplete: it weakens the IDP theory to first-order logic and invokes SPASS. An answer of true is trustworthy, but failure to prove does not establish non-entailment. Internally, deduction can detect functional dependencies.
Unsatisfiable-core extraction helps explain inconsistency by returning a minimal instantiated theory still lacking an expansion, together with source lines. Definition evaluation can use XSB when all open symbols are interpreted. Linear-time-calculus support adds initialisation and progression for temporal theories. The portfolio makes the knowledge base useful across design, completion, validation and diagnosis.
Worked example 7 · propagation before commitment
In an interactive course selector, the student chooses one module. Propagation marks a prerequisite certainly selected and an overlapping seminar certainly unavailable while leaving unrelated modules unknown. Model expansion later completes the remaining choices. The first step preserves options; the second returns full schedules.
Causal probe 7 · why offer approximate propagation?
The ideal common consequence structure may be as hard to obtain as enumerating or reasoning over all models. Cheaper propagation trades completeness of derived certainties for speed while preserving soundness: it may leave a forced atom unknown, but must not force a disputed one.
Model-expansion laboratory
This laboratory transcribes the four-node graph instance. It exhausts every subset of the seven non-forbidden directed edges, computes Reachable by least fixed point, retains models where all nodes are reachable from A and then answers three different inference-style questions.
The artifact intentionally works over distinct Edge interpretations. It validates the chapter’s 24-model expansion count and cost-three optimum. In minimisation view it shows the distinct optimal edge sets after projection; solver-level enumeration or auxiliary representation can affect how returned structures are listed, so the regression targets semantic models, legality and objective value.
Preserve high-level structure until it can reduce the search
The optimisation workflow preprocesses the theory and structure, grounds the residual problem into ECNF, searches with MINISAT(ID), and post-processes models back into the requested vocabulary.
Preprocessing first checks structural consistency: subtype domains, function uniqueness and totality, and disjoint certainly-true and certainly-false predicate tuples. Type autocompletion can infer missing domains from subtype elements and symbol interpretations, but contradictory inferred data must still be rejected.
An input-star definition whose parameters are already two-valued can be evaluated before search, refining the structure and removing the definition from the theory. Definitions can be split by dependency components so evaluable portions are isolated. Conversely, an output-star definition used only to compute final symbols can be delayed until post-processing.
Functional-dependency detection can replace a relational symbol by a lower-arity function and eliminate a quantifier. First-order symmetry detection identifies interchangeable domain elements before grounding, when the symmetry remains visible. Static symmetry-breaking sentences prevent search from rediscovering equivalent solutions.
The grounder instantiates typed variables top-down. It uses known truth values to simplify formulas and avoids grounding subformulas already decided by the input. Lifted unit propagation derives symbolic bounds before grounding; greater input precision can make the propositional result dramatically smaller. These techniques are not changes to the theory’s meaning. They are semantics-preserving ways to avoid generating irrelevant ground material.
Worked example 8 · simplify before expanding
For ∀x: P(x)∨Q(x), if P(1) is already true, the instance at 1 becomes true without generating Q(1). If Q(3) is certainly false, the instance at 3 becomes P(3). Only undecided combinations reach the solver.
Causal probe 8 · why is richer input often faster?
A more precise structure settles atoms earlier. Grounding can skip satisfied branches, shrink quantifier instantiations and propagate constants. The information reduces the residual choice space before Boolean search begins.
SAT at the core, specialised propagators around it
MINISAT(ID) combines Boolean clause learning with modules for aggregates, definitions and functions. The chapter presents this as a DPLL(T)-style architecture drawing on SAT, constraint programming and answer-set techniques.
The Boolean core is MiniSat. Additional propagators understand constraints that should not be flattened prematurely. A definition module checks completion, detects unfounded sets and validates that a complete assignment is the well-founded model. Function symbols are handled with constraint-programming techniques. Every module must explain its propagation in terms of the current assignment so conflicts can drive learning and backtracking.
Optimisation uses branch and bound. When a model with objective v is found, the solver adds a stricter bound and searches again. The result includes both a model collection and metadata about best cost and proved optimality. That distinction matters when a resource limit interrupts search.
The birthday example illustrates function handling. Age, year of birth, primality and an aggregate over prime factors are stated directly over a domain through 2013. The version described could not ground the theory when uninterpreted functions were disabled because of memory exhaustion; with function support it found 48 solutions quickly, only one with age below 100: 26. This is a reported case, not a general performance bound.
Infinite domains remain difficult. The system may infer finite bounds, retrieve interpretations lazily and let constraints bound an integer function. Lazy grounding, described as under development, interleaves grounding and search so a quantified rule is instantiated only when the search violates the assumptions that allowed delaying it. Model expansion over infinite structures is not thereby made decidable in general.
Worked example 9 · branch and bound
The graph theory first yields any legal connected Edge relation. If it has five edges, the solver adds “edge count < 5”. A later four-edge model tightens the constraint again. Once a three-edge model is found and no model with fewer edges exists, optimality is proved.
Causal probe 9 · why require explanations from propagators?
Clause-learning search must know which current decisions entailed a propagated value or conflict. Explanations translate specialised reasoning back into constraints the Boolean core can learn from, preventing the same failure from recurring under equivalent choices.
A system chapter argues for an architecture, not a universal replacement
The paper combines a semantic proposal, a system design and selected implementation evidence. Keeping those layers separate is essential to reading its contribution fairly.
The semantic claim is that first-order logic enriched with well-founded definitions, aggregates, partial functions and types forms a natural modelling language. The architectural claim is that a knowledge base plus multiple inference methods and procedural integration can reuse domain knowledge across tasks. The implementation claim is that the described IDP3 system realises much of this design through preprocessing, ground-and-solve and hybrid search.
Reported applications include scheduling, planning, verification, configuration, security analysis, interactive configuration and stemmatology. Competition and case-study results suggest useful performance and reduced modelling effort in selected settings. They do not show that IDP outperforms specialised algorithms on every problem; the authors explicitly acknowledge that highly tuned imperative algorithms can be faster.
Versioning needs care. The arXiv identifier dates from 2014, but the primary used here is v3 dated 13 March 2018 and describes the then-current knowledge-base form of IDP3. URLs, options, implementation components and availability statements are historical to that version. Modern descendants should not be inferred from the chapter without separate verification.
The deeper design lesson survives particular tooling. By separating the model from the inference, a system can answer new questions without translating the domain into a new bespoke procedure every time. The cost is transferred to generic reasoning technology, and the modeller still bears responsibility for accurate vocabulary, theory and partial data. Declarative does not mean effortless or automatically correct.
Evidence boundary
The primary is arXiv:1401.6312v3, 48 PDF pages including bibliography. The graph laboratory independently enumerates the exact transcribed four-node constraints but is not an IDP runtime. Performance remarks remain attached to cited historical experiments and configurations. No present-day service availability, API compatibility or benchmark leadership is claimed.
Worked example 10 · a wrong theory gives elegant wrong answers
If a room-capacity constraint accidentally uses < rather than ≤, model expansion may return perfectly valid models of the written theory that reject a just-full room. Propagation, optimisation and checking will consistently reuse the same error. Knowledge reuse magnifies the value of validation: and the cost of a mistaken axiom.
Causal probe 10 · where does expertise go in a knowledge-base system?
From hand-coding a separate algorithm towards formalising the domain, choosing suitable inference, validating outputs and occasionally guiding performance options. The burden changes shape; it is not abolished.
| Claim | Supported status | Boundary |
|---|---|---|
| IDP treats a theory as domain information rather than a procedure. | Core design position in §§1.1 and 1.3. | Lua procedures still control application workflows. |
| Definitions use parametrised well-founded semantics. | Formal treatment in §1.2.5. | Completion is useful but not generally equivalent. |
| One knowledge base supports multiple inference methods. | Architecture and course-management example. | Methods have different cost and completeness properties. |
| Model expansion uses a ground-and-solve workflow. | Detailed implementation in §1.6. | Some definitions use specialised XSB evaluation. |
| IDP reduced modelling effort with limited loss in selected comparisons. | Historical case-study report in §1.7. | Not a universal performance guarantee. |
Twelve retrieval hooks
Scholarly and publication gates
Review A · fidelity, teaching and evidential fairness
The companion was checked against all 48 pages of arXiv:1401.6312v3, including the Kowalski contrast; definitions as the informal semantics of rules; the knowledge-base hypothesis; IDP2-to-IDP3 history; FO, partial structures and both precision orders; partial functions; arithmetic and aggregates; well-founded induction; multiple definitions and completion; types; the three-tier architecture; the university application; concrete vocabulary, structure, theory, procedure and term syntax; constructed types, namespaces and output vocabularies; the inference portfolio; optimisation internals; structure checks; input- and output-star definitions; functional dependency and symmetry detection; grounding, simplification, lifted propagation and hybrid search; workflow controls; infinity and lazy grounding; historical applications; related systems; and the conclusion.
Fidelity review passed. The theory is not described as executable, while procedural integration remains explicit. Unknown is ordered by precision, not probability. Definitions are not reduced to implications or completion. The well-founded construction includes both derivation and unfounded-set refinements. Model expansion, propagation, checking, querying, deduction and minimisation are kept distinct. The deduction implementation’s incompleteness and the limits of infinite-domain reasoning are retained. The chapter’s historical availability and performance claims are not presented as current guarantees.
Teaching review passed. Ten worked examples and ten causal probes cover separation of concerns, language extensions, partiality, inductive semantics, components, bidirectional model use, inference choice, preprocessing, hybrid search and model validation. Ten figures encode different causal structures. The graph laboratory independently enumerates 128 edge candidates, reproduces 24 satisfying models, verifies every fixed-point closure and forbidden-edge constraint, and establishes a minimum edge cost of three.
Review B · language, accessibility, responsive layout and execution
The prose was reviewed for hype, solver anthropomorphism, vague authority, false present-tense claims, unsupported causal performance claims and repetitive AI-telltale phrasing. British English is consistent. Every figure has a unique title, description, caption and source note. Shape, text and position carry meaning beyond colour. Animation is decorative and disabled when reduced motion is requested. The document includes a skip link, ordered heading structure, labelled native controls, a live laboratory region and headed data tables.
Responsive review covers 1440, 768 and 390 pixels. The hero, orientation grid, columns, all diagrams, laboratory, evidence ledger, memory studio and sequence navigation collapse without viewport overflow; wide tables remain independently scrollable. The executable review evaluates all 128 candidate graphs on every run. Three regression gates must pass: exactly 24 expansions satisfy the transcribed theory; every retained model contains no forbidden edge and reaches all nodes from A; and optimisation plus propagation identify cost three and the shared edges A→D and D→C.
From a planning language to a general inference-bearing theory
Paper 0103 made knowledge states and defaults first-class in a specialised planning language. Paper 0104 broadens the ambition. IDP’s partial structures hold incomplete information, but the theory need not describe action at all. First-order constraints and well-founded definitions support many domains, and inference methods decide whether to complete, propagate, optimise, check or explain.
Paper 0105 moves back towards planning through Zhou, Barták and Dovier’s account of planning as tabled logic programming. The next work asks how tabling, constraints and state transitions can make a logic programme perform planning efficiently. The canon therefore alternates between declarative separation and operational techniques for exploiting logical structure.
Sources and audit trail
- De Cat, B., Bogaerts, B., Bruynooghe, M., Janssens, G., & Denecker, M. (2018 version). “Predicate Logic as a Modelling Language: The IDP System.” arXiv:1401.6312v3. Primary 48-page source; initially deposited in 2014.
- Kowalski, R. (1974). “Predicate Logic as Programming Language.” IFIP Congress, 569–574. Historical procedural/declarative point of departure used by the primary.
- Denecker, M., & Ternovska, E. (2008). “A Logic of Nonmonotone Inductive Definitions.” ACM Transactions on Computational Logic, 9(2). Formal FO(ID) foundation cited by the primary.
- Van Gelder, A., Ross, K. A., & Schlipf, J. S. (1991). “The Well-Founded Semantics for General Logic Programs.” Journal of the ACM, 38(3), 620–650. Semantic foundation for rule-based definitions.
- Mitchell, D. G., & Ternovska, E. (2005). “A Framework for Representing and Solving NP Search Problems.” AAAI, 430–435. Model-expansion framing adopted by IDP.
- Wittocx, J., Mariën, M., & Denecker, M. (2010). “Grounding FO and FO(ID) with Bounds.” Journal of Artificial Intelligence Research, 38, 223–269. Bound-based grounding work used in preprocessing.
- De Cat, B., Bogaerts, B., Bruynooghe, M., & Denecker, M. (2013). “Predicate Logic as a Modelling Language: Modelling and Solving Some Machine Learning and Data Mining Problems with IDP3.” Earlier system context and solving approach cited in the primary bibliography.
What ships with Paper 0104
Title: When one theory answers many questions: De Cat et al.’s IDP system. Standfirst: A visual and executable reconstruction of theories as models, FO(ID,AGG,PF,T), partial structures, well-founded definitions, the three-tier knowledge-base architecture, reusable inference, ground-and-solve and hybrid propagation. Search terms: IDP system, FO(ID), predicate logic, modelling language, knowledge base system, model expansion, well-founded semantics, inductive definitions, constraint programming. Demonstration: a complete 128-candidate graph model-expansion oracle reproducing the primary’s 24-model count, propagation backbone and minimum edge cost. Accessibility promise: ten titled and described SVG figures, reduced-motion support, labelled controls, keyboard operation and responsive layouts.