Wyniki wyszukiwania - BazTech

1

A generalized Suzuki-Berinde contraction that characterizes Banach spaces

Abbas Mujahid, Anjum Rizwan, Rakočević Vladimir

Journal of Applied Analysis

|

2023

|

Vol. 29, nr 2

239--250

EN

We introduce a large class of contractive mappings, called Suzuki-Berinde type contraction. We show that any Suzuki-Berinde type contraction has a fixed point and characterizes the completeness of the underlying normed space. A fixed point theorem for multivalued mappings is also obtained. These results unify, generalize and complement various known comparable results in the literature.

2

The weak eigenfunctions of boundary-value problem with symmetric discontinuities

Olğar Hayati, Mukhtarov Oktay S., Muhtarov Fahreddin S., Aydemir Kadriye

Journal of Applied Analysis

|

2022

|

Vol. 28, nr 2

275--283

EN

The main goal of this study is the investigation of discontinuous boundary-value problems for second-order differential operators with symmetric transmission conditions.We introduce the new notion of weak functions for such type of discontinuous boundary-value problems and develop an operator-theoretic method for the investigation of the spectrum and completeness property of the weak eigenfunction systems. In particular, we define some self-adjoint compact operators in suitable Sobolev spaces such that the considered problem can be reduced to an operator-pencil equation. The main result of this paper is that the spectrum is discrete and the set of eigenfunctions forms a Riesz basis of the suitable Hilbert space.

3

A Propositional Metric Logic with Fixed Finite Ranges

Djordjević Radosav, Ikodinović Nebojša, Stojanović Nenad

Fundamenta Informaticae

|

2020

|

Vol. 174, nr 2

185--199

EN

The aim of this article is developing a formal system suitable for reasoning about the distance between propositional formulas. We introduce and study a formal language which is the extension of the classical propositional language obtained by adding new binary operators D≤s and D≥s , s ∈ Range, where Range is a fixed finite set. In our language it is allowed to make formulas of the form D≤s (α ; β ) with the intended meaning ’distance between formulas α and β is less than or equal to s ’. The semantics of the proposed language consists of possible worlds with a distance function defined between sets of worlds.

4

The Duality of Classical Intersection and Union Types

Downen Paul, Ariola Zena M., Ghilezan Silvia

Fundamenta Informaticae

|

2019

|

Vol. 170, nr 1-3

39--92

EN

For a long time, intersection types have been admired for their surprising ability to complete the simply typed lambda calculus. Intersection types are an example of an implicit typing feature which can describe program behavior without manifesting itself within the syntax of a program. Dual to intersections, union types are another implicit typing feature which extends the completeness property of intersection types in the lambda calculus to full-fledged programming languages. However, the formalization of union types can easily break other desirable meta-theoretical properties of the type system. But why should unions be troublesome when their dual, intersections, are not? We look at the issues surrounding the design of type systems for both intersection and union types through the lens of duality by formalizing them within the symmetric language of the classical sequent calculus. In order to formulate type systems which have all of our properties of interest—soundness, completeness, and type safety—we also look at the impact of evaluation strategy on typing. As a result, we present two dual type systems—one for call-by-value and one for call-by-name evaluation—which have all three properties. We also consider the possibility of classical non-deterministic evaluation, for which there is a choice between two different systems depending on which properties are desired: a full type system which is complete, and a simplified type system which is sound and type safe.

5

Algorithmic Completeness of Imperative Programming Languages

Marquer Yoann

Fundamenta Informaticae

|

2019

|

Vol. 168, nr 1

51--77

EN

According to the Church-Turing Thesis, effectively calculable functions are functions computable by a Turing machine. Models that compute these functions are called Turing-complete. For example, we know that common imperative languages (such as C, Ada or Python) are Turing complete (up to unbounded memory). Algorithmic completeness is a stronger notion than Turing-completeness. It focuses not only on the input-output behavior of the computation but more importantly on the step-by-step behavior. Moreover, the issue is not limited to partial recursive functions, it applies to any set of functions. A model could compute all the desired functions, but some algorithms (ways to compute these functions) could be missing (see [10, 27] for examples related to primitive recursive algorithms). This paper’s purpose is to prove that common imperative languages are not only Turing-complete but also algorithmically complete, by using the axiomatic definition of the Gurevich’s Thesis and a fair bisimulation between the Abstract State Machines of Gurevich (defined in [16]) and a version of Jones’ While programs. No special knowledge is assumed, because all relevant material will be explained from scratch.

6

On Axiomatizability of the Multiplicative Theory of Numbers

Salehi S.

Fundamenta Informaticae

|

2018

|

Vol. 159, nr 3

279--296

EN

The multiplicative theory of a set of numbers (which could be natural, integer, rational, real or complex numbers) is the first-order theory of the structure of that set with (solely) the multiplication operation (that set is taken to be multiplicative, i.e., closed under multiplication). In this paper we study the multiplicative theories of the complex, real and (positive) rational numbers. These theories (and also the multiplicative theories of natural and integer numbers) are known to be decidable (i.e., there exists an algorithm that decides whether a given sentence is derivable form the theory); here we present explicit axiomatizations for them and show that they are not finitely axiomatizable. For each of these sets (of complex, real and [positive] rational numbers) a language, including the multiplication operation, is introduced in a way that it allows quantifier elimination (for the theory of that set).

7

Jakość danych OpenStreetMap – analiza informacji o budynkach na terenie Siedlecczyzny

Nowak-DaCosta J., Bielecka E., Całka B.

Roczniki Geomatyki

|

2016

|

T. 14, z. 2(72)

201--211

PL

Jakość danych OpenStreetMap (OSM), a w szczególności takie jej elementy ilościowe jak kompletność oraz dokładność położenia, wzbudza szerokie zainteresowanie naukowców na świecie. W artykule przedstawiono potencjalne okoliczności powszechnie obserwowanej heterogenicznej charakterystyki OSM, zwracając uwagę na aspekt niedoskonałości ustaleń semantycznych i założeń jakościowych inicjatywy oddolnej jaką jest OpenStreetMap. Część praktyczną badań stanowi ocena kompletności i dokładności lokalizacji danych o budynkach i budowlach OSM w stosunku do krajowych danych urzędowych, bazy danych obiektów topograficznych BDOT10k. Analizy zostały przeprowadzone dla peryferyjnie położonego, powiatu siedleckiego i miasta Siedlce. Opracowanie dopełnia dotychczasowe rezultaty badawcze w zakresie analiz ilościowych jakości OSM, a otrzymane wyniki potwierdzają zróżnicowaną jakość danych o budynkach, w sensie ich kompletności i wypełnienia wartościami ich atrybutów oraz dokładności lokalizacji, także na terenie Polski. Niemniej jednak, wyniki analizy dokładności geometrycznej są zaskakująco dobre. W dyskusji autorzy zwracają uwagę na fakt, że mimo niedoskonałości danych wolnych i otwartych są one powszechnie wykorzystywane przez użytkowników, do których należy także administracja publiczna.

EN

Researchers all over the world are interested in OpenStreetMap data and its quality including completeness and geometric accuracy. This article looks into the commonly observed heterogeneous characteristics of OpenStreetMap geospatial data and draws attention to the vague semantic and quality foundations of this important grass-roots initiative. The experiment is an assessment of the completeness and positional accuracy of OSM building data compared to the national data: the Database of Topographic Objects in Poland (BDOT10k). The analysis was performed for the county and city of Siedlce. This study complements previous research results in the quantitative analysis of OpenStreet- Map data quality. The results confirm the variable quality of OSM data in terms of completeness and updating of building information found in their attribute's, and the positional accuracy of building corners even for the Polish territory. Nevertheless, the analysis did find that the positional accuracy of the OpenStreetMap building data was very good in comparison to the BDOT10K database. The authors draw attention to the fact that Free and Open geospatial data, despite its imperfections, is widely adopted by users including public administrations.

8

The Sufficient Criteria For Consistent Modelling Of The Use Case Realization Diagrams With A New Functional-Structure- Behaviour UML Diagram

Niepostyn S.

Przegląd Elektrotechniczny

|

2015

|

R. 91, nr 2

31-35

EN

UML activity diagrams are primarily used to visualise scenarios. The verification of activity diagrams consistency is subsequently needed to identify errors in requirements at the early stage of the development process. The consistency verification is difficult due to a semi-formal nature of activity diagrams. We propose to extend the activity diagram to the new Functional-Structure-Behaviour (FSB) UML diagram to enable automatic verification of consistency of scenarios of the visualized use cases. Moreover the FSB UML diagram enables simultaneous modelling of the functionality, of the structure and of the behaviour of the target system model. Thus the proposed Functional-Structure-Behaviour UML activity diagram enables consistent and complete models to be developed from scenarios. Furthermore the FSB UML activity diagram can be used for automatic generation of complete workflow applications without any manual programming.

PL

Diagramy aktywności UML używane są przede wszystkim do wizualizacji scenariuszy. W celu wyeliminowania błędów w przyszłym systemie niezbędny okazuje się proces weryfikacji tych diagramów UML. Weryfikacja spójności jest jednakże dość złożonym zagadnieniem, gdyż diagramy aktywności nie są formalnym sposobem zapisu wymagań. Proponujemy rozszerzenie diagramów aktywności UML do diagramów nazwanych przez nas diagramami Funkcjonalność-Struktura-Behawioryzm (FSB) UML które umożliwiają automatyzację weryfikacji spójności scenariuszy wizualizowanych przypadków użycia. Co więcej diagram FSB UML umożliwia równoczesne modelowanie funkcjonalności, struktury i zachowania docelowego modelu systemu. Dlatego też zaproponowany diagram aktywności FSB UML umożliwia również opracowywanie kolejnych spójnych i kompletnych modeli na jego podstawie. Ponadto diagram aktywności FSB UML może być wykorzystany do automatyzacji generowania aplikacji typu workflow bez potrzeby ręcznego programowania.

9

Apriori-Based Rule Generation in Incomplete Information Databases and Non-Deterministic Information Systems

Sakai H., Wu M., Nakata M.

Fundamenta Informaticae

|

2014

|

Vol. 130, nr 3

343--376

EN

This paper discusses issues related to incomplete information databases and considers a logical framework for rule generation. In our approach, a rule is an implication satisfying specified constraints. The term incomplete information databases covers many types of inexact data, such as non-deterministic information, data with missing values, incomplete information or interval valued data. In the paper, we start by defining certain and possible rules based on non-deterministic information. We use their mathematical properties to solve computational problems related to rule generation. Then, we reconsider the NIS-Apriori algorithm which generates a given implication if and only if it is either a certain rule or a possible rule satisfying the constraints. In this sense, NIS-Apriori is logically sound and complete. In this paper, we pay a special attention to soundness and completeness of the considered algorithmic framework, which is not necessarily obvious when switching from exact to inexact data sets. Moreover, we analyze different types of non-deterministic information corresponding to different types of the underlying attributes, i.e., value sets for qualitative attributes and intervals for quantitative attributes, and we discuss various approaches to construction of descriptors related to particular attributes within the rules' premises. An improved implementation of NIS-Apriori and some demonstrations of an experimental application of our approach to data sets taken from the UCI machine learning repository are also presented. Last but not least, we show simplified proofs of some of our theoretical results.

10

Complete Conceptual Schema Algebras

Ma H., Noack R., Schewe K-D., Thalheim B., Wang Q.

Fundamenta Informaticae

|

2013

|

Vol. 124, nr 3

271--295

EN

A schema algebra comprises operations on database schemata for a given data model. Such algebras are useful in database design as well as in schema integration. In this article we address the necessary theoretical underpinnings by introducing a novel notion of conceptual schema morphism that captures at the same time the conceptual schema and its semantics by means of the set of valid instances. This leads to a category of schemata that is finitely complete and co-complete. This is the basis for a notion of completeness of schema algebras, if it captures all universal constructions in the category of schemata. We exemplify this notion of completeness for a recently introduced particular schema algebra.

11

On Realisability Semantics for Intersection Types with Expansion Variables

Kamareddine F., Nour K., Rahli V., Wells J. B.

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

153-184

EN

Expansion is a crucial operation for calculating principal typings in intersection type systems. Because the early definitions of expansion were complicated, E-variables were introduced in order to make the calculations easier to mechanise and reason about. Recently, E-variables have been further simplified and generalised to also allow calculating other type operators than just intersection. There has been much work on semantics for type systems with intersection types, but none whatsoever before our work, on type systems with E-variables. In this paper we expose the challenges of building a semantics for E-variables and we provide a novel solution. Because it is unclear how to devise a space of meanings for E-variables, we develop instead a space of meanings for types that is hierarchical. First, we index each type with a natural number and show that although this intuitively captures the use of E-variables, it is difficult to index the universal type ωwith this hierarchy and it is not possible to obtain completeness of the semantics if more than one E-variable is used. We then move to a more complex semantics where each type is associated with a list of natural numbers and establish that both ů and an arbitrary number of E-variables can be represented without losing any of the desirable properties of a realisability semantics.

12

Statistically convergent difference double sequence spaces defined by Orlicz function

Sarma B.

Fasciculi Mathematici

|

2012

|

Nr 49

137--144

EN

In this article we introduce some statistically convergent difference double sequence spaces defined by Orlicz function. Completeness of the spaces will be proved. We study some of their other properties like solidness, symmetricity etc. and prove some inclusion results.

13

Observational Completeness on Abstract Interpretation

Amato G., Scozzari F.

Fundamenta Informaticae

|

2011

|

Vol. 106, nr 2-4

149-173

EN

In the theory of abstract interpretation, a domain is complete when abstract computations are as precise as concrete computations. In addition to the standard notion of completeness, we introduce the concept of observational completeness. A domain is observationally complete for an observable when abstract computations are as precise as concrete computations, if we only look at properties in . We prove that continuity of state-transition functions ensures the existence of the least observationally complete domain and we provide a constructive characterization. We study the relationship between the least observationally complete domain and the complete shell. We provide sufficient conditions under which they coincide, and show several examples where they differ, included a detailed analysis of cellular automata.

14

First-Order Linear-time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment

Belardinelli F., Lomuscio A.

Fundamenta Informaticae

|

2011

|

Vol. 106, nr 2-4

175-190

EN

We investigate quantified interpreted systems, a computationally grounded semantics for a first-order temporal epistemic logic on linear time. We report a completeness result for themonodic fragment of a language that includes LTL modalities as well as distributed and common knowledge. We exemplify possible uses of the formalismby analysingmessage passing systems, a typical framework for distributed systems, in a first-order setting.

15

Completness of relevant modal logics with disjunctive rules

Seki T.

Reports on Mathematical Logic

|

2009

|

Vol. 44

3-18

EN

Disjunctive rules are known to validate material implication principles, which may not hold in weaker relevant logics. On the other hand, they prevent the oddity of not preserving truth at the base world, from which many weaker relevant logics suffer. The same holds for relevant modal logics. This paper proves completeness of relevant modal logics with disjunctive rules.

16

Skolem Machines

Fisher J., Bezem M.

Fundamenta Informaticae

|

2009

|

Vol. 91, nr 1

79-103

EN

The Skolem machine is a Turing-complete machine model where the instructions are first-order formulas of a specific form. We introduce Skolem machines and prove their logical correctness and completeness. Skolem machines compute queries for the Geolog language, a rich fragment of first-order logic. The concepts of Geolog trees and complete Geolog trees are defined, and these tree concepts are used to show logical correctness and completeness of Skolem machine computations. The universality of Skolem machine computations is demonstrated. Lastly, the paper outlines implementation design issues using an abstract machine model approach.

17

Some difference paranormed sequence spaces defined by Orlicz functions

Tripathy B. C., Dutta H.

Fasciculi Mathematici

|

2009

|

Nr 42

121-131

EN

In this paper we introduce the difference paranormed sequence spaces ...[wzór] respectively. We study their different properties like completeness, solidity, monotonicity, symmetricity etc.We also obtain some relations between these spaces as well as prove some inclusion results.

18

On some classes of difference double sequence spaces

Tripathy B.C.

Fasciculi Mathematici

|

2009

|

Nr 41

135-142

EN

In this article we introduce the difference double sequence spaces &some;defined over a seminormed space (X,q), seminormed by q. We examine some topological and algebraic properties of these spaces like symmetricity, solidness, monotonoc-ity, convergence free, nowhere densenes etc. We prove some inclusion results too.

19

Complete Process Semantics of Petri Nets

Juhás G., Lorenz R., Mauser S.

Fundamenta Informaticae

|

2008

|

Vol. 87, nr 3-4

331-365

EN

In the first part of this paper we extend the semantical framework proposed in [22] for process and causality semantics of Petri nets by an additional aim, firstly mentioned in the habilitation thesis [15]. The aim states that causality semantics deduced from process nets should be complete w.r.t. step semantics of a Petri net in the sense that each causality structure which is enabled w.r.t. step semantics corresponds to some process net. In the second part of this paper we examine several process semantics of different Petri net classes w.r.t. this aim. While it is well known that it is satisfied by the process semantics of place/transition Petri nets (p/t-nets), we show in particular that the process semantics of p/t-nets with weighted inhibitor arcs (PTI-nets) proposed in [22] does not satisfy the aim. We develop a modified process semantics of PTI-nets fulfilling the aim of completeness and also all remaining axioms of the semantical framework. Finally, we sketch results in literature concerning the aim of completeness for process definitions of various further Petri net classes. The paper is a revised and extended version of the conference paper [18].

20

The sequence space m(Φ, Δm, p)F

Tripathy B. C., Borgohain S.

Fasciculi Mathematici

|

2008

|

Nr 39

87-96

EN

The sequence space m(øΔmp)F of fuzzy real numbers for 0 < p < 1 and 1 < p < ∞, are introduced. Some properties of the sequence space like solidness. symmetricity, convergence-free etc. are studied.