Description Logic Knowledge Base Exchange

3y ago
68 Views
3 Downloads
1.50 MB
132 Pages
Last View : 2m ago
Last Download : 2m ago
Upload by : Esmeralda Toy
Transcription

Description Logic Knowledge Base ExchangeElena Botoevasupervisor: Diego CalvanesePhD Final ExaminationApril 10, 2014BolzanoElena Botoeva(FUB)Description Logic Knowledge Base Exchange1/33

Outline1 Introduction2 Summary of Work3 Results4 Technical DevelopmentUniversal SolutionsUniversal UCQ-solutionsUCQ-representationsElena Botoeva(FUB)Description Logic Knowledge Base Exchange2/33

Outline1 Introduction2 Summary of Work3 Results4 Technical DevelopmentUniversal SolutionsUniversal UCQ-solutionsUCQ-representationsElena Botoeva(FUB)Description Logic Knowledge Base Exchange3/33

Knowledge Base Exchange: a Simple ScenarioSizeCategoryColorChoose size5Choose color5BrandChoose brand5BItemOpen Shoes: (3 items .BApparelbrown sandStrappyeXXwedge sandPlateaueXXheel sandHighHeeleXX.Elena Botoeva(FUB)Description Logic Knowledge Base Exchange4/33

Knowledge Base Exchange: a Simple ScenarioSizeCategoryColorChoose size5BrandChoose color5Choose brand5BItemOpen Shoes: (3 items .brown sandStrappyeXXBApparelwedge sandPlateaueXXheel sandHighHeeleXX.Viewed as a knowledge uHighHeelPlateauHighHeelbrown sandwedge sandheel sand.Apparel.Elena Botoeva(FUB)Description Logic Knowledge Base Exchange4/33

Knowledge Base Exchange: a Simple ScenarioSizeCategoryColorChoose size5Choose color5BrandChoose brand5BItemOpen Shoes: (3 items .brown sandStrappyeXXBApparelwedge sandPlateaueXXheel sandHighHeeleXX.The website after restructuring:SizeCategoryColorChoose size5Choose color5BrandChoose brand5BProductSandals: (3 products hingbrown sandClassiceXXwedge sandPlatformeXXheel sandHeeledeXX.Elena Botoeva(FUB)Description Logic Knowledge Base Exchange4/33

Knowledge Base Exchange: a Simple ScenarioSizeCategoryColorChoose size5Choose color5BrandChoose brand5BItemOpen Shoes: (3 items Heel.brown sandStrappyeXXBApparelwedge sandPlateaueXXheel sandHighHeeleXX.The website after restructuring:SizeCategoryColorChoose size5Choose color5BrandChoose brand5BProductSandals: (3 products hingbrown sandClassiceXXwedge sandPlatformeXXheel sandHeeledeXX.Elena Botoeva(FUB)Description Logic Knowledge Base Exchange4/33

Data Exchange [Fagin et al., 2003]mapping MΣΣ11source schemaΣΣ22target schemaI1source instanceElena Botoeva(FUB)Description Logic Knowledge Base Exchange5/33

Data Exchange [Fagin et al., 2003]mapping MΣΣ11ΣΣ22target schemasource schemaI1source instanceElena Botoeva(FUB)best solutionI2target instanceDescription Logic Knowledge Base Exchange5/33

Data Exchange [Fagin et al., 2003]mapping MΣΣ11ΣΣ22target schemasource schemaI1best solutionI2target instancesource instanceMapping M is a set of inclusions of conjunctive queries (CQs) x, y q1 (x, y ) z q2 (x, z) .I1 is a complete database instance.I2 is an incomplete database instance.Elena Botoeva(FUB)Description Logic Knowledge Base Exchange5/33

Data Exchange ExampleM:I1 :Elena Botoeva(FUB) a, t.(AuthorOf (a, t) g .BookInfo(t, a, g ))AuthorOfnabokovlolitatolkienlotrDescription Logic Knowledge Base Exchange6/33

Data Exchange ExampleM:I1 : a, t.( AuthorOf (a, t)AuthorOf g .BookInfo(t, a, g )I2 kienlotrlotrtolkienfantasyI2 is a solution for I1 under M.Elena Botoeva(FUB)Description Logic Knowledge Base Exchange6/33

Data Exchange ExampleM:I1 : a, t.( AuthorOf (a, t) g .BookInfo(t, a, g )I2 omedytolkienlotrlotrtolkienfantasyI20 :BookInfololitanabokovnull1lotrtolkiennull2I2 is a solution for I1 under M.I20 is a universal solution for I1 under M.Elena Botoeva(FUB)Description Logic Knowledge Base Exchange6/33

Data Exchange ExampleM:I1 : a, t.( AuthorOf (a, t) g .BookInfo(t, a, g )I2 medytolkienlotrlotrtolkienfantasyI20 :I2 is a solution for I1 under M.I20 is a universal solution for I1 under M.Elena null2 there is a homomorphism from I20 to I2 .Description Logic Knowledge Base Exchange6/33

Incomplete Data and Knowledge ExchangeA framework for Data Exchange with incomplete data was proposed by Arenas et al.[2011].mapping MΣΣ11ΣΣ22target signaturesource signatureI1solutionI2incomplete source instanceElena Botoeva(FUB)Description Logic Knowledge Base Exchange7/33

Incomplete Data and Knowledge ExchangeA framework for Data Exchange with incomplete data was proposed by Arenas et al.[2011].mapping MΣΣ11ΣΣ22target signaturesource signaturelogical theory T1logical theory T2solutionElena Botoeva(FUB)I1I2source KBtarget KBDescription Logic Knowledge Base Exchange7/33

Incomplete Data and Knowledge ExchangeA framework for Data Exchange with incomplete data was proposed by Arenas et al.[2011].mapping MΣΣ11ΣΣ22target signaturesource signaturelogical theory T1logical theory T2solutionI1I2source KBtarget KBWe specialize this framework to Description Logics, and in particular to DL-Lite R .Elena Botoeva(FUB)Description Logic Knowledge Base Exchange7/33

Description Logic DL-LiteRDescription Logics (DLs) are decidable fragments of First-Order Logic,used as Knowledge Representation formalisms.DLs talk about the domain of interest by means of concepts (unary predicates): roles (binary predicates):Author, Book, A, BAuthorOf, WrittenBy, P, RDL-LiteR is a light-weight DL that asserts concept inclusions and disjointness of atomic concepts A,the domain P and the range P of atomic roles P,Book v WrittenBy , role inclusions and disjointness of atomic roles P andtheir inverses P , AuthorOf v WrittenBy , ground factsElena Botoeva(FUB)Author(nabokov), AuthorOf(nabokov,lolita),A(a), P(a, b).Description Logic Knowledge Base Exchange8/33

Description Logic DL-LiteRDescription Logics (DLs) are decidable fragments of First-Order Logic,used as Knowledge Representation formalisms.DLs talk about the domain of interest by means of concepts (unary predicates): roles (binary predicates):Author, Book, A, BAuthorOf, WrittenBy, P, RDL-LiteR is a light-weight DL that asserts concept inclusions and disjointness of atomic concepts A,the domain P and the range P of atomic roles P,Book v WrittenBy ,TBox T role inclusions and disjointness of atomic roles P andtheir inverses P , AuthorOf v WrittenBy , ground factsElena Botoeva(FUB)Author(nabokov), AuthorOf(nabokov,lolita),A(a), P(a, b).Description Logic Knowledge Base ExchangeABox A8/33

Description Logic DL-LiteRDescription Logics (DLs) are decidable fragments of First-Order Logic,used as Knowledge Representation formalisms.DLs talk about the domain of interest by means of concepts (unary predicates): roles (binary predicates):Author, Book, A, BAuthorOf, WrittenBy, P, RDL-LiteR is a light-weight DL that asserts concept inclusions and disjointness of atomic concepts A,the domain P and the range P of atomic roles P,Book v WrittenBy ,TBox T role inclusions and disjointness of atomic roles P andtheir inverses P , AuthorOf v WrittenBy , ground factsAuthor(nabokov), AuthorOf(nabokov,lolita),A(a), P(a, b).ABox ASatisfiability check over a DL-Lite R KB K hT , Ai can be donein polynomial time (in fact, in NLogSpace).Elena Botoeva(FUB)Description Logic Knowledge Base Exchange8/33

Outline1 Introduction2 Summary of Work3 Results4 Technical DevelopmentUniversal SolutionsUniversal UCQ-solutionsUCQ-representationsElena Botoeva(FUB)Description Logic Knowledge Base Exchange9/33

The Summary of my PhD WorkIn this thesis, we123Propose a general framework for exchanging Description LogicKnowledge Bases.Define and analyse relevant reasoning problems in this setting.Develop reasoning techniques and characterize the computationalcomplexity of the problems.Elena Botoeva(FUB)Description Logic Knowledge Base Exchange10/33

Outline1 Introduction2 Summary of Work3 Results4 Technical DevelopmentUniversal SolutionsUniversal UCQ-solutionsUCQ-representationsElena Botoeva(FUB)Description Logic Knowledge Base Exchange11/33

1. Knowledge Base Exchange Frameworkmapping MΣΣ11ΣΣ22target signaturesource signatureA1D1B1T1C1A1source KBElena Botoeva(FUB)Description Logic Knowledge Base Exchange12/33

1. Knowledge Base Exchange Frameworkmapping MΣΣ11ΣΣ22target signaturesource signatureA1D1B1Elena Botoeva(FUB)T1C1T2A2solutionB2C2A1A2source KBtarget KBDescription Logic Knowledge Base Exchange12/33

2. Reasoning ProblemsElena Botoeva(FUB)Description Logic Knowledge Base Exchange13/33

2. Reasoning ProblemsSolutionElena Botoeva(FUB)universal solutionpreserves all modelsuniversal UCQ-solutionpreserves all answers toUnions of Conjunctive QueriesUCQ-representationpreserves all answers to UCQs,independently of the ABoxDescription Logic Knowledge Base Exchange13/33

simpleA( ABa) ox, esexR(tea)nd,Rco ed(ant AB,bain o)lab xese lednulls2. Reasoning ProblemsABoxSolutionElena Botoeva(FUB)universal solutionpreserves all modelsuniversal UCQ-solutionpreserves all answers toUnions of Conjunctive QueriesUCQ-representationpreserves all answers to UCQs,independently of the ABoxDescription Logic Knowledge Base Exchange13/33

2. Reasoning Problemsnon-emptinessIs there any solutionfor K1 (resp. T1 ) under M?membershipIs K2 (resp. T2 ) a solutionfor K1 (resp. T1 ) under M?simpleA( ABa) ox, esexR(tea)nd,Rco ed(ant AB,bain o)lab xese lednullsDecision problemABoxSolutionElena Botoeva(FUB)universal solutionpreserves all modelsuniversal UCQ-solutionpreserves all answers toUnions of Conjunctive QueriesUCQ-representationpreserves all answers to UCQs,independently of the ABoxDescription Logic Knowledge Base Exchange13/33

3. ResultsUniversal solutionsMembershipNon-emptinesssimple ABoxesPTime-completePTime-completeextended ABoxesNP-completePSpace-hard, in ExpTimeUniversal UCQ-solutionsMembershipNon-emptinesssimple ABoxesPSpace-hardin ExpTimeextended ABoxesin -emptinessElena completeDescription Logic Knowledge Base Exchange14/33

3. ResultsUniversal solutionsMembershipNon-emptiness1 e4 e5 2 Nf3 Nc6 3 Bb5 3. . . a6 3. . . Nf6 4 Ba43VrzZ4Wb5 Xq1Tk4 6YP6šYP6YP6šYPz6šYP6YP6šYP13—VR2UN4 WB5XQ1 TKzzZ3VRsimple ABoxesPTime-completePTime-completeextended ABoxesNP-completePSpace-hard, in ExpTime8761 games54abcdefgcircuit value problemUniversal tionsMembershipNon-emptinessElena Botoeva(FUB)ad-hoc2 automata3-colorabilityvalidity of QBFhsimple ABoxesPSpace-hardin ExpTimeextended ABoxesin Space-completeDescription Logic Knowledge Base Exchange14/33

3. ResultsUniversal solutionsMembershipNon-emptinesssimple ABoxesPTime-completePTime-completeextended ABoxesNP-completePSpace-hard, in ExpTimeUniversal UCQ-solutionsMembershipNon-emptinesssimple ABoxesPSpace-hardin ExpTimeextended ABoxesin ExpTimePSpace-hard1 e4 e5 2 Nf3 Nc6 3 Bb5 3. . . a6 3. . . Nf6 4 Ba43VrzZ4Wb5 Xq1Tk4 6YP6šYP6YP6šYPz6šYP6YP6šYP13—VR2UN4 WB5XQ1 TKzzZ3VR8763 game-theoretic54abcdefghvalidity of QBFUCQ-representationsMembershipNon-emptinessElena completeDescription Logic Knowledge Base Exchange14/33

3. ResultsUniversal solutionsMembershipNon-emptinesssimple ABoxesPTime-completePTime-completeextended ABoxesNP-completePSpace-hard, in ExpTimeUniversal UCQ-solutionsMembershipNon-emptinesssimple ABoxesPSpace-hardin ExpTimeextended ABoxesin mplete4 5 graph-theoreticreachability in directed graphsElena Botoeva(FUB)Description Logic Knowledge Base Exchange14/33

3. ResultsUniversal solutionsMembershipNon-emptiness1 e4 e5 2 Nf3 Nc6 3 Bb5 3. . . a6 3. . . Nf6 4 Ba43VrzZ4Wb5 Xq1Tk4 6YP6šYP6YP6šYPz6šYP6YP6šYP13—VR2UN4 WB5XQ1 TKzzZ3VRsimple ABoxesPTime-completePTime-completeextended ABoxesNP-completePSpace-hard, in ExpTime8761 games54abcdefgad-hoc2 automata3-colorabilityvalidity of QBFhcircuit value problemUniversal UCQ-solutionsMembershipNon-emptinesssimple ABoxesPSpace-hardin ExpTime1 e4 e5 2 Nf3 Nc6 3 Bb5 3. . . a6 3. . . Nf6 4 Ba4extended ABoxesin ExpTimePSpace-hard3VrzZ4Wb5 Xq1Tk4 6YP6šYP6YP6šYPz6šYP6YP6šYP13—VR2UN4 WB5XQ1 TKzzZ3VR8763 game-theoretic54abcdefghvalidity of exityNLogSpace-completeNLogSpace-complete4 5 graph-theoreticreachability in directed graphsElena Botoeva(FUB)Description Logic Knowledge Base Exchange14/33

Outline1 Introduction2 Summary of Work3 Results4 Technical DevelopmentUniversal SolutionsUniversal UCQ-solutionsUCQ-representationsElena Botoeva(FUB)Description Logic Knowledge Base Exchange15/33

The Essence of Knowledge Base ExchangeA mapping is a triple M (Σ1 , Σ2 , T12 ),where T12 is a set of DL-Lite R inclusions from Σ1 to Σ2hT1 , A1 i is a DL-Lite R knowledge base over Σ1 (source KB)hT2 , A2 i is a DL-Lite R knowledge base over Σ2 (target KB)Elena Botoeva(FUB)Description Logic Knowledge Base Exchangemapping MΣ11ΣΣ22target signaturesource signatureA1T1D1B1C1A2solutionB2T2C2A1A2source KBtarget KB16/33

The Essence of Knowledge Base ExchangeA mapping is a triple M (Σ1 , Σ2 , T12 ),where T12 is a set of DL-Lite R inclusions from Σ1 to Σ2hT1 , A1 i is a DL-Lite R knowledge base over Σ1 (source KB)hT2 , A2 i is a DL-Lite R knowledge base over Σ2 (target KB)mapping MΣ11ΣΣ22target signaturesource signatureA1T1D1B1C1T2A2solutionB2C2A1A2source KBtarget KBFor a KB K, we denote by UK the canonical model of K (chase in databases). hT2 , A2 i is a universal solution for hT1 , A1 i under M (Σ1 , Σ2 , T12 ) iff?T2 andUA2 is Σ2 -homomorphically equivalent to UhT1 T12 ,A1 i . hT2 , A2 i is a universal UCQ-solution for hT1 , A1 i under M (Σ1 , Σ2 , T12 ) iffUhT2 ,A2 i is finitely Σ2 -homomorphically equivalent to UhT1 T12 ,A1 i . T2 is a UCQ-representation for T1 under M (Σ1 , Σ2 , T12 ) iff?for each source ABox A1 ,UhT2 T12 ,A1 i is Σ2 -homomorphically equivalent to UhT1 T12 ,A1 i .? plus one more condition with little technical impact? plus one more condition for checking consistencyElena Botoeva(FUB)Description Logic Knowledge Base Exchange16/33

The Essence of Knowledge Base ExchangeA mapping is a triple M (Σ1 , Σ2 , T12 ),where T12 is a set of DL-Lite R inclusions from Σ1 to Σ2hT1 , A1 i is a DL-Lite R knowledge base over Σ1 (source KB)hT2 , A2 i is a DL-Lite R knowledge base over Σ2 (target KB)mapping MΣ11ΣΣ22target signaturesource signatureA1T1D1B1C1T2A2solutionB2C2A1A2source KBtarget KBFor a KB K, we denote by UK the canonical model of K (chase in databases). hT2 , A2 i is a universal solution for hT1 , A1 i under M (Σ1 , Σ2 , T12 ) iff?T2 andUA2 is Σ2 -homomorphically equivalent to UhT1 T12 ,A1 i . hT2 , A2 i is a universal UCQ-solution for hT1 , A1 i under M (Σ1 , Σ2 , T12 ) iffUhT2 ,A2 i is finitely Σ2 -homomorphically equivalent to UhT1 T12 ,A1 i . T2 is a UCQ-representation for T1 under M (Σ1 , Σ2 , T12 ) iff?for each source ABox A1 ,UhT2 T12 ,A1 i is Σ2 -homomorphically equivalent to UhT1 T12 ,A1 i .We present our 5 techniques that check the existence of the homomorphisms.? plus one more condition with little technical impact? plus one more condition for checking consistencyElena Botoeva(FUB)Description Logic Knowledge Base Exchange16/33

The Canonical and Generating ModelsLet K hT , Ai, whereElena Botoeva(FUB)Description Logic Knowledge Base Exchange17/33

The Canonical and Generating ModelsLet K hT , Ai, whereA {B(a)}aaBThe canonical model UKBThe generating model GKWe call wR and wS witnesses of K, denoted Wit(K).Moreover, we write, e.g., a K wR , or wR K wS .Elena Botoeva(FUB)Description Logic Knowledge Base Exchange17/33

The Canonical and Generating ModelsLet K hT , Ai, whereA {B(a)}aT {B v RaBRawRThe canonical model UKBRwRThe generating model GKWe call wR and wS witnesses of K, denoted Wit(K).Moreover, we write, e.g., a K wR , or wR K wS .Elena Botoeva(FUB)Description Logic Knowledge Base Exchange17/33

The Canonical and Generating ModelsLet K hT , Ai, whereA {B(a)}aT {B v R R v SaBRawRBRwRSSawR wSThe canonical model UKwSThe generating model GKWe call wR and wS witnesses of K, denoted Wit(K).Moreover, we write, e.g., a K wR , or wR K wS .Elena Botoeva(FUB)Description Logic Knowledge Base Exchange17/33

The Canonical and Generating ModelsLet K hT , Ai, whereA {B(a)}aT {B v R R v S S aBRawRBRwRv SSSawR wSwSSawR wS wSS···The canonical model UKThe generating model GKWe call wR and wS witnesses of K, denoted Wit(K).Moreover, we write, e.g., a K wR , or wR K wS .Elena Botoeva(FUB)Description Logic Knowledge Base Exchange17/33

The Canonical and Generating ModelsLet K hT , Ai, whereA {B(a)}aT {B v R R v SawRBR, QwR S v SR v Q}aBR, QSSawR wSwSSawR wS wSS···The canonical model UKThe generating model GKWe call wR and wS witnesses of K, denoted Wit(K).Moreover, we write, e.g., a K wR , or wR K wS .Elena Botoeva(FUB)Description Logic Knowledge Base Exchange17/33

The Canonical and Generating ModelsLet K hT , Ai, whereA {B(a)}aaT {B v R,Q R v SawR S v SR v Q}awR wS,QwRSSwSSΣ {Q, S}awR wS wSS···The canonical model UK ΣThe generating model GK ΣWe call wR and wS witnesses of K, denoted Wit(K).Moreover, we write, e.g., a K wR , or wR K wS .Elena Botoeva(FUB)Description Logic Knowledge Base Exchange17/33

Outline1 Introduction2 Summary of Work3 Results4 Technical DevelopmentUniversal SolutionsUniversal UCQ-solutionsUCQ-representationsElena Botoeva(FUB)Description Logic Knowledge Base Exchange18/33

Membership for Simple Universal Solutions is in PTimeA2 is a universal solution for hT1 , A1 i under M (Σ1 , Σ2 , T12 ) iff? there exist a Σ2 -homomorphism from UA2 to UhT1 T12 ,A1 i , a Σ2 -homomorphism from UhT1 T12 ,A1 i to UA2 .? plus one more condition of no technical interestElena Botoeva(FUB)Description Logic Knowledge Base Exchange19/33

Membership for Simple Universal Solutions is in PTimeA2 is a universal solution for hT1 , A1 i under M (Σ1 , Σ2 , T12 ) iff? there exist a Σ2 -homomorphism from UA2 to UhT1 T12 ,A1 i ,EASY a Σ2 -homomorphism from UhT1 T12 ,A1 i to UA2 .? plus one more condition of no technical interestElena Botoeva(FUB)Description Logic Knowledge Base Exchange19/33

Membership for Simple Universal Solutions is in PTimeA2 is a universal solution for hT1 , A1 i under M (Σ1 , Σ2 , T12 ) iff? there exist a Σ2 -homomorphism from UA2 to UhT1 T12 ,A1 i ,EASY a Σ2 -homomorphism from UhT1 T12 ,A1 i to UA2 . via Reachability Games on graphs? plus one more condition of no technical interestElena Botoeva(FUB)Description Logic Knowledge Base Exchange19/33

Membership for Simple Universal Solutions is in PTimeA2 is a universal solution for hT1 , A1 i under M (Σ1 , Σ2 , T12 ) iff? there exist a Σ2 -homomorphism from UA2 to UhT1 T12 ,A1 i ,EASY a Σ2 -homomorphism from UhT1 T12 ,A1 i to UA2 . via Reachability Games on graphsFor a KB K, an ABox A, and a signature Σ,we construct a reachability game (G, F ) such thatthere exists a Σ-homomorphism from UK to UAiffDuplicator has a strategy against Spoilerto avoid F in G.? plus one more condition

Description Logic Knowledge Base Exchange Elena Botoeva supervisor: Diego Calvanese PhD Final Examination April 10, 2014 Bolzano Elena Botoeva(FUB)Description Logic Knowledge Base Exchange1/33. Outline 1 Introduction 2 Summary of Work 3 Results 4 Technical Development Universal Solutions Universal UCQ-solutions UCQ-representations Elena Botoeva(FUB)Description Logic Knowledge Base Exchange2/33 .

Related Documents:

Listing Exchange Exchange Exchange Exchange); Exchange Exchange listing Exchange Exchange listing. Exchange Exchange. Exchange ExchangeExchange Exchange .

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

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 .

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

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

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)

3-3 Derived Rules for the Base Logic 3-4 Well-Formed Terms of B, II . 3-5 Equality Axioms of B for Standard Data Types 3-6 Well-Formed Formulae of Lax Logic . 3-7 Structural Rules of Lax Logic 3-8 Induction Rules of Lax Logic . 3-9 Logica.l Inference Rules of Lax Logic 3-10 Constraint Extra.ction for Structural Rules of Lax Logic .

of domestic violence in 2003. Tjaden and Thoennes (2000) found in the National Violence Against Women Survey that 25.5% of women and 7.9% of men self-reported having experienced domestic violence at some point in their lives. Unfortunately, only a small percentage of abused men are willing to speak out in fear of ridicule, social isolation, and humiliation (Barber, 2008). Therefore, because of .