Wyniki wyszukiwania - BazTech

1

Lattice Theory for Rough Sets : A Case Study with Mizar

Grabowski A.

Fundamenta Informaticae

|

2016

|

Vol. 147, nr 2/3

223--240

EN

Rough sets offer a well-known approach to incomplete or imprecise data. In the paper I briefly report how this framework was successfully encoded by means of one of the leading computer proof-assistants in the world. The general approach is essentially based on binary relations, and all natural properties of approximation operators can be obtained via adjectives added to underlying relations. I focus on lattice-theoretical aspects of rough sets to enable the application of external theorem provers like EQP or Prover9 as well as to translate them into TPTP format widely recognized in the world of automated proof search. I wanted to have a clearly written, possibly formal, although informal as a rule, paper authored by a specialist from the discipline another than lattice theory. It appeared that Lattice theory for rough sets by Jouni Järvinen (called LTRS for short) was quite a reasonable choice to be a testbed for the current formalisation both of lattices and of rough sets. A popular computerised proof-assistant Mizar was used as a tool, hence all the efforts are available in one of the largest repositories of computer-checked mathematical knowledge, called Mizar Mathematical Library.

2

ACBC-Adequate Association and Decision Rules Versus Key Generators and Rough Sets Approximations

Kryszkiewicz M.

Fundamenta Informaticae

|

2016

|

Vol. 148, nr 1/2

65--85

EN

In this paper, we propose an ACBC-evaluation formula, which delivers a flexible way of formulating different kinds of criteria for association and decision rules. We prove that rules with minimal antecedents that fulfill ACBC-evaluation formulae are key generators, which are patterns of a special type. We also show that a number of types of rough set approximations of decision classes can be expressed based on ACBC-evaluation formulae. We prove that decision rules preserving respective approximations of decision classes are rules that satisfy an ACBC-evaluation formula and that antecedents of such optimal decision rules are key generators, too. A number of properties related to particular measures of association rules and key generators are derived.

3

A Relational Logic for Spatial Contact Based on Rough Set Approximation

Düntsch I., Orłowska E., Wang H.

Fundamenta Informaticae

|

2016

|

Vol. 148, nr 1/2

191--206

EN

In previous work we have presented a class of algebras enhanced with two contact relations representing rough set style approximations of a spatial contact relation. In this paper, we develop a class of relational systems which is mutually interpretable with that class of algebras, and we consider a relational logic whose semantics is determined by those relational systems. For this relational logic we construct a proof system in the spirit of Rasiowa-Sikorski, and we outline the proofs of its soundness and completeness.

4

On Computing Discrete Logarithms in Bulk and Randomness Extractors

Durnoga K., Źrałek B.

Fundamenta Informaticae

|

2015

|

Vol. 141, nr 4

345--366

EN

We prove several results of independent interest related to the problem of computing deterministically discrete logarithms in a finite field. The motivation was to give a number-theoretic construction of a non-malleable extractor improving the solution from the recent paper Privacy Amplification and Non-Malleable Extractors via Character Sums by Dodis et al. There, the authors provide the first explicit example of a non-malleable extractor – a cryptographic primitive that significantly strengthens the notion of a classical randomness extractor. In order to make the extractor robust, so that it runs in polynomial time and outputs a linear number of bits, they rely on a certain conjecture on the least prime in a residue class. In this work we present a modification of their construction that allows to remove that dependency and address an issue we identified in the original development. Namely, it required an additional assumption about feasibility of finding a primitive element of a finite field. As an auxiliary result, we show an efficiently computable bijection between any order M subgroup of the multiplicative group of a finite field and a set of integers modulo M with the provision that M is a smooth number. Also, we provide a version of the baby-step giantstep method for solving multiple instances of the discrete logarithm problem in the multiplicative group of a prime field. It performs better than the generic algorithm when run on a machine without constant-time access to each memory cell, e.g., on a classical Turing machine.

5

A Semantical Analysis of Focusing and Contraction in Intuitionistic Logic

Avellone A., Fiorentini C., Momigliano A.

Fundamenta Informaticae

|

2015

|

Vol. 140, nr 3/4

247--262

EN

Focusing is a proof-theoretic device to structure proof search in the sequent calculus: it provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured in two separate and disjoint phases. Although stemming from proofsearch considerations, focusing has not been thoroughly investigated in actual theorem proving, in particular w.r.t. termination. We present a contraction-free (and hence terminating) focused multisuccedent sequent calculus for propositional intuitionistic logic, which refines the G4ip calculus in the tradition of Vorob’ev, Hudelmeier and Dyckhoff. We prove completeness of the calculus semantically and argue that this offers a viable alternative to other more syntactical means.

6

Probabilistic Constructions of Computable Objects and a Computable Version of Lovász Local Lemma

Rumyantsev A., Shen A.

Fundamenta Informaticae

|

2014

|

Vol. 132, nr 1

1--14

EN

A nonconstructive proof can be used to prove the existence of an object with some properties without providing an explicit example of such an object. A special case is a probabilistic proof where we show that an object with required properties appears with some positive probability in some random process. Can we use such arguments to prove the existence of a computable infinite object? Sometimes yes: following [8], we show how the notion of a layerwise computable mapping can be used to prove a computable version of Lovász local lemma.

7

On the π-calculus and Co-intuitionistic Logic : Notes on Logic for Concurrency and λP Systems

Bellin G., Menti A.

Fundamenta Informaticae

|

2014

|

Vol. 130, nr 1

21--65

EN

We reconsider work by Bellin and Scott in the 1990s on R. Milner and S. Abramsky’s encoding of linear logic in the π-calculus and give an account of efforts to establish a tight connection between the structure of proofs and of the cut elimination process in multiplicative linear logic, on one hand, and the input-output behaviour of the processes that represent them, on the other, resulting in a proof-theoretic account of (a variant of) Chu’s construction. But Milner’s encoding of the linear lambda calculus suggests consideration of multiplicative co-intuitionistic linear logic: we provide a term assignment for it, a calculus of coroutines which presents features of concurrent and distributed computing. Finally, as a test case of its adequacy as a logic for distributed computation, we represent our term assignment as a λP system. We argue that translations of typed functional languages in concurrent and distributed systems (such as π-calculi or λP systems) are best typed with co-intuitionistic logic, where some features of computations match the logical properties in a natural way.

8

On the Computational Interpretation of CKn for Contextual Information Processing

Mendler M., Scheele S.

Fundamenta Informaticae

|

2014

|

Vol. 130, nr 1

125--162

EN

We aim to establish the multi-modal logic CKn as a baseline for a constructive correspondence theory of constructive modal logics. Just like many classical multi-modal logics may be studied as theories of the basic system K obtained by model-theoretic specialisation, we envisage constructive modal logics to be derived as proof-theoretic enrichments of CKn. The system CKn would then act as a core system for constructive contextual reasoning with controlled information flow. In this paper, as a first step towards this goal, we study CKn as a type theory and introduce its computational λ-calculus, λCKn. Extending previous work on CKn, we present a cut-free contextual sequent system in the spirit of Masini’s two-dimensional generalisation of natural deduction and Brünnler’s nested sequents and give a computational interpretation for CKn following the Curry- Howard Correspondence. The associated modal type theory λCKn permits an interpretation for both the modalities □ and ⋄ of CKn as type operators with simple and independent constructors and destructors, which has been missing in the literature. It is shown that the calculus satisfies subject reduction, strong normalisation and confluence. Since normal forms can be characterised by way of a Gentzen-style typing system with sub-formula property, CKn is suitable for proof search in CKn. At the same time, λCKn enjoys natural deduction style typing which is important for programming applications. In contrast to most existing modal type theories, which are obtained as theories of the constructive modal logic S4, CKn is not bound to a particular contextual interpretation. Thus, λCKn constitutes the core of a functional language which provides static type checking of information processing to support safe contextual navigation in relational structures like those treated by description logics. We review some existing work on modal type theories and discuss their relation to λCKn.

9

Old and New Algorithms for Minimal Coverability Sets

Valmari A., Hansen H.

Fundamenta Informaticae

|

2014

|

Vol. 131, nr 1

1--25

EN

Many algorithms for computing minimal coverability sets for Petri nets prune futures. That is, if a newmarking strictly covers an old one, then not just the old marking but also some subset of its successor markings is discarded from search. In this publication, a simpler algorithm that lacks future pruning is presented and proven correct. Its performance is compared with future pruning. It is demonstrated, using examples, that neither approach is systematically better than the other. However, the simple algorithm has some attractive features. It never needs to re-construct pruned parts of the minimal coverability set. It automatically gives most of the advantage of future pruning, if the minimal coverability set is constructed in depth-first or most tokens first order, and if so-called history merging is applied. Some implementation aspects of minimal coverability set construction are also discussed. Some measurements are given to demonstrate the effect of construction order and other implementation aspects.

10

More on Square-free Words Obtained from Prefixes by Permutations

Ochem P.

Fundamenta Informaticae

|

2014

|

Vol. 132, nr 1

109--112

EN

An infinite square-free word w over the alphabet Σ3 = {0, 1, 2} is said to have a k-stem σ if |σ| = k and w = σw1w2· · · where for each i, there exists a permutation πi of Σ3 which extended to a morphism gives wi= πi (σ). Harju proved that there exists an infinite k-stem word for k = 1, 2, 3, 9 and 13 ≤ k ≤ 19, but not for 4 ≤ k ≤ 8 and 10 ≤ k ≤ 12. He asked whether k-stem words exist for each k ≥ 20. We give a positive answer to this question. Currie has found another construction that answers Harju’s question.

11

Monteiro Spaces and Rough Sets Determined by Quasiorder Relations : Models for Nelson algebras

Järvinen J., Radeleczki S.

Fundamenta Informaticae

|

2014

|

Vol. 131, nr 2

205--215

EN

The theory of rough sets provides a widely used modern tool, and in particular, rough sets induced by quasiorders are in the focus of the current interest, because they are strongly interrelated with the applications of preference relations and intuitionistic logic. In this paper, a structural characterisation of rough sets induced by quasiorders is given. These rough sets form Nelson algebras defined on algebraic lattices. We prove that any Nelson algebra can be represented as a subalgebra of an algebra defined on rough sets induced by a suitable quasiorder. We also show that Monteiro spaces, rough sets induced by quasiorders and Nelson algebras defined on T0-spaces that are Alexandrov topologies can be considered as equivalent structures, because they determine each other up to isomorphism.

12

The CHR-based Implementation of the SCIFF Abductive System

Alberti M., Gavanelli M., Lamma E.

Fundamenta Informaticae

|

2013

|

Vol. 124, nr 4

365--381

EN

Abduction is a form of inference that supports hypothetical reasoning and has been applied to a number of domains, such as diagnosis, planning, protocol verification. Abductive Logic Programming (ALP) is the integration of abduction in logic programming. Usually, the operational semantics of an ALP language is defined as a proof procedure. The first implementations of ALP proof-procedures were based on the meta-interpretation technique, which is flexible but limits the use of the built-in predicates of logic programming systems. Another, more recent, approach exploits theoretical results on the similarity between abducibles and constraints. With this approach, which bears the advantage of an easy integration with built-in predicates and constraints, Constraint Handling Rules has been the language of choice for the implementation of abductive proof procedures. The first CHR-based implementation mapped integrity constraints directly to CHR rules, which is an efficient solution, but prevents defined predicates from being in the body of integrity constraints and does not allow a sound treatment of negation by default. In this paper, we describe the CHR-based implementation of the SCIFF abductive proof-procedure, which follows a different approach. The SCIFF implementation maps integrity constraints to CHR constraints, and the transitions of the proof-procedure to CHR rules, making it possible to treat default negation, while retaining the other advantages of CHR-based implementations of ALP proof-procedures.

13

On the Satisfiability Problem for a 4-level Quantified Syllogistic and Some Applications to Modal Logic

Cantone D., Asmundo M. N.

Fundamenta Informaticae

|

2013

|

Vol. 124, nr 4

427--448

EN

We introduce a multi-sorted stratified syllogistic, called 4LQSR, admitting variables of four sorts and a restricted form of quantification over variables of the first three sorts, and prove that it has a solvable satisfiability problem by showing that it enjoys a small model property. Then, we consider the fragments (4LQSR)h of 4LQSR, consisting of 4LQSR-formulae whose quantifier prefixes have length bounded by h ≥⃒ 2 and satisfying certain additional syntactical constraints, and prove that each of them has an NP-complete satisfiability problem. Finally we show that the modal logic K45 can be expressed in (4LQSR)3.