Wyniki wyszukiwania - BazTech

1

Logika podejmowania decyzji (podejmowanie decyzji w aspekcie klasycznej i kwantowej logiki)

Kałuski J.

Zeszyty Naukowe. Organizacja i Zarządzanie / Politechnika Śląska

|

2012

|

z. 61

191--219

PL

W pracy obszernie omówiono stosowanie logiki kwantowej do podejmowania decyzji na tle logiki klasycznej w szerokim zakresie teoretycznym i praktycznym. Wychodząc od samych początków teorii kwantowej, a więc od eksperymentu myślowego EPR, prac Heisenberga, Bohra, Borna, Schroedingera, von Neumanna, Paulli’ego i innych znakomitych teoretyków fizyki kwantowej lat 20 i 30 ubiegłego stulecia, aż do słynnego twierdzenia J. Bella (1964) i jego nierówności i kończąc eksperymentami A. Aspecta i A. Zeillingera, pokazano skomplikowaną drogę rozwoju logiki kwantowej w podejmowaniu decyzji w naukach kognitywnych, ekonomii i technice. Równolegle analizowano pojęcia logiki klasycznej i kwantowej w aspekcie filozoficznym, począwszy od I. Kanta i jego logiki formalnej, poprzez logikę Łukasiewicza – Tarskiego, kosmologię Jacyny – Onyszkiewicza, aż po filozofię buddyzmu oraz różnych, współczesnych nurtów myślenia „kwantowego”. Do podejmowania decyzji w konkretnych sytuacjach służą modele na bazie kwantowej teorii informacji, kwantowego prawdopodobieństwa a przede wszystkim kwantowej teorii gier. Na przykładach szczegółowych obliczeń prawdopodobieństw kwantowych i budowy strategii kwantowych na użytek gier zobrazowano proces postępowania, który zasadniczo różni się od modelu klasycznego.

EN

In the work some problems of quantum decision making with comparing to the classical logic are presented. Based to Bell’s theorem (1964) and many works of famous physicians as Einstein, Bohr, Heisenberg, Born, Schroedinger, von Neumann and others which hold fast to the concept of new logic, the hard way of development of quantum logic in decision making is discussed. Simultaneously in the paper the I. Kant’s formal logic, Łukasiewicz-Tarski’s truth theory and logic across the Jacyna-Onyszkiewicz’s cosmological theory and Buddism’s philosophy are presented. To decision making in the concrete situations some models of quantum information theory, quantum probability and first of all quantum game are used. On the number of examples according to detailed computing of the quantum probability and construction of the quantum strategies in the games, the methods of calculating are showed. In all mentioned discussion shows that these methods are different from classical methods.

2

Completeness and Soundness Results for χ with Intersection and Union Types

Bakel S. van

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

1-41

EN

With the eye on defining a type-based semantics, this paper defines intersection and union type assignment for the sequent calculus χ, a substitution-free language that enjoys the Curry- Howard correspondence with respect to the implicative fragment of Gentzen's sequent calculus for classical logic. We investigate the minimal requirements for such a system to be complete (i.e. closed under redex expansion), and show that the non-logical nature of both intersection and union types disturbs the soundness (i.e. closed uder reduction) properties. This implies that this notion of intersection-union type assignment needs to be restricted to satisfy soundness as well, making it unsuitable to define a semantics. We will look at two (confluent) notions of reduction, called Call-by-Name and Call-by- Value, and prove soundness results for those.

3

Arithmetical Proofs of Strong Normalization Results for Symmetric [lambda]-calculi

David R., Nour K.

Fundamenta Informaticae

|

2007

|

Vol. 77, nr 4

489-510

EN

We give arithmetical proofs of the strong normalization of two symmetric l-calculi corresponding to classical logic. The first one is the [`(l)]m[(m~)]-calculus introduced by Curien & Herbelin. It is derived via the Curry-Howard correspondence from Gentzen's classical sequent calculus LK in order to have a symmetry on one side between "program" and "context" and on other side between "call-by-name" and "call-by-value". The second one is the symmetric lm-calculus. It is the lm-calculus introduced by Parigot in which the reduction rule m?, which is the symmetric of m, is added. These results were already known but the previous proofs use candidates of reducibility where the interpretation of a type is defined as the fix point of some increasing operator and thus, are highly non arithmetical.

4

Strong normalisation of cut-elimination in clasical logic

Urban C., Bierman G.M.

Fundamenta Informaticae

|

2001

|

Vol. 45, nr 1,2

123-155

EN

In this paper we present a strongly normalising cut-elimination procedure for classical logic. This procedure adapts Gentzen's standard cut-reductions, but is less restrictive than previous strongly normalising cut-elimination procedures. In comparison, for example, with works by Dragalin and Danos et al., our procedure requires no special annotations on formulae and allows cut-rules to pass over other cut-rules. In order to adapt the notion of symmetric reducibility candidates for proving the strong normalisation property, we introduce a novel term assignment for sequent proofs of classical logic and formalise cut-reductions as term rewriting rules.

5

Fast Automatic Deduction

Stępień L.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

2000/2001

|

Vol. 8

89--99