Description Logic: A Formal Foundation For Ontology .

1y ago
40 Views
1 Downloads
3.94 MB
86 Pages
Last View : 17d ago
Last Download : 7m ago
Upload by : Josiah Pursley
Transcription

Description Logic:A Formal Foundation forOntology Languages and ToolsPart 1: LanguagesIan Horrocks ian.horrocks@comlab.ox.ac.uk Information Systems GroupOxford University Computing Laboratory

Contents MotivationBrief review of (first order) logicDescription Logics as fragments of FOLDescription Logic syntax and semanticsBrief review of relevant complexity notionsDescription Logics and OWLOntology applicationsOntologies –v- databases

DL Basics

What Are Description Logics?

What Are Description Logics? Decidable fragments of First Order LogicThank you for listeningAny questions?

What Are Description Logics? A family of logic based Knowledge Representation formalisms– Originally descended from semantic networks and KL-ONE– Describe domain in terms of concepts (aka classes), roles (akaproperties, relationships) and s-on[Quillian, 1967]Mat

What Are Description Logics? Modern DLs (after Baader et al) distinguished by:– Fully fledged logics with formal semantics Decidable fragments of FOL (often contained in C2) Closely related to Propositional Modal/Dynamic Logics & Guarded Fragment– Computational properties well understood (worst case complexity)– Provision of inference services Practical decision procedures (algorithms) for key problems(satisfiability, subsumption, query answering, etc) Implemented systems (highly optimised) The basis for widely used ontology languages

Web Ontology Language OWL (2) recommendation(s) Motivated by Semantic Web activityAdd meaning to web content by annotatingit with terms defined in ontologies Supported by tools and infrastructure– APIs (e.g., OWL API, Thea, OWLink)– Development environments(e.g., Protégé, Swoop, TopBraid Composer, Neon)– Reasoners & Information Systems(e.g., Pellet, Racer, HermiT, Quonto, ) Based on Description Logics (SHOIN / SROIQ)

and now:A Word from our Sponsors

Crash Course in (simplified) FOL Syntax– Non-logical symbols (signature) Constants: Felix, MyMat Predicates(arity): Animal(1), Cat(1), has-color(2), sits-on(2)– Logical symbols: Variables: x, y Operators: Æ, Ç, !, , Quantifiers: 9, 8 Equality: – Formulas:

Crash Course in (simplified) FOL Semantics

Crash Course in (simplified) FOL Semantics

Crash Course in (simplified) FOL SemanticsHerasy!

Crash Course in (simplified) FOL SemanticsWhy should I care about semantics? -- In fact I heard that a little goes a long way!

Crash Course in (simplified) FOL SemanticsWhy should I care about semantics? -- In fact I heard that a little goes a long way!

Crash Course in (simplified) FOL SemanticsWhy should I care about semantics? -- In fact I heard that a little goes a long way!Well, from a philosophical POV, we need to specify therelationship between statements in the logic and theexistential phenomena they describe.

Crash Course in (simplified) FOL SemanticsWhy should I care about semantics? -- In fact I heard that a little goes a long way!Well, from a philosophical POV, we need to specify therelationship between statements in the logic and theexistential phenomena they describe.That’s OK, but I don’t get paid for philosophy.

Crash Course in (simplified) FOL SemanticsWhy should I care about semantics? -- In fact I heard that a little goes a long way!Well, from a philosophical POV, we need to specify therelationship between statements in the logic and theexistential phenomena they describe.That’s OK, but I don’t get paid for philosophy.From a practical POV, in order to specify, buildand test (ontology-based) tools/systems weneed to precisely define relationships (likeentailment) between logical statements – thisdefines the intended behaviour of tools/systems.

Crash Course in (simplified) FOL SemanticsIn FOL we define the semantics in terms of models (a model theory). A model issupposed to be an analogue of (part of) the world being modeled. FOL uses a verysimple kind of model, in which “objects” in the world (not necessarily physical objects)are modeled as elements of a set, and relationships between objects are modeled assets of tuples.

Crash Course in (simplified) FOL SemanticsIn FOL we define the semantics in terms of models (a model theory). A model issupposed to be an analogue of (part of) the world being modeled. FOL uses a verysimple kind of model, in which “objects” in the world (not necessarily physical objects)are modeled as elements of a set, and relationships between objects are modeled assets of tuples.Note that this is exactly the same kind ofmodel as used in a database: objects in theworld are modeled as values (elements) andrelationships as tables (sets of tuples).

Crash Course in (simplified) FOL Semantics– Model: a pair – E.g.,with D a non-empty set and ·I an interpretation

Crash Course in (simplified) FOL Semantics– Evaluation: truth value in a given model M – E.g.,truefalsetruetruetrue

Crash Course in (simplified) FOL Semantics– Evaluation: truth value in a given model M E.g.,truefalsefalsetruetrue

Crash Course in (simplified) FOL Semantics– Given a model M and a formula F, M is a model of F (written M ² F) iffF evaluates to true in M– A formula F is satisfiable iff there exists a model M s.t. M ² F– A formula F entails another formula G (written F ² G) iff every modelof F is also a model of G (i.e., M ² F implies M ² G)E.g.,

Crash Course in (simplified) FOL Semantics– Given a model M and a formula F, M is a model of F (written M ² F) iffF evaluates to true in M– A formula F is satisfiable iff there exists a model M s.t. M ² F– A formula F entails another formula G (written F ² G) iff every modelof F is also a model of G (i.e., M ² F implies M ² G)E.g.,

Decidable Fragments FOL (satisfiability) well known to be undecidable– A sound, complete and terminating algorithm is impossible Interesting decidable fragments include, e.g.,– C2: FOL with 2 variables and Counting quantifiers Counting quantifiers abbreviate pairwise (in-) equalities, e.g.:equivalent toequivalent to– Propositional modal and description logics– Guarded fragment

Back to our ScheduledProgram

DL Syntax Signature– Concept (aka class) names, e.g., Cat, Animal, Doctor Equivalent to FOL unary predicates– Role (aka property) names, e.g., sits-on, hasParent, loves Equivalent to FOL binary predicates– Individual names, e.g., Felix, John, Mary, Boston, Italy Equivalent to FOL constants

DL Syntax Operators– Many kinds available, e.g., Standard FOL Boolean operators (u, t, ) Restricted form of quantifiers (9, 8) Counting ( , ·, )

DL Syntax Concept expressions, e.g.,– Doctor t Lawyer– Rich u Happy– Cat u 9sits-on.Mat Equivalent to FOL formulae with one free variable–––

DL Syntax Special concepts– (aka top, Thing, most general concept)– ? (aka bottom, Nothing, inconsistent concept)used as abbreviations for– (A t A) for any concept A– (A u A) for any concept A

DL Syntax Role expressions, e.g.,–– hasParent hasBrother Equivalent to FOL formulae with two free variables––

DL Syntax “Schema” Axioms, e.g.,– Rich v Poor(concept inclusion)– Cat u 9sits-on.Mat v Happy(concept inclusion)– BlackCat Cat u 9hasColour.Black(concept equivalence)– sits-on v touches(role inclusion)– Trans(part-of)(transitivity) Equivalent to (particular form of) FOL sentence, e.g.,‒ 8x.(Rich(x) ! Poor(x))‒ 8x.(Cat(x) Æ 9y.(sits-on(x,y) Æ Mat(y)) ! Happy(x))‒ 8x.(BlackCat(x) (Cat(x) Æ 9y.(hasColour(x,y) Æ Black(y)))‒ 8x,y.(sits-on(x,y) ! touches(x,y))‒ 8x,y,z.((sits-on(x,y) Æ sits-on(y,z)) ! sits-on(x,z))

DL Syntax “Data” Axioms (aka Assertions or Facts), e.g.,– BlackCat(Felix)(concept assertion)– Mat(Mat1)(concept assertion)– Sits-on(Felix,Mat1)(role assertion) Directly equivalent to FOL “ground facts”– Formulae with no variables

DL Syntax A set of axioms is called a TBox, e.g.:{Doctor v Person,Parent Person u 9hasChild.Person,Note t 9hasChild.Doctor)}HappyParent Parent u 8hasChild.(DoctorFacts sometimes written A set of facts is called an ABox,e.g.:John:HappyParent,John hasChild ld(John,Mary)} A Knowledge Base (KB) is just a TBox plus an Abox– Often written K hT, Ai

The DL Family Many different DLs, often with “strange” names– E.g., EL, ALC, SHIQ Particular DL defined by:– Concept operators (u, t, , 9, 8, etc.)– Role operators (-, , etc.)– Concept axioms (v, , etc.)– Role axioms (v, Trans, etc.)

The DL Family E.g., EL is a well known “sub-Boolean” DL––––Concept operators: u, , 9No role operators (only atomic roles)Concept axioms: v, No role axioms E.g.:Parent Person u 9hasChild.Person

The DL Family ALC is the smallest propositionally closed DL– Concept operators: u,t, , 9, 8– No role operators (only atomic roles)– Concept axioms: v, – No role axioms E.g.:ProudParent Person u 8hasChild.(Doctor t 9hasChild.Doctor)

The DL Family S used for ALC extended with (role) transitivity axioms Additional letters indicate various extensions, e.g.:‒ H for role hierarchy (e.g., hasDaughter v hasChild)‒ R for role box (e.g., hasParent‒‒‒‒‒ hasBrother v hasUncle)O for nominals/singleton classes (e.g., {Italy})I for inverse roles (e.g., isChildOf hasChild–)N for number restrictions (e.g., 2hasChild, 63hasChild)Q for qualified number restrictions (e.g., 2hasChild.Doctor)F for functional number restrictions (e.g., 61hasMother) E.g., SHIQ S role hierarchy inverse roles QNRs

The DL Family Numerous other extensions have been ncrete domains (numbers, strings, etc)DL-safe rules (Datalog-like rules)FixpointsRole value mapsAdditional role constructors (\Å, [, , , id, )Nary (i.e., predicates with arity der

DL SemanticsVia translaton to FOL, or directly using FO model theory:Interpretation function IIndividuals iI 2 ΔIJohnMaryConcepts CI µ ΔILawyerDoctorVehicleRoles rI µ ΔI ΔIhasChildownsInterpretation domain ΔI

DL Semantics Interpretation function extends to concept expressionsin the obvious(ish) way, e.g.:

DL Semantics Given a model M –––––

DL Semantics Satisfiability and entailment– A KB K is satisfiable iff there exists a model M s.t. M ² K– A concept C is satisfiable w.r.t. a KB K iff there exists a modelM hD, ·Ii s.t. M ² K and CI ;– A KB K entails an axiom ax (written K ² ax) iff for every modelM of K, M ² ax (i.e., M ² K implies M ² ax)

DL SemanticsE.g.,T {Doctor v Person, Parent Person u 9hasChild.Person,HappyParent Parent u 8hasChild.(Doctor t 9hasChild.Doctor)}A {John:HappyParent, John hasChild Mary, John hasChild Sally,Mary: Doctor, Mary hasChild Peter, Mary:(· 1 hasChild)‒ K ² John:Person ?‒ K ² Peter:Doctor ?‒ K ² Mary:HappyParent ?– What if we add “Mary hasChild Jane” ?K ² Peter Jane– What if we add “HappyPerson Person u 9hasChild.Doctor” ?K ² HappyPerson v Parent

DL and FOL Most DLs are subsets of C2– But reduction to C2 may be (highly) non-trivial Trans(R) naively reduces to Why use DL instead of C2?– Syntax is succinct and convenient for KR applications– Syntactic conformance guarantees being inside C2 Even if reduction to C2 is non-obvious– Different combinations of constructors can be selected To guarantee decidability To reduce complexity– DL research has mapped out the decidability/complexitylandscape in great detail See Evgeny Zolin’s DL Complexity Analyzerhttp://www.cs.man.ac.uk/ ezolin/dl/

Complexity Measures Taxonomic complexityMeasured w.r.t. total size of “schema” axioms Data complexityMeasured w.r.t. total size of “data” facts Query complexityMeasured w.r.t. size of query Combined complexityMeasured w.r.t. total size of KB (plus query if appropriate)

Complexity Classes LogSpace, PTime, NP, PSpace, ExpTime, etc– worst case for a given problem w.r.t. a given parameter– X-hard means at-least this hard (could be harder);in X means no harder than this (could be easier);X-complete means both hard and in, i.e., exactly this hard e.g., SROIQ KB satisfiability is 2NExpTime-complete w.r.t.combined complexity and NP-hard w.r.t. data complexity Note that:– this is for the worst case, not a typical case– complexity of problem means we can never devise a moreefficient (in the worst case) algorithm– complexity of algorithm may, however, be even higher(in the worst case)

DLs and Ontology Languages

DLs and Ontology Languages ’s OWL 2 (like OWL, DAML OIL & OIL) based on DL– OWL 2 based on SROIQ, i.e., ALC extended withtransitive roles, a role box nominals, inverse roles andqualified number restrictions OWL 2 EL based on EL OWL 2 QL based on DL-Lite OWL 2 EL based on DLP– OWL was based on SHOIN only simple role hierarchy, andunqualified NRs

Class/Concept Constructors

Ontology Axioms An Ontology is usually considered to be a TBox– but an OWL ontology is a mixed set of TBox and ABox axioms

Other OWL Features XSD datatypes and (in OWL 2) facets, e.g.,– integer, string and (in OWL 2) real, float, decimal, datetime, – minExclusive, maxExclusive, length, – PropertyAssertion( hasAge Meg "17" xsd:integer )– DatatypeRestriction( xsd:integer xsd:minInclusive "5" xsd:integerxsd:maxExclusive "10" xsd:integer )These are equivalent to (a limited form of) DL concrete domains Keys– E.g., HasKey(Vehicle Country LicensePlate) Country License Plate is a unique identifier for vehiclesThis is equivalent to (a limited form of) DL safe rules

OWL RDF/XML Exchange SyntaxE.g., Person u 8hasChild.(Doctor t 9hasChild.Doctor): owl:Class owl:intersectionOf rdf:parseType " collection" owl:Class rdf:about "#Person"/ owl:Restriction owl:onProperty rdf:resource "#hasChild"/ owl:allValuesFrom owl:unionOf rdf:parseType " collection" owl:Class rdf:about "#Doctor"/ owl:Restriction owl:onProperty rdf:resource "#hasChild"/ owl:someValuesFrom rdf:resource "#Doctor"/ /owl:Restriction /owl:unionOf /owl:allValuesFrom /owl:Restriction /owl:intersectionOf /owl:Class

Complexity/Scalability From the complexity navigator we can see that:– OWL (aka SHOIN) is NExpTime-complete– OWL Lite (aka SHIF) is ExpTime-complete (oops!)– OWL 2 (aka SROIQ) is 2NExpTime-complete– OWL 2 EL (aka EL) is PTIME-complete (robustly scalable)– OWL 2 RL (aka DLP) is PTIME-complete (robustly scalable) And implementable using rule based technologiese.g., rule-extended DBs– OWL 2 QL (aka DL-Lite) is in AC0 w.r.t. size of data same as DB query answering -- nice!

Why (Description) Logic? OWL exploits results of 20 years of DL research– Well defined (model theoretic) semantics

Why (Description) Logic? OWL exploits results of 20 years of DL research– Well defined (model theoretic) semantics– Formal properties well understood (complexity, decidability)I can’t find an efficient algorithm, but neither can all these famous people.[Garey & Johnson. Computers and Intractability: A Guide to the Theoryof NP-Completeness. Freeman, 1979.]

Why (Description) Logic? OWL exploits results of 20 years of DL research– Well defined (model theoretic) semantics– Formal properties well understood (complexity, decidability)– Known reasoning algorithms

Why (Description) Logic? OWL exploits results of 20 years of DL research– Well defined (model theoretic) semantics– Formal properties well understood (complexity, decidability)– Known reasoning algorithms– Scalability demonstrated by implemented systems

Tools, Tools, ToolsMajor benefit of OWL has been huge increase in rangeand sophistication of tools and infrastructure:

Tools, Tools, ToolsMajor benefit of OWL has been huge increase in rangeand sophistication of tools and infrastructure: Editors/development environments

Tools, Tools, ToolsMajor benefit of OWL has been huge increase in rangeand sophistication of tools and infrastructure: Editors/development environments ReasonersHermitKAON2PelletCEL

Tools, Tools, ToolsMajor benefit of OWL has been huge increase in rangeand sophistication of tools and infrastructure: Editors/development environments Reasoners Explanation,justificationand pinpointing

Tools, Tools, ToolsMajor benefit of OWL has been huge increase in rangeand sophistication of tools and infrastructure: Editors/development environments Reasoners Explanation,justificationand pinpointing Integration andmodularisation

Tools, Tools, ToolsMajor benefit of OWL has been huge increase in rangeand sophistication of tools and infrastructure: Editors/development environments Reasoners Explanation,justificationand pinpointing Integration andmodularisation APIs, in particular the OWL API

Motivating Applications OWL playing key role in increasing number & range of applications– eScience, medicine, biology, agriculture, geography, space, manufacturing,defence, – E.g., OWL tools used to identify and repair errors in a medical ontology:“would have led to missed test results if not corrected”Experience of OWL in use has identified restrictions:– on expressivity– on scalabilityThese restrictions are problematic in some applicationsResearch has now shown how some restrictions can be overcome– W3C OWL WG is updating OWL accordingly

Motivating Applications OWL playing key role in increasing number & range of applications– eScience, geography, medicine, biology, agriculture, geography, space,manufacturing, defence, – E.g., OWL tools used to identify and repair errors in a medical ontology:“would have led to missed test results if not corrected”Experience of OWL in use has identified restrictions:– on expressivity– on scalabilityThese restrictions are problematic in some applicationsResearch has now shown how some restrictions can be overcome– W3C OWL WG is updating OWL accordingly

Motivating Applications OWL playing key role in increasing number & range of applications– eScience, geography, engineering, , medicine, biology, agriculture, geography,space, manufacturing, defence, – E.g., OWL tools used to identify and repair errors in a medical ontology:“would have led to missed test results if not corrected”Experience of OWL in use has identified restrictions:– on expressivity– on scalabilityThese restrictions are problematic in some applicationsResearch has now shown how some restrictions can be overcome– W3C OWL WG is updating OWL accordingly

Motivating Applications OWL playing key role in increasing number & range of applications– eScience, geography, engineering, medicine, medicine, biology, agriculture,geography, space, manufacturing, defence, – E.g., OWL tools used to identify and repair errors in a medical ontology:“would have led to missed test results if not corrected”Experience of OWL in use has identified restrictions:– on expressivity– on scalabilityThese restrictions are problematic in some applicationsResearch has now shown how some restrictions can be overcome– W3C OWL WG is updating OWL accordingly

Motivating Applications OWL playing key role in increasing number & range of applications– eScience, geography, engineering, medicine, biology e, biology, agriculture,geography, space, manufacturing, defence, – E.g., OWL tools used to identify and repair errors in a medical ontology:“would have led to missed test results if not corrected”Experience of OWL in use has identified restrictions:– on expressivity– on scalabilityThese restrictions are problematic in some applicationsResearch has now shown how some restrictions can be overcome– W3C OWL WG is updating OWL accordingly

Motivating Applications OWL playing key role in increasing number & range of applications– eScience, geography, engineering, medicine, biology, defence, e, biology,agriculture, geography, space, manufacturing, defence, – E.g., OWL tools used to identify and repair errors in a medical ontology:“would have led to missed test resu

Description Logic: A Formal Foundation for Ontology Languages and Tools Ian Horrocks Information Systems Group Oxford University Computing Laboratory Part 1: Languages . Contents Motivation Brief review of (first order) logic Description Logics as fragments of FOL Description Logic syntax and semantics Brief review of relevant complexity .

Related Documents:

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 .

About the Open Logic Project The Open Logic Text is an open-source, collaborative textbook of formal meta-logic and formal methods, starting at an intermediate level (i.e., after an intro-ductory formal logic course). Though aimed at a non-mathematical audience (in particular, stud

"Meta-logic" is so-called because it is the discipline that studies logic itself. Logic proper is concerned with canons of valid inference, and its sym-bolic or formal version presents these canons using formal lan-guages, such as those of propositional and predicate, a.k.a., first-order logic. Meta-logic investigates the properties of .

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 .

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)

I first learned formal logic from Michael Byrd at UW-Madison, using Lemmon’s Beginning Logic, and first taught logic in 2008 as a teaching assistant for Branden Fitelson at UC Berkeley, using Forbes’ Modern Logic. When I s

review some important logical systems, from simple propositional logic to higher-order and modal predicate logic. PROPOSITIONAL LOGIC Study of formal logic now usually starts with propositional logic, in which arguments are analyzed in terms of complete propositions , which (ignoring various complications) we can take to be the

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

The PLC logic programmable logic relay system consists of PLC-V8C logic modules, elec-tromechanical relays, solid-state relays or analog terminal blocks from the PLC-INTER-FACE series, and the LOGIC programming software. The PLC-V8C logic modul

Animals Clifton B. & Anne Batchelder Foundation, Gifford Foundation Inc., Lied Foundation Trust Arts Ethel S. Abbott Charitable Foundation, Burlington Capital Foundation, Baer Foundation, The Theodore G. Baldwin Foundation, Blair Area Community Foundation, Cooper Foundation, Ford Foundation, Ike & Roz

Lenzmeier Family Foundation Susan G. Komen Breast Cancer Foundation 25,000 — 49,999 Broadway Cares/Equity Fights AIDS Frey Foundation Hope Chest for Breast Cancer Foundation 10,000 — 24,999 F.R. Bigelow Foundation Hope Chest for Breast Cancer Foundation HRK Foundation John Mondati Foundation Pohlad Family Foundation Randy Shaver Foundation

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 .

3 Predicate Logic 4 Theorem Proving, Description Logics and Logic Programming 5 Search Methods 6 CommonKADS 7 Problem Solving Methods 8 Planning 9 Agents 10 Rule Learning 11 Inductive Logic Programming 12 Formal Concept Analysis 13 Neural Networks 14 Semantic Web and Exam Preparation . www.sti-innsbruck.at Agenda Motivation Technical Solution – Introduction to Theorem Proving .

2. Lubin-Tate spaces 45 2.1. The height of a formal A-module 46 2.2. Lubin-Tate spaces via formal group laws 49 2.3. Lazard's theorem for formal A-modules 52 2.4. Proof of the lemma of Lazard and Drinfeld 60 2.5. Consequences for formal A-modules 66 2.6. Proof of representability of Lubin-Tate spaces 76 3. Formal schemes 82 3.1. Formal .

Formal Methods: Analogy with Engineering Math (ctd.) Formal methods: same idea, applied to computational systems The applied math of Computer Science is formal logic So the models are formal descriptions in some logical system E.g., a program reinterpreted as a mathematical formula rather than instructions to a machine And calculation is mechanized by automated deduction:

down your commitment to practice jazz piano, tell it to others, and schedule in specific practice times. MONTH ONE: Jazz Piano 101 A. Chord types (Play each in all keys) 2 B. Quick Fix Voicing C. ETUDE: (Quick fix voicings with inversions for better voice leading) ALL MUSICAL EXAMPLES TAKEN FROM “JAZZ PIANO HANDBOOK” (ALFRED PUBLISHING) AND USED WITH PERMISSION MONTH TWO: Position .