18.11.2004

Multivalued Calculi for Logics Based on Non-determinism

Niedeterministyczne macierze logiczne to wielowartościowe struktury, w których wartość przypisywana przez wartościowanie złożonej formule można wybrać w sposób niedeterministyczny z pewnego niepustego zbioru opcji. Rozważamy dwie semantyki dla logik opartych na takich macierzach: dynamiczna o pełnym niedeterminizmie wyboru wartości, i statyczna o ograniczonym niedeterminizmie wyboru. Używamy metodologii dekompozycyjnej w stylu Rasiowa-Sikorski do otrzymania pełnych systemów dowodzenia dla logik opartych na takich macierzach. Systemy te bazują na zbiorach wielowartościowych formuł znakowanych i można je przedstawić także w formalizmie n - sekwentów. Następnie pokazujemy, jak systemy te można przekształcić w zwykle rachunki sekwentowe bez reguły cięcia dla pewnych dobrze znanych logik.