Wyniki wyszukiwania - Biblioteka Nauki

Nowa wersja platformy, zawierająca wyłącznie zasoby pełnotekstowe, jest już dostępna.
Przejdź na https://bibliotekanauki.pl

Ograniczanie wyników

Znaleziono wyników: 5

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

A Propositional Programming Environment for Linear Algebra

100%

Srebrny M. , Stępień L.

2007

tom Vol. 81, nr 1-3

325-345

In this paper we present an application of the propositional SATisfiability environment to computing bases of some vector spaces. As a motivation we refer to certain computational tasks in the area of the algebraic theory of quadratic forms; more precisely, in the theory of Witt rings of quadratic forms. As known in algebra, the problem of finding all automorphisms of an elementary Witt ring can be reduced to searching for some special kind of bases of certain vector space over the two-element Galois field. We show how one can code a search for some kind of bases as a propositional formula in such a way that its satisfying valuations code the desired bases. Some encouraging experimental results are reported for the proposed propositional search procedure using the currently best SAT solvers.

SAT as a Programming Environment for Linear Algebra

100%

Srebrny M. , Stępień L.

2010

tom Vol. 102, nr 1

115-127

In this paper we pursue the propositional calculus and the SATisfiability solvers as a powerful declarative programming environment that makes it possible to create and run the propositional declarative programs for computational tasks in various areas of mathematics. We report some experimental results on our application of the propositional SATisfiability environment to computing some simple orthogonal matrices and the orders of some orthogonal groups. Some encouraging (and not very encouraging) experiments are reported for the proposed propositional search procedures using off-the-shelf general-purpose SAT solvers. Our new software toolkit SAT4Alg is announced.

AIgorithms for Sharing a Password

100%

Soroczuk A. , Srebrny M.

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

2000/2001

tom Vol. 8

81--87

A Quantifier-free First-order Knowledge Logic of Authentication

100%

Kurkowski M. , Srebrny M.

2006

tom Vol. 72, nr 1-3

263-282

In this paper we introduce a new, complete and decidable knowledge logic of authentication with a well defined semantics, intended for model checking verification of properties of authentication protocols. It is a version of the old BAN logic but with no belief modality, no modality at all, and with clearly expressible knowledge predicate. The new logic enjoys carefully defined and developed knowledge sets of the participants, with a potential intruder's knowledge and a well defined algorithm of gaining, extracting and generating knowledge. The semantics is provided with a computation structure modelling a considered authentication protocol as a transition system. We provide a sound and complete axiomatization of the new logic and prove its decidability. From a pure mathematical logic standpoint, the new logic is a simple quantifier-free first order extension of the classical propositional calculus, while it is not a typical logic of knowledge, nor is it an extension of the BAN-logic. As the correctness property of an authentication protocol we require that the agents identify themselves by showing that they know the right keys.

Remarks on the Classical Threshold Secret Sharing Schemes

80%

Spież S. , Srebrny M. , Urbanowicz J.

2012

tom Vol. 114, nr 3/4

345-357

We survey some results related to classical secret sharing schemes defined in Shamir [10] and Blakley [1], and developed in Brickell [2] and Lai and Ding [4]. Using elementary symmetric polynomials, we describe in a unified way which allocations of identities to participants define Shamir’s threshold scheme, or its generalization by Lai and Ding, with a secret placed as a fixed coefficient of the scheme polynomial. This characterization enabled proving in Schinzel et al. [8], [9] and Spie˙z et al. [13] some new and non-trivial properties of such schemes. Also a characterization of matrices corresponding to the threshold secret sharing schemes of Blakley and Brickell’s type is given. Using Gaussian elimination we provide an algorithm to construct all such matrices which is efficient in the case of relatively small matrices. The algorithm may be useful in constructing systems where dynamics is important (one may generate new identities using it). It can also be used to construct all possible MDS codes.