Proof Systems for Logics Based on Non-deterministic Multiple-valued Structures

• Autorzy: Avron A. , Konikowska B.
• Języki publikacji: EN

Abstrakty

EN

Non-deterministic matrices (Nmatrices) are multiple-valued structures in which the value assigned by a valuation to a complex formula can be chosen non-deterministically out of a certain nonempty set of options. We consider two different types of semantics which are based on Nmatrices: the dynamic one and the static one (the latter is new here). We use the Rasiowa-Sikorski (R-S) decomposition methodology to get sound and complete proof systems employing finite sets of mv-signed formulas for all propositional logics based on such structures with either of the above types of semantics. Later we demonstrate how these systems can be converted into cut-free ordinary Gentzen calculi which are also sound and complete for the corresponding non-deterministic semantics. As a by-product, we get new semantic characterizations for some well-known logics (like the logic CAR from [18, 28]).

PL

Macierze niedeterministyczne to wielowartościowe struktury, w których wartość przypisaną przez wartościowanie złożonej formule można wybrać w niedeterministyczny sposób z pewnego niepustego zbioru opcji. Opracowujemy ogólne dedukcyjne systemy dowodzenia dla logik opartych na tych strukturach z użyciem mechanizmu n-sekwentów oraz dekompozycyjnej metodologii R-S. Później pokazujemy, jak można użyć tych systemów do uzyskania zwykłych rachunków Gentzenowskich bez reguły cięcia dla pewnych dobrze znanych logik tolerujących sprzeczność.

Słowa kluczowe

EN

formal logics; non-deterministic matrices; deduction systems; logiki formalne

PL

macierze niedeterministyczne; systemy dedukcyjne

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2004
• Tom: Nr 976
• Strony: 1--26
• Opis fizyczny: Bibliogr. 16 poz.

Twórcy

autor

Avron A.

• School of Computer Science, Tel-Aviv University, Ramat-Aviv 69978, Israel

autor

Konikowska B.

• Institute of Computer Science Polish Academy of Sciences Ordona 21, 01-237 Warsaw. Poland

Bibliografia

• [1] A. Avron and I. Lev, Non-Deterministic Multiple-valued Structures, Submitted to the Journal of Symbolic Logic
• [2] A. Avron and I. Lev, Canonical Propositional Gentzen-Type Systems, in Proceedings of the 1st International Joint Conference on An tornated Reasoning (IJCAR 2001) (R. Gore, A Leitsch, T. Nipkow Eds), LNAI 2C83, 529-544, Springer Verlag, 2001.
• [3] D. Batens, K. De Clercq, and N. Kurtonina, Embedding and interpolation for some paralogies. The propositional Case, Reports on Mathematica Logic 33 (1999), 29-44.
• [4] M. Baaz, C.G. Fermuller, and G. Salzer, Automated deduction for many valued logics, in Handbook of Automated Reasoning (Robinson, A and Voronkov, A. eds.), 1355-1400, Elsevier Science Publishers, 2000.
• [5] M. Baaz, C.G. Fermiiller, and R. Zach, Elimination of Cuts in First-ode 1 Finite-valued Logics, Information Processing Cybernetics 29 (1994), 333 355.
• [6] H. B. Curry, Foundations of Mathematical Logic, McGraw-Hill, 1961
• [7] N.C.A. da Costa and J.-Y. Beziau, Carnot’s Logic, Bulletin of the Section of Logic, 22/3 (1993), 98-105.
• [8] J. M. Crawford and D. W. Etherington, A Non-deterministic Semantia for Tractable Inference, in Proc. of the 15tli International Conference on Artificial Intelligence and the 10th Conference on Inno vative Applications of Artificial Intelligence, 286-291, MIT Press, Cambridge, 1998.
• [9] W. A. Carnielli and J. Marcos, A Taxonomy of C-systems, in Paracon- sistency — the logical way to the inconsistent (W. A. Carnielli, M. E. Coniglio, 1. L. M. D’ottaviano, eds.), Lecture notes in pure and applied Mathematics, 1-99, Marcell Dckker, 2002.
• [10] R. Hähnle, Tableaux for multiple-valued, logics, in Handbook of Tableau Methods (D’Agostiuo, M., Gabbay, D.M., Hähnle, R. and Posegga, J. eds.), 529-580, Kluwer Publishing Company, 1999.
• [11] B. Konikowska, Rasiowa-Sikorski deduction systems in computer science applications, Theoretical Computer Science 286 (2002), pp. 323-266.
• [12] M. Nowak, A Note on the Logic CAR of da Costa and Beziau, Bulletin of the Section of Logic, 28/1 (1999), 43-49
• [13] G. Rousseau, Sequents in many-valued logics /, Fundamenta Mathematica LX (1967), 23-33.
• [14] H. Rasiowaand R. Sikorski, The Mathematics of Metamathematics, PWN (Polish Scientific Publishers), Warsaw 1963.
• [15] K. Schröter, Methoden zur Axiomatisierung beliebiger Aussagen- und Prädikatenkalkle, Zeitschrift für math. Logik und Grundlagen der Mathe¬matik 1 (1955), 241-251.
• [16] R. Zach, Proof Theory of Finite-valued Logics, Master’s thesis, Technische Universität Wien, 1993 (Available as Technical Report TUW-E185.2-Z.1- 93).