The generation of proof certi cates and the use of proof checkers is nowadays standard in rst-order automated theorem proving and related areas. They have, to the best of our knowledge, not yet been employed in Description Logics, where the focus was on detecting and repairing errors in the ontology, rather than on catching erroneous consequences created by an incorrect reasoner. This paper reports on rst steps towards remedying this de cit for subsumptions computed by the DL reasoner Elk. We use an existing tool for generating proofs of consequences from Elk, and transform these proofs into a format that is accepted as certi cates by our proof checker. The checker is obtained as an instance of a generic certi cation tool based on the Logical Framework with Side Conditions (LFSC), by formalizing the inference rules of Elk in LFSC. We report on the results of applying this approach to the classi cation of a large number of real-world OWL 2 EL ontologies.
The purpose of this paper is to show that tools developed in rst-order automated theorem proving (ATP) and satis ability modulo theories (SMT) for certifying reasoning results can in principle also be employed in Description Logic (DL) to increase the trust in reasoning results (such as the subsumption hierarchy) computed by DL reasoners.
Highly-optimized automated reasoning tools are complex software systems, and thus may produce erroneous results due to programming errors, even if soundness and completeness of the underlying calculus have been proved in detail. If the results of the reasoning process are used in safety-critical situations (e.g., when verifying software), then it is important that one can trust these results. Since it is currently not possible to verify a large and sophisticated software system like an automated theorem prover, the solution to this problem is ? Partly funded by the DFG grant 389793660 as part of TRR 248.
Copyright c 2020 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0).
that the prover outputs a proof certi cate for the result, which can then easily
be checked using a proof checker. In contrast to the provers, proof checkers are
rather simple pieces of software, and thus are easier to trust or verify. For this
reason, the generation of proof certi cates is now common in (general-purpose)
ATP [
Since most DLs [
This paper reports on rst steps towards remedying this de ciency, where
we mainly tried to employ existing software rather than implementing new one.
As reasoning task we consider classi cation for OWL 2 EL ontologies,2 i.e., the
computation of the subsumption hierarchy between the concepts de ned in the
given ontology. Our aim is to certify subsumption relationships that have been
computed by the consequence-based DL reasoner Elk [
We have evaluated our approach on a large number of real-world OWL 2 EL
ontologies, obtaining promising results. Our experiments show that the certi
cates are usually of manageable size and can be checked in reasonable time,
1 See, e.g., [
Evaluation (ORE) in 2015. 2 OWL 2 EL is a pro le of the standard Web Ontology Language OWL 2 https://www. w3.org/TR/owl2-pro les/. though creating them may take a relatively long time. The latter problem could be mitigated by developing reasoners that directly generate certi cates, rather than extracting them from outputs of existing tools not built for this purpose. 2
Certi cate generation in ATP and SMT takes various forms depending on the query issued to the prover and its result. When the query consists in showing that a goal formula ' is entailed by a set of hypotheses and the prover succeeds in proving that, the generated certi cate typically consists in a term that encodes a proof of ' from or, equivalently, a proof of the unsatis ability of [ f:'g. In the DL context, ' could be a subsumption statement C v D and an ontology. If the subsumption holds, then consequence-based calculi provide us with a proof of ' from whereas tableau-based calculi yield a proof of the unsatis ability of with an a ABox of the form fC(a); :D(a)g, which describes a counterexample to the subsumption statement.
The encoding of proofs varies depending on the proof system in which the
proof is expressed and the granularity of proof terms. Some provers, such as
Vampire [
The last approach to proof checking provides the highest level of exibility
because the same proof checker can be used for very di erent provers and proof
systems as long as those systems are representable in the underlying logical
framework. The approach also provides a high level of trust in principle, for two
reasons. First, a generic checker that has been used successfully with many proof
systems is arguably more trustworthy than one custom-made for a speci c proof
system, unless the latter is very simple. Second, because the proof system is an
input to the proof checker, it is expressed as set of proof rules whose soundness
can be proved separately with a proof assistant, such as Coq [
x: 1[fp tg]: 2
(Terms) t ::= x j c j t: j x[: ]: t j t1 t2
For this work, we have used the LFSC [
A slightly simpli ed version of LFSC's abstract syntax is provided in Figure 1.
It is an extension of LF's calculus, itself an extension of the simply typed
-calculus. The calculus has three levels of semantic entities, all denoted
by terms: values; types, understood as collections of values; and kinds, families
of types. The constant type denotes the kind of types. Types and kinds can be
dependent on (i.e., indexed by) values. Syntactically, if 2[x] is a type term whose
set of free term variables is fxg and 1 is a type term with no free variables, the
expression x: 1: 2[x] denotes in the calculus the (dependent) type of functions
that return a value of type 2[v] for each value v of type 1 for input x. When
2 has no free variables, the type x: 1: 2 is just the type 1 ! 2 of simply
typed -calculus,3 and we will use the latter notation for it, treating ! as right
associative. The same sort of parametrization applies to kinds as well, allowing
one for instance to de ne the type of vectors of size n with a type constant vec
of kind n:int: type where int is the prede ned type of mathematical integers.
LFSC adds to the calculus the possibility of imposing restrictions on the
parameters of a depended type. These restrictions are expressed operationally
by side conditions of the form fp tg where p is a program in the side condition
language and t is an LF term. The restriction, enforced at type checking time,
is that p does not fail and its result is equal to (more precisely, matches) t.
The LFSC Checker
The LFSC checker developed at the University of Iowa is a small, high
performance type checker for LFSC written in C++.4 It takes as input one or more
3 The type of unary functions with inputs of type 1 and outputs of type 2.
4 The checker is available in source form at https://github.com/CVC4/LFSC.
signature les containing an LFSC encoding of a proof system with side
conditions, and a le containing the certi cate, the proof term to be checked, and
reports whether the term is a correct proof or not. For any of the LFSC checker's
applications, the trusted core consists of the signature(s) used and the checker
itself which has, however, a rather small code base. Although the checker was
developed originally to check SMT proofs [
+ [
nite sets of axioms of the form C v D for concepts C; D (concept inclusion,
CI) and r1 : : : rn v r for role names r1; : : : ; rn; r (role inclusion, RI). The
+ concepts and ontologies, which de nes how interpretations I
semantics of E L?
assign sets CI to concepts C and under what conditions an interpretation is a
model of an ontology, is formalized in the usual way (see [
C v C R9 C v C9rv:D9r:DE v E
R > C v >
R
C v D u E u C v D C v E
Ru+ C Cv vD DCu vE E R? C v 9Cr:Dv ?
D v ?
Rv CC vv DE : D v E 2 O
R C0 v 9r1:C1 C1 v 9r2:C2 : : : Cn 1 v 9rn:Cn : r1 : : : rn v r 2 O
C0 v 9r:Cn
For E L+?, Elk follows a consequence-based approach for classi cation [
The OWL 2 EL standard de nes a range of axioms that can be seen as syn+-axioms. In addition to the rules shown here, Elk uses rules tactic sugar for E L? that convert those axioms into CIs or RIs, and some other rules we do not discuss for space constraints. To allow the certi cation of Elk proofs, we designed and implemented an LFSC signature specifying datatypes and rules corresponding to the language constructs and rules used in Elk. In the source code of Elk, we found 50 classes implementing the interface ElkInference for rule applications. +-axiom, We restricted ourselves to the inferences on (syntactic variations of) E L? and identi ed the rules actually used in the corpora discussed in the next section. This resulted in a set of 18 rules which we then implemented in LFSC. fP v R u S; P v 9r:T; T v Ug
O
P v P P v 9r:T
P v 9r:U
R0
Rv
TT vv UT RRR09v
P v P P v R u S
P v R R+Ru1
u R0
Rv P v 9r:U u R (a) Elk proof
P; R; S; T; U : conc
r : role o = P v R u S ; P v 9 r T ; T v U ; ; p = R0 (P v P) check (Ru+ (R9 (Rv (Rv (Ru1 ) : h(P v 9 r U u R) o p) o (R0 (T v T)))) (Rv o p)) (b) LFSC proof For illustration purposes, Figure 3 contains a fragment of the LFSC signature, in abstract syntax, showing how the rst seven Elk rules from Figure 2 could be encoded in LFSC.6 The rst three rows declare a number of types (with conc for concepts, ont for ontologies, and so on) and constants corresponding to the + symbols of E L?. For increased readability, for constants we use the same symbols + as the corresponding operator in E L?. The subset of ontology axioms used in the proof are encoded as a sequence of axiom constructed with the operators ; and ;. The type constant h is used to construct proof judgments, statements of the form h(a) expressing that axiom a is provable.
A proof rule is represented by a dependently-typed constant whose type directly encodes the rule's premises and conclusion. We name each such constant as its corresponding rule in Figure 2, except for rules Ru1 and Ru2 which correspond respectively to the rst and the second conclusion of rule Ru from that gure. For brevity, we use notation like x; y: 1: 2 as a shorthand for x: 1: y: 1: 2. The type of each rule is parametrized by term variables that correspond to the schema variables in the Elk rule. For instance, R+, which has type u c:conc: d:conc: e:conc: h(c v d) ! h(c v e) ! h(c v d u e); is parametrized by variables c, d, and e of type conc which correspond, respectively, to the schema variables C, D, and E of the corresponding Elk rule. The return type h(c v d u e) of Ru+ encodes the conclusion C v D u E of the Elk rule whereas the argument types h(c v d) and h(c v e) encode the two premises C v D and C v E. The other rules are similar. Note that the type of Rv encodes the side condition of the corresponding Elk rule by means of an LFSC side condition that checks whether the axiom c v d occurs in the input ontology o. This is done by the side condition program in (whose de nition is not shown), which scans o looking for c v d and returns tt if, and only if, it nds it. 6 The actual LFSC signature for the Elk calculus, including the side condition code, is provided in full in the appendix in the Lisp-like concrete syntax of LFSC. with the optimization that the two occurrences of subterm (R0 (P v P)) are factored out by the de ned constant p. In each rule application, underscores are used for arguments whose value does not need to be speci ed as it can be generated by type inference from the remaining arguments. The term directly represents the proof tree of the Elk proof. Intuitively, for the inner rule applications, the result of the rule (its conclusion) is given as input to the surrounding rule application. The term is a correct proof of P v 9r:U u R exactly if it is well typed and has type h(P v 9 r U u R). Using the type ascription operator :, the check command directs the LFSC checker to verify that.
Extracting Proofs Using Elk's Explanation Servive
To generate LFSC proofs that can serve as certi cates, we used the explanation
service implemented in Elk 0.5 [
This non-termination issue is solved in Algorithm 1 by keeping track, in the variable inferences, of the set of inferences (i.e., rule applications including 7 https://protege.stanford.edu/ Algorithm 1 Algorithm used for generating proofs. premises and conclusion) for the current branch of the proof being constructed. To generate a proof of an axiom , we start with the call generateProof( ; ;) with an empty set of inferences. Then we ask Elk via getInferencesFor( ) for inference steps, but consider only those inferences that are not already in inferences. For each inference inf, we call the procedure recursively on the premises involved, adding the current inference to the set inferences (Line 8). If the proof construction did not fail for any premise, we have constructed the proof and can return it (Line 12). To further speed up the computation, we use a global cache to store previously constructed proofs or sub-proofs (Line 1, 4, 5 and 11). 4
We used our approach to generate certi cates for E L+? ontologies and veri ed them using LFSC. Our experiments, including classi cation, certi cate generation, and certi cation, were performed on an Intel(R) Core(TM) i5-4590 CPU with 4 cores at 3.30GHz and 32 GB RAM. The operating system was Debian GNU/Linux 9. The code is available online.8 + ontologies:
We generated classi cation certi cates for two corpora of E L?
the OWL EL classi cation track of the OWL Reasoner Evaluation 2015 (ORE
2015) [
ORE
MOWLCorp 105 s 104 t n e lm 103 i a t n 102 E # 101 100
104 others, while also taking care that equivalence classes of concepts stayed intact. Speci cally, for each such equivalence class, we would pick an arbitrary cyclic chain of subsumption relations to be included. Furthermore, we excluded concept inclusions/equivalences that were explicitly stated in the ontology. In the following, when talking of the classi cation result, we always refer to the set of inferred subsumption relationships obtained this way, that is, the transitive reduct without explicitly stated concept inclusions and equivalences. We also removed ontologies for which the transitive closure of the stated subsumptions produced the whole hierarchy. After these removals, the ORE corpus contains 62 ontologies and the MOWLCorp corpus contains 310 ontologies. Figure 5 shows the number of axioms and the number of entailments to be veri ed.
We computed certi cates for each classi cation result and veri ed them with the LFSC checker. For one of the ontologies from MOwlCorp, we terminated the certi cate generation after 16 hours, while for all ontologies in ORE certi cate was generated. In Figure 6, we show for each of the ontologies the time taken for classi cation, certi cate generation, and veri cation by LFSC, where the x-axis shows the number of entailments that was certi ed. One can see that certi cate generation took signi cantly longer than the classi cation task itself, while certi cate veri cation took signi cantly less time in almost all cases. The long time for certi cate generation is to due the backtracking approach used to reconstruct the proofs with Elk. We expect this to incur a much smaller overhead if certi cates were generated directly during reasoning. It is therefore more insightful to look at the sizes of the generated certi cates. In Figure 7, we plot those sizes against the number of entailments in each ontology. Most certi cates had a size between 1 KB and 1 MB, with the largest certi cate being 1.43 GB. Note that these are certi cates for the whole subsumption hierarchy, and not for single subsumptions. Certi cates for single subsumptions are quite small. Despite their large sizes, the certi cates were veri ed by the LFSC checker in the order of milliseconds. Since we generated proofs for each entailment separately, our classi cation certi cates collectively contained a lot of redundancy. By caching and sharing subproofs, the cumulative size of the certi cates for all the entailments could be signi cantly reduced. 5
We have implemented a prototypical proof certi cation system for the reasoner Elk, utilizing the proof-generation facilities available in Elk for the generation of certi cates, and employing the LFSC checker as proof-checker. Our evaluation demonstrates that, even though certi cates may be quite large, they can nevertheless be veri ed in very short time. We exploited the explanation service of Elk to generate proof certi cates a posteriori. Ideally, the generation of certi cates should take place during reasoning. This would reduce certi cate generation times considerably and result in smaller certi cates. Before embarking on the major task of implementing a proof-producing reasoner for E L, we found it sensible to assess rst whether proof checking of DL reasoning results based on LFSC is viable in principle.
Since our focus was on evaluating certi cate checking rather than certi cate
generation, our algorithm for extracting proofs from Elk is fairly unsophisticated
and not optimal. For instance, by building the proof starting from the relevant
axioms in the ontology, rather than from the conclusion, we would avoid the need
for detecting cycles. This should lead to a procedure with the same (polynomial)
time complexity as Elk. The Proof Utility Library PULi9 or the techniques by
Alrabbaa et al. [
Certi cation of reasoning results is even more important for more
expressive DLs than the one supported by Elk since reasoners for them are more
complex and so more likely to contain errors. There are reasoners for more
expressive DLs, such as Avalance [
Encoding complex proof systems in LFSC has the cost of trusting, or proving formally, the soundness of the encoded proof rules for each system. An alternative approach would be to design a standardised, simpler proof system for all DLs, and have reasoners translate their proofs into proofs in that system. The challenge in that case is probably more of a social than a technical nature as it requires a community-wide acceptance of a common standard.
Finally, we point out that proofs, and proof checkers, can be used only to validate the soundness of a classi cation result. In principle, the completeness of classi cation results can be certi ed if the reasoner provides counter-examples for non-entailed subsumption relations, which could then be validated using model checking techniques for rst-order logic. Because the number of nonsubsumptions is usually much higher than the number of subsumptions, the challenge in this case would be nding common certi cates for a large number of non-subsumptions at a time. 9 https://github.com/liveontologies/puli
Included below is the LFSC signature used to model the fragment of the calculus of Elk used for our experiments. The source code of our implementation, CSV les with evaluation results, and information on how to repeat the experiments are provided under
https://lat.inf.tu-dresden.de/dl2020-certifying-classi cation-results .
For space constraints, the paper glosses over a number of lower level technical points. For instance, the handling of role chains is more complex in practice, and an exact description would have been out of the scope of the paper. The main points are the following.
{ LFSC does not support rules with a variable number of premises, which is why we had to represent rule applications of this kind by a sequence of rule application with a xed number of premises. For the -rule, the easiest way to do this is to allow existential role restrictions to contain role chains instead of roles, as we can then build up the role chain step-wise, before matching it with the role inclusion axiom. { For certi cation purposes, it is more convenient to use the needed axioms from the ontology as proof assumptions, instead of having side conditions that check their membership in the ontology. Checking that proof assumptions are from a given ontology can be achieved with the TBox proof rule. { Types rname, rchain, concept, axiom, and ontology are used respectively for roles, role chains, concepts, axioms, and ontologies. { An LFSC signature is de ned by a series of commands for declaring or de ning constants, for checking the well-typedness of term, and for de ning side-condition programs. New type or term constants are introduced by the declare command. Side condition programs are de ned by the program command. { The concrete syntax of LFSC is s-expression-based, as in Lisp and Scheme, so all the encoded E L operators are pre x operators (and typically have an alphanumeric name). Comments in the signature (lines starting with ;) relate these operators to the E L ones they encode. { While we do not use TBox axioms as side conditions in the certi cation, side conditions are used for various technical reasons not discussed in the paper. For instance, they are used to compute the concatenation of two role chains. The actual LFSC signature used in the experiments follows next. ;; LFSC encoding of ELK proof system ;; Authors: Patrick Koopmann and Cesare Tinelli ;; Date: June 2020 ;-------; Legend ;-------; (t1 t2) ; (! x 1 2) ; (\ x t) ; (% x t) ; (@ x t e) ; (: t) denotes function application " x : 1: 2 " x:t " x : :t " let x = t in e " t : ;; Note: Except for function applications, the syntax above is ;; used in LFSC terms, not in side condition programs ;---------------; Proof Language ;--------------;; Note: Every user-defined type ;; an algebraic datatype: ;; every function of return type ;; ; Role name type (declare rname type) ;; Note: no constructors are needed for rname, ;; using variables of type rname is enough.
in LFSC is effectively is a constructor for . ; Role chain type (declare rchain type) ;; Note: rchain is used to represent concatenations of roles ;; in (flat) normal form. ; Role chain constructors ; ; empty role chain (declare erc rchain) ; non-empty role chain constructor (declare rc (! x rname (! y rchain rchain))) ;; Note: rchains are essentially erc-terminated lists. ; Concept type (declare concept type) ; Concept constructors ; ; atomic concept (has the form (ac 0), (ac 1), ...) (declare ac (! n mpz concept)) ;; Note: mpz is the builtin type in LFSC of (infinite precision) ;; integers. The usual integer operators are built in. ; ; > (declare top concept) ; ? (declare bot concept) ; _ u _ (declare inter (! x concept (! y concept concept))) ; 9 _._ (declare ex (! x rchain (! y concept concept))) ;; Note: The first argument of ex is a *role chain*, not a role. ;; This is for convenience. ; ;; : _ (declare neg (! c concept concept)) ;; Note : should not be part of EL, but interestingly, ;; some rules of ELK use it. ; Axiom type (declare axiom type) ; Axiom constructors ; ; Concept inclusion _ v _ (declare sub (! x concept (! y concept axiom))) ; Concept equivalence _ _ (declare eq (! x concept (! y concept axiom))) ; Role (chain) inclusion _ v _ (declare rsub (! x rchain (! y rchain axiom))) ; Role (chain) equivalence _ _ (declare req (! x rchain (! y rchain axiom))) ; object property domain axioms (declare roleDomain (! x rchain (! y concept axiom))) ; object property range axioms (declare roleRange (! x rchain (! y concept axiom))) ; transitive property axiom (declare transRole (! r rchain axiom)) ; Ontology type (declare ontology type) ; Ontology constructors ; ; empty ontology (declare eon ontology) ; non-empty ontology constructor (declare on (! x axiom (! y ontology ontology))) ;; Note: An ontology is essentially a (flat, eon-termindated) ;; list of of axioms. ;------------------------; Side Condition Programs ;------------------------;; Side condition terms can appear directly in a side condition ;; or can be abstracted in named, parametrized programs. ;; Programs are functional, monomorphic, and first-order. ;; They can be recursive but not mutually recursive. They can ;; diverge, terminate normally (returning a value), or ;; abnormally (raising a "fail" exception). ;; Inputs and output are LF terms which need not be ground, ;; that is, they can contain logical variables. Those are not ;; to be confused with program variables, i.e., input parameters ;; and local variables. ;; Local variables are introduced by the match and let ;; constructs. Program variables are lexically scoped. ;; Program evaluation is eager, with pass-by-value semantics. ; Useful for side condition programs (declare bool type) ; bool constructors (declare tt bool) (declare ff bool) ; (IsIn t1 t2) returns tt if t1 occurs as an axiom of t2; ; it returns ff otherwise. (program isIn ((a axiom) (o ontology)) bool (match o (eon ff) ((on a1 o1) ; evaluates to tt if a1 is syntactically equal to a; ; and to the value of (isIn a o1) otherwise (ifequal a1 a tt (isIn a o1))))) ;; Note: For (IsIn t1 t2) to terminate normally t2 cannot be ;; a logical variable; it has to have the form eon or ;; (on a1 (on a2 ... (on an eon) ...)), otherwise match will fail. ;; However, t1, a1, ..., an can all be or contain logical variables. ; Concatenates two role chains (like list append) (program concat ((rc1 rchain) (rc2 rchain)) rchain
(match rc1 (erc rc2) ((rc r rs) (rc r (concat rs rc2))))) ;; Note: For similar reason as in isIn, (concat t1 t2) fails ;; if t1 is a logical variable ; Proof judgment for assumed or proved axioms. ; Technically, a type dependent on input axiom c. (declare holds (! c axiom type)) ;; The proof rules are functions whose return type has the form ;; (holds a) where a is the rule's conclusion. ;; The input parameters correspond to the rule's parameters ;; and premises, if any
(! sc (^ (isIn a o) tt) ; ----------------------
(holds a) ; TBox ; Every axiom in o is derivable (declare TBox (! o ontology (! a axiom ; rule parameters ; ; premises (none) ; side condition ; conclusion ;; Note: For notational convenience, side conditions are ;; introduced as fake arguments whose "type" has the form ;; (^ p r) where ;; - p is a side condition program (a term in the side-condition ;; language) and ;; - r is a term (possibly with variables). ;; When a proof rule is applied to actual arguments, ;; the side condition succeeds iff ;; 1) running p doesn't cause a fail exception and ;; 2) the result of p matches r ;; Any unbound variables in r get bound by the matching ;; substitution. ;; In TBox, p is the call (isIn a o) and r is the ground Boolean ;; term tt. ;; Note: The term (TBox t1 t2) is well typed iff ;; - t1 has type ontology, ;; - t2 has type axiom, and ;; - (isIn t1 t2) evaluates to tt ;; Since the the formal parameter sc of TBox is fictitious, ;; no actual parameter for it is needed in the rule application ;; (TBox t1 t2). ; Bottom Subclass (declare Bottom (! c concept ; rule parameters ; ; premises (none) ; ------------------(holds (sub bot c)) ; conclusion ? v C ; )) )) ; Top Superclass (declare Top (! c concept ; ;--------------------
(holds (sub c top)) ; Class Inclusion Tautology (declare subRef (! c concept ; ; ----------------(holds (sub c c)) ; C v C
; C v > ; )) ; )) ; Property Inclusion Tautology (declare rsubRef (! r rchain ; ; -----------------(holds (rsub r r))
; r v r ; Intersection Decomposition 1 (declare InterDec1 (! c concept (! d concept ; ; --------------------------
(holds (sub (inter c d) c)) ; C u D v C ; Intersection Decomposition ; Useful for nested intersections (declare InterDec (! c concept (! d concept ;
(! sc (^ (icontains c d) tt) ; D occurs in C ; ---------------------------
(holds (sub c d)) ; C v D ; Intersection Composition (declare InterComp (! c concept (! d concept (! e concept ; ; ))) ; ))) ; ))
(! p (holds (sub c d)) ; C v D ; ------------------------------(holds (sub (ex r c) (ex r d))) ; 9r:C v 9r:D (! p1 (holds (sub c d)) (! p2 (holds (sub c e)) ; --------------------------
(holds (sub c (inter d e))) ; )))))) ; Existential of Bottom (declare ExBottom (! r rchain ; ; ---------------------------(holds (sub (ex r bot) bot)) ; 9r:? v ? ; C v D ; C v E ; C v D u E ; Existential Property Expansion (declare ExExpandRole (! c concept (! r1 rchain (! r2 rchain ;
(! p (holds (rsub r1 r2)) ; --------------------------------
(holds (sub (ex r1 c) (ex r2 c))) ))))) ; r1 v r2 ; 9r1:C v 9r2:C ;; Note: The Existential Composition rule of ELK cannot be ;; encoded as a single LFSC rule because it has a variable ;; number of premises. So it has by several variants in LFSC. ; Existential Composition 1 (declare ExComp1 (! c0 concept (! c1 concept (! c2 concept
(! r1 rchain (! r2 rchain (! r rchain ; ; ; ; ))))))))))) ; Existential Composition 2 (declare ExComp2 (! c0 concept (! c1 concept
(! r1 rchain (! r rchain (! p1 (holds (sub c0 (ex r1 c1))) (! p2 (holds (rsub r1 r)) ; --------------------------------
(holds (sub c0 (ex r c1))) ; ))))))) ; C0 v 9r1:C1 ; C1 v 9r2:C2 ; r = r1 r2 ; C0 v 9r:C2 ; C0 v 9r1:C1 ; r1 v r ; C0 v 9r:C1 ; Existential Composition (declare ExComp (! c0 concept (! c1 concept (! c2 concept
(! r1 rchain (! r2 rchain (! r12 rchain (! r rchain ; Class Hierarchy (declare ConHi (! c1 concept (! c2 concept (! c3 concept ; ; )))))) ; C1 v C2 ; C2 v C3 ; C1 v C3 ; Property Hierarchy (declare RolHi (! r1 rchain (! r2 rchain (! r3 rchain ; ; Equivalent Classes Decomposition 1 (declare EqDec1 (! c concept (! d concept ;
(! p (holds (eq c d)) ; --------------------
(holds (sub c d)) ; )))) ; Equivalent Classes Decomposition 2 (declare EqDec2 (! c concept (! d concept ;
(! p (holds (eq c d)) ; --------------------
(holds (sub d c)) ; )))) ; C
D ; C v D ; C
D ; D v C ; Classes Inclusion Cycle (declare ConCyc (! c concept (! d concept ; (! p1 (holds (sub c d)) (! p2 (holds (sub d c)) ; ----------------------
(holds (eq c d)) ; ))))) ; C v D ; D v C ; D
C ; Proof judgment used to single out a goal. (declare goal (! c axiom type)) ; Proof judgment used for convenience. ; All goal-oriented proofs end in done. (declare done type) (! p1 (goal g) (! p2 (holds g) ; --------------
done )))) ; we can conclude that we are done ;---------------------------------------------------------; Missing Rules used by ELK but not mentioned in ELK paper ;---------------------------------------------------------; Property Domain Translation (declare RoleDomain (! r rchain (! c concept ;
(! p1 (holds (roleDomain r c)) ; -----------------------------
(holds (sub (ex r top) c)) )))) ; The domain of r is C ; 9r:> v C ; Transitive Role (declare TransitiveRole (! r rchain (! rr rchain ; (! p1 (holds (transRole r)) (! sc (^ (concat r r) rr) ; --------------------------
(holds (rsub rr r)) ))))) ; Negation Clash (declare NegationClash (! c concept ; ; ---------------------------------(holds (sub (inter c (neg c)) bot)) )) ; r is transitive ; rr = r r ; rr v r ; C u :C v ?
Included below is a le with several proof certi cates The certi cates were manually generated for greater readability. A few of the certi cates automatically generated with our implementation are available at https://lat.inf.tu-dresden.de/dl2020-certifying-classi cation-results. ;--------------------------------------------; Sample proof certificates for ELK signature ;--------------------------------------------; check proof that > v > (check (: (holds (sub top top))
(InterDec top top) )) ; check proof that C u D v C (check (% C concept (% D concept (: (holds (sub (inter C D) C))
(InterDec (inter C D) C) ))))) ; check proof that C u D v D (check (% n1 mpz (% n2 mpz (@ C (ac n1) (@ D (ac n2) (: (holds (sub (inter C D) D))
(InterDec (inter C D) D) )))))) ; Deductive proof of Kidney v Kidney ; Shows an axiom derivable from no assumption (check (% Kidney concept (: (holds (sub Kidney Kidney))
(subRef Kidney) ))) ; Goal oriented proof of Kidney v Kidney ; the expected goal is specified beforehand (check ; -----------------------------------------------------;; Note:: _ above can be used instead of the actual ;; parameter whenever the latter can be constructed ;; from the other actual parameters by type inference. ;; In this case, the inferred actual parameter is ;; (sub Kidney Kidney) ; Proof from ontology ; ; Check that AntiDiuresis v 9isFunctionOf.Kidney ; follows from an ontology containing ; - AntiDiuresis (Excretion u 9actsSpecificallyOn.Urine ; u 9hasProcessActivity.decreasedActivityLevel) ; - AntiDiuresis v ExcretionOfUrine ; - ExcretionOfUrine v 9isFunctionOf.Kidney (check ; Roles (% actsSpecificallyOn rname (% hasProcessActivity rname (% isFunctionOf rname ; Concepts (@ AntiDiuresis (ac 1) (@ decreasedActivityLevel (ac 2) (@ Excretion (ac 3) (@ ExcretionOfUrine (ac 4) (@ Kidney (ac 5) (@ Urine (ac 6) ; Axioms ; AntiDiuresis (Excretion u 9actsSpecificallyOn.Urine ; u 9hasProcessActivity.decreasedActivityLevel) (@ a1 (eq AntiDiuresis (inter Excretion (inter (ex (rc actsSpecificallyOn erc) Urine)
(ex (rc hasProcessActivity erc) decreasedActivityLevel)))) ; AntiDiuresis v ExcretionOfUrine (@ a2 (sub AntiDiuresis ExcretionOfUrine) ; ExcretionOfUrine v 9isFunctionOf.Kidney (@ a3 (sub ExcretionOfUrine (ex (rc isFunctionOf erc) Kidney)) ; Ontology (@ o (on a1 (on a2 (on a3 eon))) ; Goal: AntiDiuresis v 9isFunctionOf.Kidney (% g (goal (sub AntiDiuresis (ex (rc isFunctionOf erc) Kidney))) ; Assumptions ; Proof of goal from assumptions (: done (Proved _ g (ConHi _ _ _ (TBox o a2) (TBox o a3) ) )))))))))))))))))) ;; Note: the applications of TBox are not really needed. ;; A proof of g from explicit assumptions a2 and a3 ;; should suffice as a proof certificate. ;; Proof from assumptions (no TBox applications) (check ; Roles (% actsSpecificallyOn rname (% hasProcessActivity rname (% isFunctionOf rname ; Concepts (@ AntiDiuresis (ac 1) (@ decreasedActivityLevel (ac 2) (@ Excretion (ac 3) (@ ExcretionOfUrine (ac 4) (@ Kidney (ac 5) (@ Urine (ac 6) ; Goal: AntiDiuresis v 9isFunctionOf.Kidney (% g (goal (sub AntiDiuresis (ex (rc isFunctionOf erc) Kidney))) ; Assumptions ; AntiDiuresis (Excretion u 9actsSpecificallyOn.Urine ; u 9hasProcessActivity.decreasedActivityLevel) (% p1 (holds (eq AntiDiuresis (inter Excretion (inter (ex (rc actsSpecificallyOn erc) Urine) (ex (rc hasProcessActivity erc)
decreasedActivityLevel))))) ; (Excretion u 9actsSpecificallyOn.Urine) ExcretionOfUrine (% p2 (holds (eq (inter Excretion
(ex (rc actsSpecificallyOn erc) Urine))
ExcretionOfUrine)) ; ExcretionOfUrine v 9isFunctionOf.Kidney (% p3 (holds (sub ExcretionOfUrine
(ex (rc isFunctionOf erc) Kidney))) ; Proof of goal from assumptions (: done (Proved _ g (ConHi _ _ _ (ConHi _ _ _ (InterComp _ _ _ (ConHi _ _ _ (EqDec1 _ _ p1) (InterDec1 Excretion ; actually inferrable, kept for readability (inter (ex (rc actsSpecificallyOn erc) Urine) (ex (rc hasProcessActivity erc)
decreasedActivityLevel)))) (ConHi _ _ _ (EqDec1 _ _ p1) (InterDec (inter Excretion (inter (ex (rc actsSpecificallyOn erc) Urine) (ex (rc hasProcessActivity erc)
decreasedActivityLevel))) (ex (rc actsSpecificallyOn erc) Urine)))) (EqDec1 _ _ p2)) p3))) ))))))))))))))