Pith. sign in

REVIEW 2 cited by

Interactive configurator with FO(.) and IDP-Z3

Not yet reviewed by Pith; the record is open.

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

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

SPECIMEN: schema-true, not a live event

T0 review · schema-true

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

pith:XXXXXXXX · record.json · timestamp

arxiv 2202.00343 v3 pith:TG7W457B submitted 2022-02-01 cs.LO cs.AI

Pierre Carbonnelle , Simon Vandevelde , Joost Vennekens , Marc Denecker This is my paper · ORCID
classification cs.LOcs.AI
keywords problemscomputerconfiguratorconfiguratorsidp-z3interactivereasoningabounds
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

Industry abounds with interactive configuration problems, i.e., constraint solving problems interactively solved by persons with the assistance of a computer. The computer program, called a configurator, needs to perform a variety of reasoning tasks with the (often incomplete) information that the user provides. Imperative programming approaches make such systems difficult to implement and maintain. Knowledge-based configurators have been proposed to help engineers solve such problems, but many challenges remain. We present IDP-Z3, a new reasoning engine for the FO(.) KR language, and we report on its use for building configurators automatically from a knowledge base.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. OpenAlex reports about 4 citations worldwide. Full citation record

  1. Towards a Certifying Grounder

    cs.LO 2026-07 conditional novelty 7.0 of 10

    CertiFOX makes a grounder prove that its low-level CNF output is equivalent to the original high-level first-order logic specification, with an independent checker verifying the proof.

  2. Enhancing Computer Vision with Knowledge: a Rummikub Case Study

    cs.CV 2024-11 conditional novelty 4.0 of 10

    For Rummikub tile recognition, a logical correction step makes a model trained on 30% of the data match the accuracy of a pure neural model trained on 95%.

Pith tools