Okres realizacji: od kwietnia 2012 do marca 2014

Projekt „Logika liniowa z dystrybutywnością oraz jej zastosowanie w automatycznej kompozycji usług sieciowych” jest projektem badawczym finansowanym przez MNiSW (nr projektu: 0265/IP3/2011/71). Kierownikiem projektu jest dr Michał Kozak, członek Zespołu Bibliotek Cyfrowych PCSS.

Logika liniowa, blisko spokrewniona z modelowaniem procesów współbieżnych, znalazła już zastosowanie w automatycznej kompozycji usług sieciowych. Odszukanie właściwej kompozycji usług atomowych jest jednak bardzo złożone ze względu na złożoność dedukcji w tej logice. Wydaje się, że proces ten można by nieco uprościć przekształcając (z wykorzystaniem  prawa dystrybutywności) modalności logiki liniowej na formuły zbudowane za pomocą koniunkcji addytywnej. Projekt ten ma za zadanie zbadanie tego problemu, opracowanie odpowiedniego systemu dowodzenia w stylu Gentzena, jego implementację oraz implementację prototypu systemu kompozycji usług atomowych (opisywanych za pomocą ontologii OWL-S).