Pith. sign in

REVIEW 3 major objections 5 minor 50 references

SAT-Based Bounded Fitting for the Description Logic ALC

T0 review · 3 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read Finding a smallest ALC concept that separates given positive from negative examples is NP-complete for every fragment containing an existential or universal quantifier, even with a single example of each kind, and efficient PAC learning…

desk verdict The main NP-hardness proof has a real gap in the normalization step; the paper is still worth serious review, but the theorem is not established as written. read the letter →

arxiv 2507.21752 v1 pith:EKMOVLRY submitted 2025-07-29 cs.AI

Maurice Funk , Jean Christoph Jung , Tom Voellmer This is my paper · ORCID
classification cs.AI
keywords descriptionlogicALCboundedfittingsize-restrictedNP-completenessPAClearningSATsolvingconceptsyntacticfragments
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 studies bounded fitting for the description logic ALC (class expressions built from conjunction, disjunction, negation, and existential or universal role restrictions): given positive and negative examples, find the smallest concept that separates them. Its main theorem is that this size-restricted fitting problem is NP-complete for ALC and for every syntactic fragment containing an existential or universal restriction, and hardness already occurs with a single positive and a single negative example. It also shows that no such fragment admits an efficient PAC learning algorithm unless $\mathrm{NP}=\mathrm{RP}$ or RSA-style encryption can be inverted in polynomial time, and that algorithms which always return the most specific, most general, or minimal-quantifier-depth fitting concept are not sample-efficient, with two exceptions. On the constructive side, it reports a SAT-based implementation with encoding optimizations and an approximation scheme, and gives experiments in which it finds exact fits quickly and matches or exceeds existing concept-learning tools in accuracy. The practical upshot is that exact minimal-concept learning is computationally hard in the worst case, yet feasible enough for real learning tasks.

What carries the argument

Three mechanisms carry the argument. The first is a reduction from Hitting Set: from a collection of sets $S_1,\dots,S_m$ and a bound $k$, the proof builds two example interpretations $I$ and $J$ made of $r$-paths of length $n$ with $s$-detours that encode which indices each set contains, plus a sink $c$; a fitting concept of size $k' = n+k+2$ exists exactly when a hitting set of size $k$ exists, because any fitting concept must follow one path shape per index and mark the chosen hitting-set elements. The second is the duality lemma: replacing conjunction with disjunction, existential with universal restrictions, and complementing concept-name extensions in the examples transfers fitting problems between dual fragments, so hardness and sample-complexity results for existential fragments automatically apply to universal fragments. The third is the SAT encoding: Boolean variables represent syntax-tree node labels, successor pointers, and whether each node's concept holds at each domain element; clauses enforce well-formed syntax trees and evaluate them over the example interpretation, and the fitting condition is a conjunction of positive and negative literals. The optimizations replace per-concept-name clauses with type variables and canonicalize syntax-tree topologies to break symmetries in the search space.

What would settle it

Build the two example interpretations from the reduction for a small Hitting Set instance, then exhaustively enumerate all ALC concepts over the signature $\{r,s,A\}$ of size at most $n+k+2$. If any concept fits the positive and negative examples yet is not equivalent to a concept of the form $\exists r.w.A$ with $w\in\{r,ss\}^n$ and at most $k$ occurrences of $ss$, the normalization step underlying Proposition 1 is false and the NP-hardness proof collapses.

Watch

Extended reading notes

Core claim

The central discovery is Theorem 1: for every set $O$ of ALC constructors that contains at least one of $\exists$ or $\forall$, size-restricted fitting for the fragment $L(O)$ is NP-complete. The hardness direction, Proposition 1, is stronger: it holds already for exactly one positive and one negative example, over a signature with two role names and one concept name, and the reduction uses only existential restrictions even when the fragment in question has more constructors. The paper further proves that no fragment $L(O)$ with an existential or universal quantifier admits an efficient PAC learning algorithm under standard assumptions ($\mathrm{NP} = \mathrm{RP}$ when the fragment lacks either conjunction or disjunction; otherwise polynomial-time inversion of RSA-style encryption), and that fitting algorithms returning most specific, most general, or minimal-quantifier-depth concepts are not sample-efficient, except that bounded fitting for $L(\{\exists,\sqcup\})$ is most specific and for $L(\{\forall,\sqcap\})$ is most general. The implementation contribution is a SAT encoding of syntax trees and their evaluation over a finite interpretation, with type-based clause reduction and syntax-tree-topology symmetry breaking, plus an approximation scheme that maximizes example coverage when no exact fit exists.

Load-bearing premise

The load-bearing premise is that every small concept fitting the two constructed examples can be rewritten, without growing, into the exact path-shaped formula that encodes a hitting set; this rewriting relies on the roles being deterministic functions everywhere except at the starting points and on any subconcept satisfied in the sink also being satisfied throughout the negative example.

Editorial extensions

If this is right

  • No polynomial-time algorithm can solve size-restricted fitting for any quantifier-containing fragment unless $\mathrm{P}=\mathrm{NP}$, so bounded fitting must rely on SAT solvers or other backtracking methods.
  • The one-positive-one-negative hardness means the difficulty is inherent to choosing the right concept shape, not to gathering many examples.
  • The duality lemma transfers every complexity and sample-complexity result between existential and universal fragments, making results for existential fragments immediately available for their dual universal fragments.
  • Unless $\mathrm{NP}=\mathrm{RP}$ and RSA-style encryption is secure, no ALC fragment with an existential or universal quantifier has an efficient PAC learning algorithm; bounded fitting's sample guarantees do not come with polynomial runtime.
  • For most fragments, algorithms that always return the most specific, most general, or minimal-quantifier-depth fitting concept are not sample-efficient; the exceptions are exactly the fragments where bounded fitting is the most-specific learner ($L(\{\exists,\sqcup\})$) or the most-general learner ($L(\{\forall,\sqcap\})$).

Reading between the lines

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

  • Editorial inference: the same path-and-detour gadget could give NP-completeness for bounded fitting in richer description logics with inverse roles or number restrictions, since the gadget uses only two functional roles and one concept name.
  • Editorial inference: the type-based clause reduction suggests that on knowledge bases with few distinct types relative to individuals, SAT-based bounded fitting may scale to much larger data instances than reported; a direct test would fix the type count and grow the domain size.
  • Editorial inference: the sample-efficiency results imply that concept-learning tools that gravitate toward logically extreme concepts (most specific or most general) may be systematically over- or under-generalizing; a minimal-size objective is a more conservative inductive bias even though computing it is NP-hard.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper studies bounded fitting for ALC and its syntactic fragments L(O). The decision problem is size-restricted fitting: given positive and negative examples and a size bound k, is there an L(O) concept of size at most k separating the examples. The main theoretical result is Theorem 1, NP-completeness for every O containing ∃ or ∀, even for one positive and one negative example over a fixed signature of two roles and one concept name. The hardness proof reduces Hitting Set to fitting and includes a normalization argument in Appendix B intended to show that any fitting ALC concept of bounded size can be brought into a pure existential form. The paper also gives PAC lower bounds (Theorems 2 and 3), proves that some natural fitting algorithms are not sample-efficient, and presents a SAT-based implementation with optimizations and experiments on SML benchmarks. The implementation is released.

Significance. If Theorem 1 is correct, the paper makes a strong contribution: it settles the complexity of size-restricted fitting for all quantifier-containing ALC fragments, with a surprisingly strong hardness regime (singleton sample, fixed signature), and it provides a usable SAT-based tool. The PAC results and the discussion of most-specific/most-general algorithms are also valuable. The released implementation and reproducible benchmark setup are credit-worthy. However, the central hardness proof currently contains a real gap, and some transfer arguments in the PAC section are not fully justified, so the paper cannot be accepted in its present form.

major comments (3)
  1. [Appendix B, final claim in the proof of Proposition 1] In the last claim of the proof of Proposition 1 (Appendix B), the case d = a_ℓ replaces D_i = ∃r.F1 ⊓ ∃s.F2 by ∃s.∃s.F1 and justifies Property 2 by saying that all elements of R_{w_i}(J,b) 'do not satisfy ∃s.∃s.F1, by the assumption that they do not satisfy ∃r.F1 ⊓ ∃s.F2.' This inference is invalid: an element can fail the conjunction by failing only the ∃s.F2 conjunct. A concrete witness within the size bound is obtained for S = {{1},{2},{3}} (n = k = 3, k' = 8). The concept C = ∃r.∃s.∃s.(∃r.⊤ ⊓ ∃s.A) has size 8 and fits (I,a) and (J,b): after the prefix rss the witness in I is a_1, while R_{rss}(J,b) = {c, b_{2,1}, b_{3,1}}; each of these elements fails ∃r.⊤ ⊓ ∃s.A (the ∃s.A conjunct fails), yet each satisfies ∃s.∃s.⊤. The claimed replacement yields ∃r.∃s.∃s.∃s.∃s.⊤, which is satisfied at b, so Property 2 is not preserved. Since this normalization is exactly the step that extracts a pure L({∃}) fitting from which a hitting set is read off, the proof of (iii)⇒(i), and hence of Theorem 1, is not established as written.
  2. [Section 4, proof of Theorem 2] The proof of Point 1 says that Lemma 6 proves NP-hardness of fitting for L({∀}), L({∀,⊓}), and L({∀,∃,⊓}), and that 'Applying Lemma 1 then yields the same lower bounds for all other fragments from Point 1.' This does not cover fragments containing negation, such as L({∀,¬}) and L({∃,∀}), nor their duals. NP-hardness for a sublanguage does not automatically transfer to a superlanguage, because additional constructors can only make fitting easier. The authors should either extend Lemma 6 to all fragments covered by Point 1 or spell out the additional argument.
  3. [Section 4, proof of Theorem 3] Point 1 is said to follow from [10, Theorem 6] for every fragment containing EL, and Point 2 is proved for L({∃,⊔}), L({∃,⊔,⊓}), and L({∃,∀,⊓}). The parenthetical remark that adding negation to these operator sets leads to full ALC does not transfer the lower bounds to full ALC: an algorithm that returns a most specific (or most general) fitting in the larger language may return a concept outside the subfragment, and the uniqueness/most-general arguments in Lemmas 3, 7, and 8 are stated only for the subfragments. The full-ALC cases of Theorem 3 therefore need an explicit proof or a precise reduction.
minor comments (5)
  1. [Section 2, definition of 'fits'] The text 'a ∈ C^I for each (I, a) ∈ C' should read '∈ P'.
  2. [Section 5, formula for φ1] The clause 'xi,⊓ → W i<ℓ<k v2,i,ℓ' appears to use the undefined variable v2,i,ℓ; it should be y2,i,ℓ.
  3. [Appendix C, Lemma 7] The phrase 'returns always a most general' should be 'always returns a most general'.
  4. [Appendix B, Equation (7)] The expression 'Qℓ−1 i=0 (N − i)' should be written as a product \(\prod_{i=0}^{\ell-1}(N-i)\).
  5. [Table 1] The entry '3.2, ±1.03' contains a stray comma, and 'Nctrer' appears to be a typo for the benchmark name.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the NP-completeness proof is self-contained, and the cited prior work is used as parameter-free supporting lemmas rather than as a re-import of the target results.

full rationale

The central claim, Theorem 1, is established by an explicit reduction from Hitting Set. The forward direction constructs an L({∃}) concept from a hitting set, and the reverse direction normalizes an arbitrary fitting ALC concept into the required shape using structural properties of the constructed interpretations (totality and functionality of r and s away from the roots, single positive and negative examples to eliminate ⊔ and ⊓). Neither direction fits a parameter to the answer nor defines a concept in terms of the fitting relation, so the hardness proof is not circular by construction. Lemma 1, which transfers hardness to universal fragments, is proved by structural induction and does not presuppose the theorem. In Section 4, the paper does rely on its own prior work: Theorem 4 on simulation duals from [9] and the EL base-case claims from [10] in the proofs of Lemmas 7 and 8. These citations have overlapping authors with the present paper and are load-bearing for the non-sample-efficiency results. However, they are parameter-free mathematical statements with explicitly stated assumptions that do not include the target results; the paper supplies the new reduction from the additional fragments to those EL facts. They therefore function as prior evidence, not as a re-importation of the conclusion being proved, and do not make the derivation circular. The algorithm evaluation similarly contains no fitted-input-called-prediction step: handcrafted concepts are used to generate benchmark examples, and accuracy is measured on held-out labels. A reviewer might question the soundness of the size-preserving normalization in Appendix B, but that is a potential correctness gap in the proof, not a circular dependency between input and output, so it does not affect the circularity score.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

The theoretical core is a set of proofs, so the ledger lists the external theorems and standard assumptions the proofs import. The only free parameter is an implementation-level tuning constant for symmetry breaking. No new entities are postulated.

free parameters (1)
  • topology prefix threshold = 10 nodes
    Empirically determined cap for syntax tree topology symmetry breaking in the SAT encoding (Section 5.1); higher values slowed solving on the benchmarks. This affects runtime, not the complexity theorems.
assumptions (4)
  • standard math Pitt-Valiant theorem (from [31]): efficient PAC learnability implies the fitting problem is in RP for classes with polynomial-size fitting and polynomial-time evaluation.
    Used in Corollary 2 and Theorem 2 to convert fitting hardness into conditional non-learnability.
  • domain assumption Complexity and cryptographic assumptions: NP ≠ RP and RSA encryption is not polynomial-time invertible.
    Theorem 2 is conditional on these standard assumptions.
  • domain assumption Simulation dual theorem from [9, Theorem 4]: every EL concept C has a simulation dual of size at most 3|Σ|∥C∥², computable in polynomial time.
    Imported from the authors' prior work and used to construct negative examples in Lemmas 7 and 8.
  • domain assumption EL-specific lower bounds from [10, Theorem 6] and [10, Theorem 3/7] are used as black boxes for the sample-efficiency lower bounds in Theorem 3.
    The paper extends these proofs to ALC fragments, but the original results are not reproved in the appendix.

how reviews work

0 comments
Cite this review

Pith. "Pith review of SAT-Based Bounded Fitting for the Description Logic ALC." pith.science (2026). https://pith.science/paper/EKMOVLRY

@misc{pith2026250721752,
  author       = {Pith},
  title        = {Pith review of: SAT-Based Bounded Fitting for the Description Logic ALC},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EKMOVLRY}},
  note         = {Machine review of arXiv:2507.21752}
}
read the original abstract

Bounded fitting is a general paradigm for learning logical formulas from positive and negative data examples, that has received considerable interest recently. We investigate bounded fitting for the description logic ALC and its syntactic fragments. We show that the underlying size-restricted fitting problem is NP-complete for all studied fragments, even in the special case of a single positive and a single negative example. By design, bounded fitting comes with probabilistic guarantees in Valiant's PAC learning framework. In contrast, we show that other classes of algorithms for learning ALC concepts do not provide such guarantees. Finally, we present an implementation of bounded fitting in ALC and its fragments based on a SAT solver. We discuss optimizations and compare our implementation to other concept learning tools.

Figures

Figures reproduced from arXiv: 2507.21752 by the authors.

Figure 1
Figure 1. Example for size-restricted fitting interpretation IΣ is obtained by complementing the interpretation of the concept names in Σ, that is, ∆IΣ = ∆I , A IΣ = ( ∆I \ AI if A ∈ NC ∩ Σ, AI if A ∈ NC \ Σ, and keeping the interpretation of the role names, that is, r IΣ = r I , for all r ∈ NR. One can then show inductively that the following duality is satisfied for all signatures Σ, ALC concepts C with signature contained … view at source ↗
Figure 2
Figure 2. Example of the interpretations I and J used in the reduction. We start with (i)⇒(ii). Let H be a hitting set for S = {S1, . . . , Sm} with |H| = k. We inductively define concepts Ci , for i = 0, . . . , n, by setting C0 = A and Ci = ( ∃r.Ci−1 if n − i + 1 ∈/ H ∃s.∃s.Ci−1 otherwise, (3) for 1 ≤ i ≤ n. Thus, ∥Cn∥ = n + |H| + 1 and therefore ∥∃r.Cn∥ = n + k + 2 = k ′ . We claim that D = ∃r.Cn fits P, N. In the example … view at source ↗
Figure 3
Figure 3. Exact learning runtime both a daughter (gender female) and a son (male); we use also deeper concepts, referring to grand-children and so on. For the language fragment we use shallow concepts that contain Boolean combinations of concept names under existential or universal restrictions, for example, ∃l.(F ⊔ I ⊔ R) ⊓ ∀l.¬G. We highlight the impact of our optimizations on the encoding in [PITH_FULL_IMAGE:figures/full_… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

50 extracted references · 30 canonical work pages

  1. [1]

    https://www.w3.org/TR/2012/REC-owl2- overview-20121211/, accessed: July 24, 2025

    OWL 2 web ontology language overview. https://www.w3.org/TR/2012/REC-owl2- overview-20121211/, accessed: July 24, 2025

    work page 2012

  2. [2]

    Cam- bridge Tracts in Theoretical Computer Science, Cambridge University Press (1992)

    Anthony, M., Biggs, N.: Computational Learning Theory: An Introduction. Cam- bridge Tracts in Theoretical Computer Science, Cambridge University Press (1992)

    work page 1992

  3. [3]

    Cambridge University Press (2017)

    Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logics. Cambridge University Press (2017). https://doi.org/10.1017/9781139025355

    doi:10.1017/9781139025355 2017

  4. [4]

    Journal of the ACM (JACM)36(4), 929–965 (1989)

    Blumer, A., Ehrenfeucht, A., Haussler, D., Warmuth, M.K.: Learnability and the Vapnik-Chervonenkis dimension. Journal of the ACM (JACM)36(4), 929–965 (1989). https://doi.org/10.1145/76359.76371

    arXiv 1989

  5. [5]

    In: Proceedings of 42nd International Symposium on Theoretical Aspects of Computer Science, STACS

    Bordais, B., Neider, D., Roy, R.: The complexity of learning LTL, CTL and ATL formulas. In: Proceedings of 42nd International Symposium on Theoretical Aspects of Computer Science, STACS. LIPIcs, vol. 327, pp. 19:1–19:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2025). https://doi.org/10.4230/LIPICS.STACS. 2025.19

    doi:10.4230/lipics.stacs 2025

  6. [6]

    In: Companion Proceedings of the The Web Conference 2018

    Bühmann, L., Lehmann, J., Westphal, P., Bin, S.: DL-Learner – structured ma- chine learning on semantic web data. In: Companion Proceedings of the The Web Conference 2018. pp. 467–471 (2018). https://doi.org/10.1145/3184558.3186235

    work page arXiv 2018

  7. [7]

    In: Proceedings of the Twenty-Ninth International Conference on Automated Planning and Scheduling, ICAPS

    Camacho, A., McIlraith, S.A.: Learning interpretable models expressed in linear temporal logic. In: Proceedings of the Twenty-Ninth International Conference on Automated Planning and Scheduling, ICAPS. pp. 621–630. AAAI Press (2019). https://doi.org/10.1609/icaps.v29i1.3529

    work page doi:10.1609/icaps.v29i1.3529 2019

  8. [8]

    SIGMOD Rec.52(4), 6–18 (2023)

    ten Cate, B., Funk, M., Jung, J.C., Lutz, C.: Fitting algorithms for conjunc- tive queries. SIGMOD Rec.52(4), 6–18 (2023). https://doi.org/10.1145/3641832. 3641834, https://doi.org/10.1145/3641832.3641834

    work page arXiv 2023

Show all 50 references
  1. [9]

    In: Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023

    ten Cate, B., Funk, M., Jung, J.C., Lutz, C.: SAT-based PAC learning of description logic concepts. In: Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023. pp. 3347–3355. ijcai.org (2023). https://doi. org/10.24963/IJCAI.2023/373

    2023 doi

  2. [10]

    CoRRabs/2305.08511 (2023)

    ten Cate, B., Funk, M., Jung, J.C., Lutz, C.: SAT-based PAC learning of description logic concepts. CoRRabs/2305.08511 (2023). https://doi.org/10.48550/arXiv. 2305.08511

    2023 doi arXiv

  3. [11]

    Information Processing Letters183, 106431 (2024)

    ten Cate, B., Funk, M., Jung, J.C., Lutz, C.: On the non-efficient PAC learnability of conjunctive queries. Information Processing Letters183, 106431 (2024). https: //doi.org/10.1016/J.IPL.2023.106431

    2024

  4. [12]

    Machine Learning17(2-3), 169–199 (1994)

    Cohen, W.W., Hirsh, H.: The learnability of description logics with equality constraints. Machine Learning17(2-3), 169–199 (1994). https://doi.org/10.1007/ BF00993470

    1994

  5. [13]

    Demir,C.,NgongaNgomo,A.:Neuro-symbolicclassexpressionlearning.In:Proceed- ings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China. pp. 3624–3632. ijcai.org (2023). https://doi.org/10.24963/ijcai....

    2023 doi

  6. [14]

    In: Proceedings of the Thirtieth International Joint Confer- ence on Artificial Intelligence, IJCAI-21

    Funk, M., Jung, J.C., Lutz, C.: Actively learning concept and conjunctive queries under EL r-ontologies. In: Proceedings of the Thirtieth International Joint Confer- ence on Artificial Intelligence, IJCAI-21. pp. 1887–1893 (2021). https://doi.org/10. 24963/ijcai.2021/260

    2021

  7. [15]

    Funk, M., Jung, J.C., Lutz, C., Pulcini, H., Wolter, F.: Learning description logic concepts: When can positive and negative examples be separated? In: Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI-19. pp. 1682–1688 (2019). h...

    2019 doi

  8. [16]

    In: WWW ’22: The ACM Web Conference 2022

    Heindorf, S., Blübaum, L., Düsterhus, N., Werner, T., Golani, V.N., Demir, C., Ngonga Ngomo, A.: EvoLearner: Learning description logics with evolutionary algorithms. In: WWW ’22: The ACM Web Conference 2022. pp. 818–828. ACM (2022). https://doi.org/10.1145/3485447.3511925

    2022

  9. [17]

    In: Doherty, P., Mylopoulos, J., Welty, C.A

    Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Doherty, P., Mylopoulos, J., Welty, C.A. (eds.) Proceedings, Tenth International Conference on Principles of Knowledge Representation and Reasoning, Lake District of the United Kingdom, June 2-5, 2006. ...

    2006

  10. [18]

    Applied Intelligence26(2), 139–159 (2007)

    Iannone, L., Palmisano, I., Fanizzi, N.: An algorithm based on counterfactuals for concept learning in the semantic web. Applied Intelligence26(2), 139–159 (2007). https://doi.org/10.1007/S10489-006-0011-5

    2007 doi

  11. [19]

    In: Theory and Applications of Satisfiability Testing – SAT 2018

    Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: A Python toolkit for pro- totyping with SAT oracles. In: Theory and Applications of Satisfiability Testing – SAT 2018. pp. 428–437 (2018). https://doi.org/10.1007/978-3-319-94144-8_26

    2018 doi

  12. [20]

    In: 27th International Conference on Theory and Applications of Satisfiability Testing

    Ignatiev, A., Tan, Z.L., Karamanos, C.: Towards universally accessible SAT technol- ogy. In: 27th International Conference on Theory and Applications of Satisfiability Testing. pp. 4:1–4:11 (2024). https://doi.org/10.4230/LIPICS.SAT.2024.16

    2024 doi

  13. [21]

    Journal of the ACM (JACM)41(1), 67–95 (1994)

    Kearns, M.J., Valiant, L.G.: Cryptographic limitations on learning Boolean formulae and finite automata. Journal of the ACM (JACM)41(1), 67–95 (1994). https: //doi.org/10.1145/174644.174647

    1994

  14. [22]

    In: Machine Learning: ECML-93

    Kietz, J.: Some lower bounds for the computational complexity of inductive logic programming. In: Machine Learning: ECML-93. pp. 115–123 (1993). https://doi. org/10.1007/3-540-56602-3_131

    1993 doi

  15. [23]

    In: The Semantic Web - 20th International Conference, ESWC 2023

    Kouagou, N.J., Heindorf, S., Demir, C., Ngomo, A.N.: Neural class expression synthesis. In: The Semantic Web - 20th International Conference, ESWC 2023. Lecture Notes in Computer Science, vol. 13870, pp. 209–226. Springer (2023). https://doi.org/10.1007/978-3-031-33455-9_13

    2023 doi

  16. [24]

    In: Machine Learning and Knowledge Discovery in Databases: Research Track - European Conference, ECML PKDD 2023

    Kouagou, N.J., Heindorf, S., Demir, C., Ngonga Ngomo, A.: Neural class expression synthesis in ALCHIQ(D). In: Machine Learning and Knowledge Discovery in Databases: Research Track - European Conference, ECML PKDD 2023. Lecture Notes in Computer Science, vol. 14172, pp. 196–212...

    2023 doi

  17. [25]

    Lehmann, J.: Learning OWL Class Expressions, Studies on the Semantic Web, vol. 6. IOS Press (2010). https://doi.org/10.3233/978-1-61499-340-7-i

    2010 doi

  18. [26]

    In: Per- spectives on Ontology Learning, pp

    Lehmann, J., Fanizzi, N., Bühmann, L., d’Amato, C.: Concept learning. In: Per- spectives on Ontology Learning, pp. 71–91. AKA / IOS Press (2014), https: //jens-lehmann.org/files/2014/pol_concept_learning.pdf

    2014

  19. [27]

    Machine Learning78, 203–250 (2010)

    Lehmann, J., Hitzler, P.: Concept learning in description logics using refine- ment operators. Machine Learning78, 203–250 (2010). https://doi.org/10.1007/ s10994-009-5146-2 SAT-Based Bounded Fitting for the Description LogicALC 19

    2010

  20. [28]

    Information Systems83, 89–100 (2019)

    Martins, D.M.L.: Reverse engineering database queries from examples: State-of-the- art, challenges, and research opportunities. Information Systems83, 89–100 (2019). https://doi.org/10.1016/J.IS.2019.03.002

    2019 doi

  21. [29]

    CoRRabs/2312.16336 (2023)

    Mascle, C., Fijalkow, N., Lagarde, G.: Learning temporal formulas from examples is hard. CoRRabs/2312.16336 (2023). https://doi.org/10.48550/ARXIV.2312.16336

    2023 doi arXiv

  22. [30]

    In: Proceedings of 18th Conference on Formal Methods in Computer Aided Design FMCAD

    Neider, D., Gavran, I.: Learning linear temporal properties. In: Proceedings of 18th Conference on Formal Methods in Computer Aided Design FMCAD. pp. 1–10. IEEE (2018). https://doi.org/10.23919/FMCAD.2018.8603016

    2018

  23. [31]

    Pitt, L., Valiant, L.G.: Computational limitations on learning from examples. J. ACM 35(4), 965–984 (1988). https://doi.org/10.1145/48014.63140

    1988

  24. [32]

    In: Proceedings of 12th International Joint Conference on Automated Reasoning IJCAR

    Pommellet, A., Stan, D., Scatton, S.: SAT-based learning of computation tree logic. In: Proceedings of 12th International Joint Conference on Automated Reasoning IJCAR. Lecture Notes in Computer Science, vol. 14739, pp. 366–385. Springer (2024). https://doi.org/10.1007/978-3-0...

    2024 doi

  25. [33]

    In: Kazmierski, T.J., von Hanxleden, R., Mak, T.S.T

    Riener, H.: Exact synthesis of LTL properties from traces. In: Kazmierski, T.J., von Hanxleden, R., Mak, T.S.T. (eds.) 2019 Forum for Specification and Design Languages, FDL 2019, Southampton, United Kingdom, September 2-4, 2019. pp. 1–6. IEEE (2019). https://doi.org/10.1109/F...

    2019

  26. [34]

    Future Gener

    Rizzo, G., Fanizzi, N., d’Amato, C.: Class expression induction as concept space exploration: From DL-FOIL to DL-FOCL. Future Gener. Comput. Syst.108, 256–272 (2020). https://doi.org/10.1016/J.FUTURE.2020.02.071

    2020 doi

  27. [35]

    In: Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol

    Sakallah, K.A.: Symmetry and satisfiability. In: Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 509–570. IOS Press (2021). https://doi.org/10.3233/FAIA200996

    2021 doi

  28. [36]

    In: Proceedings of the 47th International ACM SIGIR Conference on Research and Development in Information Retrieval, SIGIR 2024

    Suchanek, F.M., Alam, M., Bonald, T., Chen, L., Paris, P., Soria, J.: YAGO 4.5: A large and clean knowledge base with a rich taxonomy. In: Proceedings of the 47th International ACM SIGIR Conference on Research and Development in Information Retrieval, SIGIR 2024. pp. 131–140. ...

    2024 doi

  29. [37]

    Journal of Machine Learning Research18, 64:1–64:34 (2017), https://jmlr.org/papers/v18/14-317.html

    Tran, A.C., Dietrich, J., Guesgen, H.W., Marsland, S.: Parallel symmetric class expression learning. Journal of Machine Learning Research18, 64:1–64:34 (2017), https://jmlr.org/papers/v18/14-317.html

    2017

  30. [38]

    Communications of the ACM27(11), 1134–1142 (1984)

    Valiant, L.G.: A theory of the learnable. Communications of the ACM27(11), 1134–1142 (1984). https://doi.org/10.1145/1968.1972

    1984

  31. [39]

    Semantic Web10(2), 231–245 (2019)

    Westphal, P., Bühmann, L., Bin, S., Jabeen, H., Lehmann, J.: SML-bench - A benchmarking framework for structured machine learning. Semantic Web10(2), 231–245 (2019). https://doi.org/10.3233/SW-180308

    2019 doi

  32. [40]

    In: American Federation of Information Processing Societies: 1975 National Computer Conference, 19-22 May 1975, Anaheim, CA, USA

    Zloof, M.M.: Query by example. In: American Federation of Information Processing Societies: 1975 National Computer Conference, 19-22 May 1975, Anaheim, CA, USA. AFIPS Conference Proceedings, vol. 44, pp. 431–438. AFIPS Press (1975). https://doi.org/10.1145/1499949.1500034 20 M...

    1975

  33. [41]

    C = ¬D: a ∈ (¬D)I ⇔ a /∈ DI (I.H) ⇔ a ∈ D IΣ ⇔ a /∈ (¬D)IΣ = (¬D)IΣ

  34. [42]

    C = (C1 ⊓ C2): a ∈ (C1 ⊓ C2)I ⇔ a ∈ C I 1 ∩ C I 2 (I.H) ⇔ a /∈ C1 IΣ and a /∈ C2 IΣ ⇔ a /∈ (C1 IΣ ∪ C2 IΣ ) ⇔ a /∈ (C1 ⊔ C2)IΣ = (C1 ⊓ C2) IΣ

  35. [43]

    C = (C1 ⊔ C2): a ∈ (C1 ⊔ C2)I ⇔ a ∈ C I 1 ∪ C I 2 (I.H) ⇔ a /∈ C1 IΣ or a /∈ C2 IΣ ⇔ a /∈ (C1 IΣ ∩ C2 IΣ ) ⇔ a /∈ (C1 ⊓ C2)IΣ = (C1 ⊔ C2) IΣ

  36. [44]

    C = ∃r.C1: a ∈ (∃r.C1)I ⇔ there is (a, b) ∈ rI with b ∈ C I 1 (I.H) ⇔ there is (a, b) ∈ rIΣ and b /∈ C1 IΣ ⇔ a /∈ (∀r.C1)IΣ = (∃r.C1) IΣ SAT-Based Bounded Fitting for the Description LogicALC 21

  37. [45]

    only if"-direction; the

    C = ∀r.C1: a ∈ (∀r.C1)I ⇔ for all (a, b) ∈ rI : b ∈ C I 1 (I.H) ⇔ for all (a, b) ∈ rI : b /∈ C1 IΣ ⇔ for all (a, b) ∈ rI : b ∈ (¬C 1)IΣ ⇔ a ∈ (∀r.¬C1)IΣ = (¬∃r.C 1)IΣ = (¬∀r.C1)IΣ ⇔ a /∈ ∀r.C1 IΣ Lemma 1. For any signatureΣ, all sets of examplesP and N and ALC concepts C with ...

  38. [46]

    , an, a′ n} contains a single element and this element satisfies Di

    Rwi (I, a) ∩ {a0, a′ 0, . . . , an, a′ n} contains a single element and this element satisfies Di

  39. [47]

    In the inductive base, we setw1 = r and D1 = D

    Rwi (J , b) ̸= ∅ and no element fromRwi (J , b) satisfies Di. In the inductive base, we setw1 = r and D1 = D. Clearly, Properties 1 and 2 are satisfied by this choice. For the inductive step, take anyCi = ∃wi.Di. We distinguish cases on the shape of Di. The easy cases are the ...

  40. [48]

    Proof of the claim.To show, (i)⇒(ii), let α be a satisfying assignment ofφ

    | 1 ≤ i ≤ m}, N = {(J , a)}: (i) φ is satisfiable; (ii) there is anL({∀}) concept fitting P, N; (iii) there is anL({∀, ∃, ⊓}) concept fitting P, N. Proof of the claim.To show, (i)⇒(ii), let α be a satisfying assignment ofφ. Based on the definition of theIi and J, it is routine...

  41. [49]

    if d1 ∈ AI1 with A ∈ Σ, then d2 ∈ AI2

  42. [50]

    switch off

    if (d1, e1) ∈ rI1 with r ∈ Σ, there is(d2, e2) ∈ rI2 such that (e1, e2) ∈ S. For d1 ∈ ∆I1 and d2 ∈ ∆I2, we write (I1, d1) ⪯Σ (I2, d2) if there is a Σ-simulation S from I1 to I2 with (d1, d2) ∈ S. Simulationsareimportantsinceontheonehandtheyconvenientlycharacterize evaluation a...

Pith tools

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