Converting ALC Connection Proofs into ALC Sequents

Eunice Palmeira (Federal Institute of Alagoas); Fred Freitas (Federal University of Pernambuco); Jens Otten (University of Oslo)

REVIEW 4 major objections 5 minor 11 references

Converting ALC Connection Proofs into ALC Sequents

T0 review · 4 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read The paper claims that non-clausal ALC connection proofs can be converted into ALC sequent proofs, preserving the original formula structure and making the proofs readable.

desk verdict A plausible conversion method from ALC connection proofs to sequent proofs, but the central correctness claim is not proved and the key admissibility condition is under-specified. read the letter →

arxiv 1908.09477 v1 pith:3OYEZDTN submitted 2019-08-26 cs.SC cs.LO

Eunice Palmeira (Federal Institute of Alagoas) , Fred Freitas (Federal University of Pernambuco) , Jens Otten (University of Oslo) This is my paper · ORCID

classification cs.SCcs.LO MSC 03B3568T15

keywords connectionmethoddescriptionlogicALCsequentcalculusproofconversionreadabilitynon-clausalmatrixreductionorderautomatedtheoremproving

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 tries to establish that the compact, machine-oriented proofs produced by the non-clausal ALC connection method can be converted into ALC sequent proofs, which read as structured logical arguments and translate more easily into natural language. The conversion works directly on the original formula, avoiding the disjunctive-normal-form translation that obscures the structure of a query. It proceeds in four steps: build a formula tree, assign matrix literals to tree positions, construct a partial sequent proof structure from the connections, and complete the sequent proof using a correspondence between node types and sequent rules. If the construction succeeds, a valid ALC query that a connection prover certifies can be replayed as a sequent proof whose auxiliary algorithms are polynomial, with connection search the most expensive step at $O(n^4)$. The practical payoff is that ontology reasoners built on the connection method could justify their inferences in a human-readable form.

What carries the argument

The central object is the formula tree, a syntactic tree of the input ALC formula whose nodes are labelled with positions, polarities, and types $\alpha$, $\alpha'$, $\beta$, $\beta'$, $\gamma$, and $\delta$; the type of a node determines which sequent rule applies, for example an $\sqcap$-node with polarity 1 becomes $l\sqcap$ and a $\beta'$-node is reduced by the cut rule. The argument runs on the reduction order $\triangleleft$, defined as the transitive closure of $(\prec \cup \sqsubset_\delta \cup \sqsubset_{\beta'})^+$: $\prec$ is the tree ordering, $\sqsubset_\delta$ records that a type-$\delta$ node must be reduced before a type-$\gamma$ node whose position it replaces, and $\sqsubset_{\beta'}$ records instantiations of $\beta'$/ $\gamma$/ $\delta$ positions. The machinery works because the reduction order turns the spatial, path-checking information of a matrix proof into a linear schedule of sequent inferences, and the $\sigma_{\mathrm{Final}}$ substitution keeps track of which universal and existential positions are identified and which variables are instantiated. Admissibility of $\sigma_{\mathrm{Final}}$---non-reflexivity of $\triangleleft$---is the condition that the schedule is acyclic and hence executable as a sequent proof.

What would settle it

Exhibit one non-clausal ALC connection proof whose $\sigma_{\mathrm{Final}}$ substitution induces a reflexive reduction order, or run the conversion procedure on proofs emitted by a connection-based ALC reasoner and find any proof that terminates without an admissible substitution; either observation would refute the claim that all such proofs can be converted.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central claim is a constructive translation theorem: given an ALC query and a non-clausal $\theta$-connection proof of it, the procedure of Section 5.2 produces a proof in the ALC sequent calculus. The bridge is the $\sigma_{\mathrm{Final}}$ substitution, made of a position substitution $\sigma_\delta$ that maps type-$\gamma$ universal positions to type-$\delta$ existential positions and a second substitution $\sigma_{\beta'}$ that maps $\beta'$, $\gamma$, and $\delta$ positions to instances or $\beta'$ positions. Connections in the matrix proof become $\sigma_{\mathrm{Final}}$-complementary pairs of leaf nodes, and the transitive closure of the tree ordering with the relations induced by $\sigma_\delta$ and $\sigma_{\beta'}$ yields a reduction order $\triangleleft$ that schedules sequent rule applications. Definition 21 states that when $\triangleleft$ is not reflexive, $\sigma_{\mathrm{Final}}$ is admissible and a sequent proof can be constructed; the worked example of an ontology query about old ladies, cats, and cat owners shows each connection closing a branch of the sequent proof, with $\beta'$ nodes triggering cut rules. The conversion therefore gives a way to view the entire connection proof as a readable sequent derivation rather than a set of complementary pairs.

Load-bearing premise

The load-bearing premise is that every non-clausal ALC connection proof yields an admissible $\sigma_{\mathrm{Final}}$ substitution---that is, one whose reduction order is not reflexive---because the paper asserts but does not prove this for all connection proofs.

Editorial extensions

If this is right

A connection-method proof for an ALC query no longer has to be read through the lens of clause-form transformations; the converted sequent proof operates on the original formula structure.
Each connection in the matrix proof corresponds to closing a branch of the sequent proof, with the reduction order $\triangleleft$ fixing the order of rule applications, so the translation is deterministic once the formula tree and substitutions are fixed.
Because the main algorithms run in polynomial time, with the most expensive step at $O(n^4)$ for connection search, the conversion is practically feasible for proofs produced by connection-based ALC reasoners.
The resulting sequent proofs are better suited to automatic translation into natural-language justifications, as the paper demonstrates on the old-lady/cat-owner example.
The correspondence table between node types and sequent rules gives a direct recipe for assigning a sequent inference to every reduction step in the connection proof.

Reading between the lines

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

This suggests a practical test: instrument a connection-method prover for ALC to output $\sigma_{\mathrm{Final}}$ together with each proof, then check how often the reduction order is non-reflexive; if reflexive orders occur in real ontologies, the conversion would need a fallback for those cases.
One could formalize Definition 21 in a proof assistant and prove that admissibility of $\sigma_{\mathrm{Final}}$ is not only sufficient but also necessary for the existence of a sequent proof respecting the eigenvariable conditions, which the paper states but does not fully demonstrate.
Because the converted proofs use the cut rule for $\beta'$ nodes, a natural next step is to study whether cut elimination applied after conversion yields a cut-free ALC sequent proof, which would connect this work to standard proof normalization.
The same tree-ordering-and-substitution recipe may extend to other non-clausal connection calculi or other description logics, since the position machinery is not specific to ALC connectives.

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.

Desk Editor's Note

read the letter

This paper describes a method for converting non-clausal ALC connection proofs into ALC sequent proofs, motivated by the poor readability of connection proofs. The basic idea is sound: build a formula tree from the input query, use the connection proof to determine a reduction order, and then construct a sequent proof. The non-clausal presentation is a genuine extension of the authors' earlier clausal work, and the detailed worked example in Section 5 shows how the pieces fit together. The paper also gives a useful overview of the algorithms' polynomial complexity.

What is actually new is the non-clausal adaptation and the explicit correspondence between connection steps and sequent rules. The central conversion itself is already claimed in the cited thesis [10], so a reader expecting the full technical development here will be disappointed. The paper is essentially a condensed exposition, which is fine for a workshop, but it means the correctness of the method rests on the thesis rather than on anything proved in this document.

Where the paper is genuinely soft is in Definition 21 and the surrounding construction. Definition 21 asserts that a sigmaFinal substitution is admissible if the reduction order is not reflexive, and that in this case a sequent proof can be constructed. This is the load-bearing step, and no proof is given. Worse, the reduction order uses a relation ⋏β′ that is never actually defined; Definition 16 defines a substitution σβ′ but not the induced ordering. And even if that relation were filled in, non-reflexivity alone does not enforce the eigenvariable condition for the δ rules. An acyclic order can still allow a δ rule to be applied when its eigenvariable occurs in an unrelated formula of the lower sequent, which would be invalid. This is not a minor typo—it blocks the main theorem as stated.

Steps 3 and 4 of Section 5.2 are also described informally, with enough detail to follow the example but not enough to verify a general construction. The full algorithms are relegated to the thesis, so the paper is not self-contained. There is no machine-checked proof, no code, and no independent artifact to lean on.

The reader's and stress-test concerns land. This is a believable workshop contribution with a plausible idea and a good worked example, but the central claim—that every non-clausal ALC connection proof can be converted—is not established in this text. The paper is worth reading if you work on proof transformations or explainable DL reasoning, and it deserves referee time because an editor should ask the authors to supply the missing definitions and a real proof. But the current version should not be accepted as a correctness result.

My recommendation: send it to peer review with a clear request for a complete definition of the reduction order and a proof of the admissibility condition. If those are supplied, the paper could be solid; until then, treat it as an extended abstract.

Referee Report

4 major / 5 minor

Summary. The paper proposes a method for converting proofs produced by the non-clausal ALCθ-connection calculus [5,8] into proofs in the ALC sequent calculus of Borgida et al. [4]. The conversion proceeds in four steps: (1) building a formula tree with positions, polarities, and node types; (2) assigning matrix elements to leaf positions; (3) constructing a partial sequent proof structure from connections and a reduction order; (4) completing the sequent proof. The central claim is that if the final substitution σFinal is admissible in the sense that the induced reduction order ◁ is non-reflexive, then a sequent proof can be constructed (Definition 21). The paper illustrates the method on a single nontrivial ontology query and gives a brief complexity overview.

Significance. If the conversion were fully established, it would provide a useful bridge between efficient connection-method reasoning for ALC and readable sequent-style proofs, with potential applications to explanation generation and user interaction with description logic reasoners. The paper has clear strengths: it targets a concrete and relevant proof calculus, it includes a detailed worked example, it explicitly defines the target sequent calculus, and it states a concrete polynomial complexity claim (O(n^4) for the search-connections algorithm). The idea of using σδ and σβ′ substitutions to manage the order of quantifier reductions is promising. However, as submitted, the central correctness claim is not established: Definition 21 is stated without proof, the reduction order is not fully defined (⊏β′ is missing), and the crucial Steps 3 and 4 of Section 5.2 are described only informally via the example. The paper also defers the actual algorithms to the author's thesis [10], so the complexity claims cannot be checked from the text.

major comments (4)

[Section 5, Definition 21] The admissibility criterion for σFinal—non-reflexivity of the reduction order ◁—is stated to be sufficient for constructing a sequent proof, but no proof or lemma is provided that (a) every connection proof produced by the calculus of Figure 1 yields an admissible σFinal, or (b) the resulting reduction order respects the eigenvariable condition of the δ-rules (r∀, l∃, l¬∀, r¬∃) of Section 4. Non-reflexivity merely rules out cycles in ◁; it does not prevent a δ-rule from being applied when its eigenvariable already occurs elsewhere in the lower sequent, which is the actual side condition of the target sequent calculus. This is the central correctness gate of the paper, and it is not demonstrated.
[Section 5, Definitions 16 and 20] The ordering ⊏β′ is used in Definition 20 to define the reduction order ◁ as the transitive closure of ≺, ⊏δ, and ⊏β′, but Definition 16 defines only the substitution σβ′ and never defines an induced ordering ⊏β′. Without this ordering, the expression (≺∪⊏δ∪⊏β′)+ is not well-defined, and the admissibility predicate of Definition 21 cannot be checked from the text. This under-specification affects the main claim and the running example, where reduction orders involving β′ nodes are asserted without the missing definition.
[Section 5.2, Steps 3 and 4] The construction of the partial sequent proof structure is described only informally through the example. In Step 3, connections are 'analyzed' and the text states, for instance, that 'the second connection was only reached in the tree after the third connection,' but no algorithm or invariant specifies the order in which connections are processed or how paths between leaf nodes are combined into a reduction order. Step 4 is similarly informal: it says the partial structure is 'traversed,' but gives no rule for how the traversal yields the final sequent proof. Without a formal description, the conversion cannot be checked, implemented, or verified from the paper alone.
[Section 6] The complexity claims are made about algorithms that are only named, with the statement 'All the algorithms are demonstrated in [10]'. Since the conversion procedure is not fully specified in this paper—particularly Steps 3 and 4 of Section 5.2—the polynomial complexity claim cannot be verified from the manuscript, and the correctness of the method remains dependent on an external thesis that is not available to the reader.

minor comments (5)

[Section 4, Figure 3] The axiom rule labelled (l⊤) has ⊤ on the right of the sequent, so the label should be (r⊤).
[Section 2 and Section 5.1] There are several typos: 'th following formulae' in Section 2, 'eingevariable' in Section 5.1, and 'sequent poof' in Definition 20; these should be corrected.
[Example 6] The sentence 'y was θ-substituted by y (i.e., θ(y) = a)' is confusing and appears to contain a typo; it should state which variable is substituted by a. Also, in Example 1 the FOL rendering of the second axiom contains a free variable z in the conjunct ∀k(hasPet(z,k)→Cat(k)).
[Table 3] Several entries in Table 3 are empty (e.g., for ∃0, ∀1, ⊑0 under 'Typeδ'/'Typeγ'), which could be interpreted as missing rules; a brief note explaining that some node polarities/types have no directly corresponding rule in the target calculus would improve clarity.
[Section 5.2, Step 3 example] The running example is difficult to follow because branch names a, b, c, d are introduced without a figure showing their positions in the formula tree; a version of Figure 7 with branch annotations would substantially improve readability.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the conversion is a constructive translation from connection proofs to sequent proofs; the unproved admissibility criterion is a correctness gap, not a circular reduction.

full rationale

Step-by-step, Section 5.2's conversion takes an existing non-clausal ALC theta-connection proof as input and constructs a formula tree (Step 1), assigns matrix positions (Step 2), builds a partial sequent structure from the connection paths (Step 3), and then emits the complete sequent proof using Table 3's rule correspondence (Step 4). The output is not contained in the input: the input is a matrix/connection proof and the output is a sequent derivation in the external calculus of [4]. Definition 21 states that if the reduction order is non-reflexive then a sequent proof can be constructed, but this is asserted rather than proved; together with the undefined ordering, this is an under-specification and proof gap, not a circularity. The self-citations ([5], [8], [9], [10]) support the background connection calculus, the RACCOON reasoner, and the thesis containing implementation details; none of them defines the sequent consequence relation in terms of the conclusion or turns a fitted parameter into a predicted output. There is no equation in which a derived quantity equals its input by construction, and no fitted input is renamed as a prediction.

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

No numeric parameters are fitted; the substitutions sigmaDelta, sigmaBetaPrime, and sigmaFinal are derived from the formula tree and the input connection proof. No unexplained postulates are introduced; the formula tree, positions, and substitution functions are defined constructs of the conversion method, not new explanatory entities.

assumptions (4)

domain assumption Matrix characterization (Lemma 1): a matrix M is valid iff there are theta-substitutions and connections such that every path through M contains a theta-complementary connection.
Stated without proof in Section 3.1 and used to justify treating connection proofs as validity certificates.
domain assumption The ALC sequent calculus of Borgida et al. is sound and complete for ALC subsumption, with cut elimination.
Section 4 adopts this external calculus as the conversion target; Theorem 1 is cited from [6].
ad hoc to paper Definition 21: if the reduction order is not reflexive, a sequent proof can be constructed.
This is the conversion's key existence assertion; no proof is given for its generality.
ad hoc to paper The reduction order respects the eigenvariable conditions of the gamma/delta sequent rules.
Section 5.1 defines the ordering relation to enforce this, but does not prove that every connection proof yields such an order.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Converting ALC Connection Proofs into ALC Sequents." pith.science (2026). https://pith.science/paper/3OYEZDTN

@misc{pith2026190809477,
  author       = {Pith},
  title        = {Pith review of: Converting ALC Connection Proofs into ALC Sequents},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3OYEZDTN}},
  note         = {Machine review of arXiv:1908.09477}
}

read the original abstract

The connection method has earned good reputation in the area of automated theorem proving, due to its simplicity, efficiency and rational use of memory. This method has been applied recently in automatic provers that reason over ontologies written in the description logic ALC. However, proofs generated by connection calculi are difficult to understand. Proof readability is largely lost by the transformations to disjunctive normal form applied over the formulae to be proven. Such a proof model, albeit efficient, prevents inference systems based on it from effectively providing justifications and/or descriptions of the steps used in inferences. To address this problem, in this paper we propose a method for converting matricial proofs generated by the ALC connection method to ALC sequent proofs, which are much easier to understand, and whose translation to natural language is more straightforward. We also describe a calculus that accepts the input formula in a non-clausal ALC format, what simplifies the translation.

Figures

Figures reproduced from arXiv: 1908.09477 by the authors.

**Figure 1.** Non-clausal ALC θ-Connection Calculus. CatOwner1 by an extension step and instance a is the θ-substitution of CatOwner1 and CatOwner(a) 0 . This connection is still not enough to prove all the paths starting from CatOwner(a) 0 ; the paths that start in it and pass through the literals from the other connected clause, namely, Cat0 and hasPet0 , are still to be verified. Indeed, each connection creates two sets of lit… view at source ↗

**Figure 2.** The ALC non-clausal matrix proof of the F1 using the graphical matrix representation. Next, we present the Sequent Calculus to which ALC non-clausal proofs will be translated [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

**Figure 3.** The Sequent Calculus for ALC Subsumption [4]. OL ` ∃h.Au ∀h.C TRUE = A,C ` C l∃ ∃h.A,∀h.C ` ∃h.C lu ∃h.Au ∀h.C ` ∃h.C cut OL ` ∃h.C ∃h.C ` CO cut (∃h.C ` CO, OL ` ∃h.Au ∀h.C) ` (OL ` CO) lu (∃h.C ` CO)u(OL ` ∃h.Au ∀h.C) ` (OL ` CO) [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗

Figures from the paper (7 more)

**Figure 4.** Figure 4: ALC sequent proof for F1. The names of the clauses and the roles are abbreviated. 5 Conversion Method The process consists of two steps: building a formula tree and then converting this formula tree into sequents, given an ALC query and its matrix non-clausal connectio…

**Figure 5.** Figure 5: Node Representation [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]

**Figure 6.** Figure 6: Step 01 Process of building the formula tree for [PITH_FULL_IMAGE:figures/full_fig_p010_6.png]

**Figure 7.** Figure 7: Formula Tree for F1 with labels, polarities and types. For a given formula A, A 0 , B, B 0 , Γ and ∆ are used to denote the sets of node positions of type α, α 0 , β, β 0 , γ, and δ, respectively. Definition 15. (Substitution of positions σδ, ordering relation @δ)). It…

**Figure 8.** Figure 8: Steps representation in the connection proof/ [PITH_FULL_IMAGE:figures/full_fig_p012_8.png]

**Figure 9.** Figure 9: Complete proof in ALC sequents for F1. 6 Complexity This section presents a very brief overview of the main algorithms for the conversion method with its complexities, according to the 4 steps seen in section 5.2. All the algorithms are demonstrated in [10]. Time compl…

**Figure 10.** Figure 10: Overview of the main algorithms’ order. this conversion assumes that the input formulae will always be in non-clausal form, i.e., without the need to transform these formulae into any normal form. A tree representation of formulae is used as a guide in this conversion…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

11 extracted references · 8 canonical work pages

[10]

Palmeira (2017): Conversion of Proof in Description LogicALC Generated by Connection Method into Sequents

E. Palmeira (2017): Conversion of Proof in Description LogicALC Generated by Connection Method into Sequents. Ph.D. thesis, Federal University of Pernambuco

work page 2017
[4]

Borgida, E

A. Borgida, E. Franconi & I. Horrocks (2000): ExplainingALC Subsumption. In: ECAI 2000, Proceedings of the 14th European Conference on Artiﬁcial Intelligence, Berlin, Germany, 2000, pp. 209–213

work page 2000
[1]

Baader, D

F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi & P. F. Patel-Schneider, editors (2003):The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press

work page 2003
[2]

Baader, I

F. Baader, I. Horrocks & U. Sattler (2008): Description Logics. In: Handbook of Knowledge Representation, Foundations of Artiﬁcial Intelligence 3, Elsevier, pp. 135–179, doi:10.1016/S1574-6526(07)03003-9

doi:10.1016/s1574-6526(07)03003-9 2008
[3]

Bibel (1993): Deduction - automated logic

W. Bibel (1993): Deduction - automated logic. Academic Press

work page 1993
[5]

Freitas & J

F. Freitas & J. Otten (2016): A Connection Calculus for the Description Logic ALC. In: Advances in Artiﬁcial Intelligence - 29th Canadian Conference on Artiﬁcial Intelligence, Canadian AI 2016, Victoria, BC, Canada, May 31 - June 3, 2016. Proceedings, pp. 243–256, doi:10.1007/978-3-319-34111-8 30

doi:10.1007/978-3-319-34111-8 2016
[6]

Cambridge University Press

Jean-Yves Girard, Paul Taylor & Yves Lafont (1989): Proofs and Types. Cambridge University Press

work page 1989
[7]

Horrocks (2008): Ontologies and the semantic web

I. Horrocks (2008): Ontologies and the semantic web . Commun. ACM 51(12), pp. 58–67, doi:10.1145/1409360.1409377

work page arXiv 2008

Show all 11 references

[8]

D. Melo, F. Freitas & J. Otten (2017):RACCOON: A Connection Reasoner for the Description Logic ALC. In: LPAR-21, 21st International Conference on Logic for Programming, Artiﬁcial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, pp. 200–211

2017
[9]

Otten (2011): A Non-clausal Connection Calculus

J. Otten (2011): A Non-clausal Connection Calculus . In: Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Bern, Switzerland, July 4-8, 2011. Proceedings, pp. 226–241, doi:10.1007/978-3-642-22119-4 18

2011 doi
[11]

D. A. Plaisted & S. Greenbaum (1986): A Structure-Preserving Clause Form Translation. J. Symb. Comput. 2(3), pp. 293–304, doi:10.1016/S0747-7171(86)80028-1

1986 doi

Pith tools

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

[1] [10]

Palmeira (2017): Conversion of Proof in Description LogicALC Generated by Connection Method into Sequents

E. Palmeira (2017): Conversion of Proof in Description LogicALC Generated by Connection Method into Sequents. Ph.D. thesis, Federal University of Pernambuco

work page 2017

[2] [4]

Borgida, E

A. Borgida, E. Franconi & I. Horrocks (2000): ExplainingALC Subsumption. In: ECAI 2000, Proceedings of the 14th European Conference on Artiﬁcial Intelligence, Berlin, Germany, 2000, pp. 209–213

work page 2000

[3] [1]

Baader, D

F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi & P. F. Patel-Schneider, editors (2003):The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press

work page 2003

[4] [2]

Baader, I

F. Baader, I. Horrocks & U. Sattler (2008): Description Logics. In: Handbook of Knowledge Representation, Foundations of Artiﬁcial Intelligence 3, Elsevier, pp. 135–179, doi:10.1016/S1574-6526(07)03003-9

doi:10.1016/s1574-6526(07)03003-9 2008

[5] [3]

Bibel (1993): Deduction - automated logic

W. Bibel (1993): Deduction - automated logic. Academic Press

work page 1993

[6] [5]

Freitas & J

F. Freitas & J. Otten (2016): A Connection Calculus for the Description Logic ALC. In: Advances in Artiﬁcial Intelligence - 29th Canadian Conference on Artiﬁcial Intelligence, Canadian AI 2016, Victoria, BC, Canada, May 31 - June 3, 2016. Proceedings, pp. 243–256, doi:10.1007/978-3-319-34111-8 30

doi:10.1007/978-3-319-34111-8 2016

[7] [6]

Cambridge University Press

Jean-Yves Girard, Paul Taylor & Yves Lafont (1989): Proofs and Types. Cambridge University Press

work page 1989

[8] [7]

Horrocks (2008): Ontologies and the semantic web

I. Horrocks (2008): Ontologies and the semantic web . Commun. ACM 51(12), pp. 58–67, doi:10.1145/1409360.1409377

work page arXiv 2008