Implementacja systemu wnioskującego za pomocą DNA

Obliczenia DNA (z ang. DNA computing) są nowatorską dziedziną nauki, leżącą na pograniczu informatyki i biologii molekularnej. Przedmiotem jej badań są komputery biomolekularne, które w przyszłości mogą stanowić alternatywę dla tradycyjnych systemów komputerowych. Mają one ogromny potencjał ze względu na masowość i równoległość obliczeń. Narzędziem, wykorzystywanym do rozwiązywania problemów algorytmicznych, matematycznych czy logicznych, są tu łańcuchy DNA, a same obliczenia przeprowadzane są w odpowiednich warunkach laboratoryjnych za pomocą operacji biochemicznych. Siła tych obliczeń nie tkwi w ich prędkości a w masowej równoległości operacji, dzięki czemu problemy o naprawdę dużej złożoności mogą być rozwiązywane przy sensownych ograniczeniach czasowych. W trakcie rozwoju (od 1994 roku) w obliczeniach DNA wyodrębniło się wiele gałęzi. Między innymi: 1. rozwiązania za pomocą DNA wielu problemów informatycznych np. drogi Hamiltona, SAT problemu itp.; 2. implementacje za pomocą DNA teoretycznych modeli komputerów: automatów skończonych, automatów ze stosem, maszyn Turinga, sieci logicznych itp.; 3. implementacje za pomocą DNA systemów wnioskowań znanych z logiki. Przedstawiona rozprawa doktorska dotyczy trzeciego tematu. Najprostszym systemem formalnym logiki matematycznej jest klasyczny rachunek zdań. Bada on zbiór zdań elementarnych (zwanych atomowymi), które mogą przyjmować tylko dwie wartości: prawdy lub fałszu, oraz powstający z nich (za pomocą spójników logicznych) zbiór zdań złożonych. W otaczającym nas świecie często spotykamy się z następującym problemem: dany jest układ skończony zdań złożonych A (mogą to być dowolne zdania, niekoniecznie tautologie). Traktujemy je jako specyficzne aksjomaty czyli zdania, które uznajemy w danym układzie za prawdziwe. Wówczas dla dowolnego zdania p pytamy czy wynika ono z A za pomocą reguł wnioskowania, czyli czy p jest konsekwencją zdań z A. Realizacja rozwiązania tego problemu za pomocą łańcuchów DNA i operacji na nich jest głównym celem tej pracy. W rozdziale 1 omówione zostały wiadomości wstępne dotyczące logiki matematycznej i klasycznego rachunku zdań w odniesieniu do prezentowanej koncepcji systemu wnioskującego. Rozdział 2 stanowi wprowadzenie do obliczeń DNA, prezentuje podstawowe modele konstrukcji biokomputerów i przedstawia niektóre prace z rozwoju tej dziedziny. W rozdziale 3 omówione zostały istniejące wcześniej koncepcje związane z implementacją logiki i wnioskowania za pomocą DNA. Rozdział 4 bardzo szczegółowo omawia wszystkie elementy nowej koncepcji. Rozdziały 5 i 6 stanowią uzupełnienie rozdziału 4. Rozdział 5 zawiera analizę poprawności oraz istniejących ograniczeń, a także omawia dodatkowe zastosowania systemu (m. in. koncepcja częściowego rozwiązania problemu SAT oraz obliczanie wartości funkcji logicznych) i możliwości dalszego rozwoju. Rozdział 6 szczegółowo opisuje wszystkie kroki eksperymentu laboratoryjnego. Niektóre wyniki rozprawy były prezentowane w publikacjach i na konferencjach.

DNA computing is an innovative interdisciplinary field which combines elements of molecular biology with computer sciences and mathematics. It investigates biomolecular computers which can be one of the future alternatives to the traditional computer systems. It holds a great potential for massively parallel computation, which is one of the inherent characteristics of operating on DNA molecules. These DNA chains are used to solve algorithmic, mathematical or logical problems, through biochemical operations in laboratory environments. The compactness and reactivity of DNA strands allow for massive amounts of simultaneous parallel processing, which potentially allows us to find solutions to problems with huge computational complexity in sensible time constraints. Since the beginning of the field (starting in 1994) there are many different directions in DNA computing. Among others: 1. solving with DNA many well-known algorithmic problems i.e. Hamiltonian path problem, SAT problem etc.; 2. DNA implementations of theoretical computer models: finite automatons, push-down automatons, Turing machine, logical networks etc.; 3. DNA implementations of inference systems known from mathematical logic. Presented thesis belongs to the third theme. The simplest formal logic system in mathematics is the classical propositional calculus. It investigates a set of logical statements, each of which can assume only one of two possible values: true or false. Propositional calculus also explores the set of composite expressions formed from these basic statements by the use of logic connectives. A common real world problem is whether we can deduce a certain conclusion p from a given set of statements A. Our set A consists of a finite amount of assertions treated as axioms which can include tautologies, but not necessarily so. We can then pose a question if some arbitrary statement p can be derived from A by rules of logical inference. The main aim of this thesis is the realisation of this type of system with DNA molecules. Chapter 1 is an introduction to mathematical logic and propositional calculus which are used by the proposed biochemical logic inference system. Chapter 2 contains preliminary facts about DNA computing. It includes descriptions of basic models of bio-computers and brief explanations of the most important concepts from this field. Chapter 3 describes previous attempts at implementation of logic and reasoning systems by DNA molecules. Chapter 4 meticulously presents all the elements of the new biochemical inference system concept. Chapters 5 and 6 complement the previous one. Chapter 5 analyse the correctness and limitations of the proposed system and presents additional applications of it (partial solving of the SAT problem and logical functions implementation) and future improvement possibilities. Chapter 6 precisely describes all the steps of laboratory experiment. Some of the results were previously published and shown at the conferences.