An Introduction To Description Logic IV Relations To First .
An Introduction to Description Logic IVRelations to first order logicMarco CeramiPalacký University in OlomoucDepartment of Computer ScienceOlomouc, Czech RepublicOlomouc, November 6th 2014Marco Cerami (UP)Description Logic IV6.11.20141 / 25
PreliminariesPreliminaries:First order logicMarco Cerami (UP)Description Logic IV6.11.20142 / 25
PreliminariesSyntaxSyntax: signature and termsA predicate signature s consists of:a countable set of predicate symbols P1 , . . . , Pn , . . ., each onewith arity 1,a countable set of function symbols f1 , . . . , fn , . . ., each onewith its arity,a countable set of constant symbols c1 , . . . , cn , . . ., that are0-ary function symbols.Given a countable set Var of individual variables, the set of Termsover a predicate signature is defined inductively as follows:every variable x Var is a term,every constant c s is a term,if t1 , . . . , tn are terms and f s is an n-ary function symbol,then f (t1 , . . . , tn ) is a term.Marco Cerami (UP)Description Logic IV6.11.20143 / 25
PreliminariesSyntaxSyntax: formulasThe set Ls of Formulas over a given predicate signature s is definedinductively as follows: and are formulas,if t1 , . . . , tn are terms and P s is an n-ary predicate, thenP(t1 , . . . , tn ) is a formula (called atomic formula),if ϕ, ψ are formulas, then ϕ, ϕ ψ, ϕ ψ are formulas,if ϕ(x) is a formula and x a variable, then xϕ(x) and xϕ(x)are formulas.A variable that does not fall within the scope of a quantifier is said tobe a free variable, otherwise, it is said to be bound. A formula thathas no free variable is a closed formula.Marco Cerami (UP)Description Logic IV6.11.20144 / 25
PreliminariesSyntaxFragmentsInteresting fragments of the set of first order formulas L are thefollowing:L̈ is the fragment where only binary and ternary predicatesare allowed,Ln is the set of formulas built up from a set of n variables.We are indeed interested in the sets L̈2 and L̈3 .Marco Cerami (UP)Description Logic IV6.11.20145 / 25
PreliminariesSemanticsSemantics: structures and assignmentsA first order structure M for a given signature s, is a structureM (M, (P M )P s , (f M )f s , (c M )c s ), where:M is a non-empty set, called domain,for each predicate symbol P s of arity n, P M is an n-aryrelation on M,for each function symbol f s of arity n, f M is an n-aryfunction on M andfor each constant symbol c s, c M is an element of M.An assignment α is a mapping α : Var M. Each assignmentextends univocally to an assignment on terms satisfying, for everyterms t1 , . . . , tn and each n-ary function f s, thatα(f (t1 , . . . , tn )) f M (α(t1 ), . . . , α(tn )).To denote that assignment α assigns objects v1 , . . . , vn to variablesx1 , . . . , xn , we will write α([v1 /x1 ], . . . , [vn /xn ]).Marco Cerami (UP)Description Logic IV6.11.20146 / 25
PreliminariesSemanticsSemantics: modelsGiven a structure M assignment α and a formula ϕ, we say that Mand α satisfy ϕ (in symbols M, α ϕ) if:if ϕ P(t1 , . . . , tn ) thenP M (α(t1 ), . . . , α(tn ))if ϕ ψ χ, thenM, α ψandM, α χif ϕ ψ, thenM, α 2 ψif ϕ x1 , . . . , xn ϕ(x1 , . . . , xn ), then exists v1 , . . . , vn Msuch thatM, α ϕ(v1 , . . . , vn )Marco Cerami (UP)Description Logic IV6.11.20147 / 25
PreliminariesLogicLogicWe say that a formula ϕ is satisfiable if there exists a structureM and an assignment α such thatM, α ϕ.We say that a formula ϕ is a tautology if for every structure Mand an assignment α it holds thatM, α ϕ.We say that a formula ϕ is entailed by a set of formulas Γ if forevery structure M and an assignment α it holds thatif M, α ψ, for every formula ψ Γ, then M, α ϕ.Marco Cerami (UP)Description Logic IV6.11.20148 / 25
Translating DL into FOLTranslating Description Logicinto first order logicMarco Cerami (UP)Description Logic IV6.11.20149 / 25
Translating DL into FOLSignatureTranslation of the signaturesGiven a description signature D hNI , NC , NR i, we define thefirst order signature sD NI NC NR , whereNI is the set of constant symbols,NC NR is the set of unary and binary predicate symbols.For every concept name A NC , every role name R NR and everyx, y Var , we define the translations of concept and role names,respectively, into the set of atomic first order formulas in thefollowing way:τ x (A) : A(x)τ x,y (R) : R(x, y ).Marco Cerami (UP)Description Logic IV6.11.201410 / 25
Translating DL into FOLAttributive languages with nominalsTranslation of complex concepts in ALCOThis translation can be inductively extended over the set of complexconcept in ALCO in the following way:τ x ( C ) : τ x (C )τ x (C u D) : τ x (C ) τ x (D)τ x (C t D) : τ x (C ) τ x (D)τ x ( R.C ) : y ( τ x,y (R) τ y (C ))τ x ( R.C ) : y (τ x,y (R) τ y (C ))τ x {a1 , . . . , an } : {a1 , . . . , an }(x)Marco Cerami (UP)Description Logic IV6.11.201411 / 25
Translating DL into FOLAttributive languages with nominalsSoundness of the translation/ FOLDLOO DL interpretationsMarco Cerami (UP)Description Logic IV/ FO structures6.11.201412 / 25
Translating DL into FOLAttributive languages with nominalsInclusion in L̈2ALC concepts can be expressed by means of L̈2 formulas. Indeed,there are needed just two variables.In the case of nested quantifiers, e.g. R. R. R.Awe have that the translation is y (R(x, y ) x(R(y , x) y (R(x, y ) A(y ))))and, since the inner variable “y ” is closed, when a value of theouter quantifier “ ” has to be calculated, this variable fallsoutside its scope.Marco Cerami (UP)Description Logic IV6.11.201413 / 25
Translating DL into FOLAttributive languages with nominalsIn case of conjugated quantified concepts, e.g.( R.A) u ( R.B)we have that the translation is( y )(R(x, y ) A(y )) ( y )(R(x, y ) B(y ))where each appearance of variable “y ” is closed inside thescope of a different quantifier and, for this reason, it doesnot fall inside the scope of the other quantifier.Marco Cerami (UP)Description Logic IV6.11.201414 / 25
Translating DL into FOLAttributive languages with nominalsTranslation of axiomsA concept inclusion axiom C v D can be translated in thefollowing form: x(τ x (C ) τ x (D))A concept assertion axiom C (a) can be translated in thefollowing form:τ x (C )[a/x]A role assertion axiom R(a, b) can be translated in thefollowing form:τ x,y (R)[a/x, b/y ]Marco Cerami (UP)Description Logic IV6.11.201415 / 25
Translating DL into FOLAttributive languages with nominalsTranslation of the reasoning tasksSince every reasoning task is reducible to knowledge baseconsistency, it is enough to translate this task.A TBox T {Ci v Di : 0 i n} is satisfiable iff the formula xVni 0τ x (Ci ) τ x (Di )is satisfiable.An ABox A {Cj (ai ) : hi, ji I } {Rj (ai , bk ) : hi, j, ki J}is satisfiable iff the formulaVhi,ji Iτ x (Cj )[ai /x] Vhi,j,ki Jτ x,y (Rj )[ai /x, bk /y ]is satisfiable.Marco Cerami (UP)Description Logic IV6.11.201416 / 25
Translating DL into FOLRole constructorsTranslation of different role constructorsThe translation of roles in the language ALCROI extends the onefor ALCO in the following way:τ x,y ( R) : τ x,y (R)τ x,y (R u S) : τ x,y (R) τ x,y (S)τ x,y (R t S) : τ x,y (R) τ x,y (S)τ x,y (R ) : τ y ,x (R)Marco Cerami (UP)Description Logic IV6.11.201417 / 25
Translating DL into FOLRole constructorsProperties of the translation of complex rolesAs for ALCO, also the soundness of the translation forcomplex roles in ALCROI is proved by means on a translationbetween the respective semantics.Again, it is easy to prove that only L̈2 formulas can beobtained.A role inclusion axiom R v P can be translated in thefollowing form: x y (τ x,y (R) τ x,y (P))Marco Cerami (UP)Description Logic IV6.11.201418 / 25
Translating DL into FOLRole compositionTranslation of role compositionThe translation of roles in the language ALCROI( ) extendsthe one for ALCROI in the following way:τ x,y (R S) : z( y (y z τ x,y (R)) x(x z τ x,y (S)))For longer chains of composed roles, the composition is definedas a binary operation:τ x,y (R1 R2 R3 . . . Rn 1 Rn ) τ x,y (τ x,y (. . . τ x,y (τ x,y (R1 R2 ) R3 ) . . . Rn 1 ) Rn )Since the inner variable “z” is closed, when a value of the outerquantifier “ ” has to be calculated, this variable falls outsideits scope.Hence, the translation of ALCROI( ) can be expressed bymeans of L̈3 formulas.Marco Cerami (UP)Description Logic IV6.11.201419 / 25
Translating DL into FOLCardinality restrictionsTranslation of cardinality restrictionThis translation of roles in the language ALCON and ALCOQ canbe made as an extension of the one for ALCO in two ways:by allowing an unbounded number of variables, sotranslating:τ x1 ,.,xn ( nR): x1 . . . xn (R(x, x1 ), . . . , R(x, xn ))by allowing an bounded quantifiers, so obtaining the F.O.fragment C 2 and translating:τ x,y ( nR): n y (R(x, y ))But both ways are essentially equivalent and go beyond C 2 .Marco Cerami (UP)Description Logic IV6.11.201420 / 25
Translating DL into FOLSummarySummaryDLFOLALCOL̈2ALCROIL̈2ALCROI( )L̈3ALCONC 2ALCOQC 2Marco Cerami (UP)Description Logic IV6.11.201421 / 25
Translating FOL into DLTranslating first order logicinto Description LogicMarco Cerami (UP)Description Logic IV6.11.201422 / 25
Translating FOL into DLTranslating FOL into DLIn general it is not possible to obtain a syntactical translationof the full first order logic into any DL language.Indeed, there are some FOL formulas that cannot be defined byany DL language:Iformulas with predicates with arity 2 cannot be used in DLconcepts, since there are just unary and binary predicates,Iformulas with more than one free variable cannot beexpressed as DL concepts, since these express just unaryrelations in the domain set,Iformulas with global quantification cannot be expressed as DLconcepts, since these only quantify on the successors of a givennode.Marco Cerami (UP)Description Logic IV6.11.201423 / 25
Translating FOL into DLTranslating fragments into DLIn A. Borgida, On the relative expressiveness of Description Logicsand predicate logics it is proved that the fragments L̈2 and L̈3 can beindeed translated into ALCROI and ALCROI( ) with somemodifications:the following two role constructors are introduced:identityid{hv , v i : v I }cross-productC D{hv , w i : v C I , w D I }Roles are treated as concept, in the sense that they canappear outside complex concepts or axioms.Marco Cerami (UP)Description Logic IV6.11.201424 / 25
Translating FOL into DLNow:the restriction of the signature to L̈ allows to restrict toformulas with just binary and unary predicates;the restriction of the language to L2 or L3 allows to restrict toformulas with just two or three variables;the modifications to the DL languages above provided allow totranslate formulas with up to three free variables;the global quantification can be treated through the use of auniversal role, which, in languages with role constructors, canbe obtained as R t R.Marco Cerami (UP)Description Logic IV6.11.201425 / 25
An Introduction to Description Logic IV Relations to rst order logic Marco Cerami Palack y University in Olomouc Department of Computer Science Olomouc, Czech Republic Olomouc, November 6th 2014 Marco Cerami (UP) Description Logic IV 6.11.2014 1 / 25. Preliminaries Preliminaries: First order logic Marco Cerami (UP) Description Logic IV 6.11.2014 2 / 25. Preliminaries Syntax Syntax: signature .
Dynamic Logic Dynamic Circuits will be introduced and their performance in terms of power, area, delay, energy and AT2 will be reviewed. We will review the following logic families: Domino logic P-E logic NORA logic 2-phase logic Multiple O/P domino logic Cascode logic
Digital Logic Fundamentals Unit 1 – Introduction to the Circuit Board 2 LOGIC STATES The output logic state (level) of a gate depends on the logic state of the input(s). There are two logic states: logic 1, or high, and logic 0, or low. The output of some gates can also be in a high-Z (high impedance) state, which is neither a high
MOSFET Logic Revised: March 22, 2020 ECE2274 Pre-Lab for MOSFET logic LTspice NAND Logic Gate, NOR Logic Gate, and CMOS Inverter Include CRN # and schematics. 1. NMOS NMOSNAND Logic Gate Use Vdd 10Vdc. For the NMOS NAND LOGIC GATE shown below, use the 2N7000 MOSFET LTspice model that has a gate to source voltage Vgs threshold of 2V (Vto 2.0).File Size: 586KB
categorical and hypothetical syllogism, and modal and inductive logic. It is also associated with the Stoics and their propositional logic, and their work on implication. Syllogistic logic and propositional logic led later to the development of predicate logic (or first order logic, i.e. the foundational logic for mathematics)
An Introduction to Modal Logic 2009 Formosan Summer School on Logic, Language, and Computation 29 June-10 July, 2009 ; 9 9 B . : The Agenda Introduction Basic Modal Logic Normal Systems of Modal Logic Meta-theorems of Normal Systems Variants of Modal Logic Conclusion ; 9 9 B . ; Introduction Let me tell you the story ; 9 9 B . Introduction Historical overview .
The University of Texas at Arlington Sequential Logic - Intro CSE 2340/2140 – Introduction to Digital Logic Dr. Gergely Záruba The Sequential Circuit Model x 1 Combinational z1 x n zm (a) y y Y Y Combinational logic logic x1 z1 x n z m Combinational logic with n inputs and m switching functions: Sequential logic with n inputs, m outputs, r .
2.2 Fuzzy Logic Fuzzy Logic is a form of multi-valued logic derived from fuzzy set theory to deal with reasoning that is approximate rather than precise. Fuzzy logic is not a vague logic system, but a system of logic for dealing with vague concepts. As in fuzzy set theory the set membership values can range (inclusively) between 0 and 1, in
opinions about the courts in a survey conducted by the National . criminal justice system, and that black women are imprisoned at a rate seven times greater than white women. The report indicates there has been an increase in their incarceration rate in excess of 400% in recent years. Further, three-fourths of the women, according to the report, were mothers, and two-thirds had children .
