El butlletí de l’Associació Catalana d’Intel·ligència Artificial (ACIA)

Expansions modals de lògiques basades en T-normes

Amanda Vidal

Data de lectura: 29 de setembre de 2015
Directors de la tesi: Félix Bou, Francesc Esteva i Lluís Godo
Programa de doctorat: Universitat de Barcelona.

http://www.tdx.cat/handle/10803/316575


Aquesta tesi s’emmarca en l’àmbit de l’anomenada investigació bàsica, que estudia problemes de la lògica matemàtica que estan a la base del desenvolupament de les branques més aplicades de la computació i la intel·ligència artificial.

Des d’un punt de vista formal, una lògica és simplement un conjunt de parells que representen les deduccions vàlides entre conjunts de fórmules i fórmules d’un llenguatge. Caracteritzar aquest conjunt permet estudiar les seves propietats i en alguns casos automatitzar la generació de deduccions. Els anomenats sistemes sintàctics o axiomàtics es basen en la generació de deduccions a partir d’uns axiomes utilitzant unes regles d’inferència. Per una altra banda, els sistemes semàntics es caracteritzen per establir una interpretació de les fórmules del llenguatge en una estructura matemàtica —una àlgebra, una estructura relacional, etc.— que satisfà un conjunt determinat de propietats, i un criteri per establir la validesa d’una fórmula sota aquella interpretació.

Caracteritzar una lògica tant sintàcticament com semànticament és el que es coneix com demostrar la seva completesa, un dels problemes clàssics de la lògica matemàtica, i és el que aborda la tesi en un cas que combina dues famílies de lògiques no clàssiques ben conegudes: les lògiques modals i les lògiques fuzzy basades en t-normes. Les lògiques modals, intensament estudiades i també aplicades en diversos àmbits de la computació i la intel·ligència artificial (per exemple en sistemes basats en el coneixement o verificació automàtica de software), s’expliquen intuïtivament a través d’una semàntica basada en models relacionals (models de Kripke), i permeten expressar nocions com “necessàriament P” o “eventualment P”. Per altra banda, les lògiques basades en t-normes són lògiques multivaluades que es defineixen semànticament a partir d’àlgebres sobre l’interval real [0,1] (agafat com a conjunt de valors de veritat) amb una t-norma i el seu residu, que interpreten la noció de conjunció i implicació respectivament. Lògiques que combinin ambdós formalismes són, per tant, molt versàtils i ofereixen una gran capacitat expressiva—que permet l’ús de quantificadors limitats i de valors de veritat intermedis.

A la tesi s’aborda l’estudi d’extensions modals de lògiques fuzzy basades en t-normes que satisfacin uns certs requisits de regularitat, entre les quals s’inclou la t-norma producte i moltes altres no estudiades prèviament. El nostre objectiu ha estat, fixada una t-norma, obtenir un sistema axiomàtic recursivament enumerable de la lògica definida semànticament per models de Kripke sobre l’àlgebra a [0,1], definida per la t-norma i el seu residu. Pel que fa a la part no modal, la nostra solució passa primer, entre altres coses, per introduir en el llenguatge constants associades als racionals de [0,1]. A continuació, hem definit un sistema axiomàtic (extensió de la lògica MTL), que inclou una regla d’inferència infinitària, per al qual obtenim completesa forta (i.e. completesa per deduccions a partir d’un conjunt arbitrari de premisses), un requisit essencial per, finalment, encarar amb possibilitat d’èxit l’extensió modal. Aquest problema s’aborda a la segona part de la tesi, on hem provat que el sistema axiomàtic anterior, ampliat amb cinc axiomes modals i una regla d’inferència que només afecta els teoremes de la lògica, és també fortament complet respecte a la lògica modal mencionada prèviament definida per models de Kripke. També s’ha estudiat una semàntica algebraica alternativa i les relacions entre les dues.

Finalment, a la tercera i última part de la tesi, ens hem centrat en el problema d’automatitzar les deduccions (un aspecte clau per a possibles aplicacions) i descrivim el disseny i la implementació d’un solver, mNiBLoS, per a algunes de les lògiques estudiades a la tesi (ens limitem als models de Kripke finits i sobre t-normes continues), utilitzant formalismes i eines desenvolupats en el context dels solvers SMT (Satisfiability Modulo Theories). En el disseny s’han tingut en compte diversos resultats teòrics associats a aquestes lògiques que han resultat en una major eficiència en relació amb solvers previs que tractaven algunes d’aquestes lògiques. També s’ha intentat oferir a l’usuari molta flexibilitat quant al gran ventall de lògiques fuzzy suportades (qualsevol definida per una t-norma continua que l’usuari pugi especificar) i de problemes a resoldre (comprovar si una formula és un teorema de la lògica, si és satisfactible, si una deducció és vàlida, etc.); tot això amb l’objectiu d’acostar aquestes lògiques fuzzy i les corresponents extensions modals a comunitats no especialitzades en lògica però possiblement interessades en la seva aplicació.

El software està disponible a http://www.iiia.csic.es/~amanda/publications.html. Animem a qualsevol interessat a utilitzar-lo a contactar amb els autors per a qualsevol dubte, suggeriment, o possibilitat de col·laboració.

 

  XKCD ens ensenya aplicacions de la lògica matemàtica.



Subscripcions
Vull rebre NODES
Donar-me de baixa
Enviar  Enviar  Enviar
SocisACIA
Usuari
Contrasenya


Si no ets soci de l'ACIA dona't d'alta i gaudeix dels avantatges dels socis

Alta usuari  Alta usuari  Alta usuari

Si has oblidat la teva contrasenya

Recupera contraseña  Recupera contrasenya  Recupera contraseña

© 2012 ACIA - The Catalan Association for Artificial Intelligence | ISSN: 2014-5020 | www.acia.cat | info@acia.cat
IIIA, Campus Universitat Autònoma de Barcelona - 08193 Bellaterra, +34 935809570