This paper contains a discussion of striking similarities between influential philosophical concepts of the past and the approaches currently employed in selected areas of computer science. In particular, works of the Pythagoreans, Plato, Abelard, Ash’arites, Malebranche and Berkeley are presented and contrasted with such computer science ideas as digital computers, object-oriented programming, the modelling of an object’s actions and causality in virtual environments, and 3D graphics rendering. The intention of this paper is to provoke the computer science community to go (...) off the beaten path in order to find inspiration for the development of new approaches in software engineering. (shrink)

In [2], Bar-Hillel, Gaifman, and Shamir prove that the simple phrase structure grammars (SPGs) defined by Chomsky are equivalent in a certain sense to Bar-Hillel's bidirectional categorial grammars (BCGs). On the other hand, Cohen [3] proves the equivalence of the latter ones to what the calls free categorial grammars (FCGs). They are closely related to Lambek's syntactic calculus which, in turn, is based on the idea due to Ajdukiewicz [1]. For the reasons which will be discussed in the last section, (...) Cohen's proof seems to be at least incomplete. This paper yields a direct proof of the equivalence ofFCGs andSPGs. (shrink)

A precise velocity model is necessary to obtain reliable locations of microseismic events, which provide information about the effectiveness of the hydraulic stimulation. Seismic anisotropy plays an important role in microseismic event location by imposing the dependency between wave velocities and its propagation direction. Building an anisotropic velocity model that accounts for that effect allows for more accurate location of microseismic events. We have used downhole microseismic records from a pilot hydraulic fracturing experiment in Lower-Paleozoic shale gas play in the (...) Baltic Basin, Northern Poland, to obtain accurate microseismic events locations. We have developed a workflow for a vertical transverse isotropy velocity model construction when facing a challenging absence of horizontally polarized S-waves in perforation shot data, which carry information about Thomsen’s [Formula: see text] parameter and provide valuable constraints for locating microseismic events. We extract effective [Formula: see text], [Formula: see text] and [Formula: see text], [Formula: see text] for each layer from the P- and SV-wave arrivals of perforation shots, whereas the unresolved [Formula: see text] is retrieved afterward from the SH-SV-wave delay time of selected microseismic events. An inverted velocity model provides more reliable location of microseismic events, which then becomes an essential input for evaluating the hydraulic stimulation job effectiveness in the geomechanical context. We evaluate the influence of the preexisting fracture sets and obliquity between the borehole trajectory and principal horizontal stress direction on the hydraulic treatment performance. The fracturing fluid migrates to previously fractured zones, while the growth of the microseismic volume in consecutive stages is caused by increased penetration of the above-lying lithologic formations. (shrink)

We characterize all finitary consequence relations over S4.3, both syntactically, by exhibiting so-called passive rules that extend the given logic, and semantically, by providing suitable strongly adequate classes of algebras. This is achieved by applying an earlier result stating that a modal logic L extending S4 has projective unification if and only if L contains S4.3. In particular, we show that these consequence relations enjoy the strong finite model property, and are finitely based. In this way, we extend the known (...) results by Bull and Fine, from logics, to consequence relations. We also show that the lattice of consequence relations over S4.3 is countable and distributive and it forms a Heyting algebra. (shrink)

In [4], I proved that the product-free fragment L of Lambek's syntactic calculus (cf. Lambek [2]) is not finitely axiomatizable if the only rule of inference admitted is Lambek's cut-rule. The proof (which is rather complicated and roundabout) was subsequently adapted by Kandulski [1] to the non-associative variant NL of L (cf. Lambek [3]). It turns out, however, that there exists an extremely simple method of non-finite-axiomatizability proofs which works uniformly for different subsystems of L (in particular, for NL). We (...) present it below to the use of those who refer to the results of [1] and [4]. (shrink)

We propose a non-standard interpretation of Alternating-time Temporal Logic with imperfect information, for which no commonly accepted semantics has been proposed yet. Rather than changing the semantic structures, we generalize the usual interpretation of formulae in single states to sets of states. We also propose a new epistemic operator for ?practical? or ?constructive? knowledge, and we show that the new logic (which we call Constructive Strategic Logic) is strictly more expressive than most existing solutions, while it retains the same model (...) checking complexity. Finally, we study properties of constructive knowledge and other operators in this non-standard semantics. (shrink)

Helium and neon, the two lightest noble gases, have been traditionally positioned by IUPAC in the Group 18 of the Periodic Table of Elements, together with argon, and other unreactive or moderately reactive gaseous elements, and oganesson. In this account we revive the old discussion on the possible placement of helium in the Group 2, while preserving the position of neon in Group 18. We provide quantum-chemical arguments for such scenario—as well as other qualitative and quantitative arguments—and we describe previous (...) suggestions in the literature which support it or put it into question. To this author’s own taste, He should be placed in Group 2. (shrink)

Several Gentzen-style syntactic type calculi with product are considered. They form a hierarchy in such a way that one calculus results from another by imposing a new condition upon the sequent-forming operation. It turns out that, at some steps of this process, two different functors collapse to a single one. For the remaining stages of the hierarchy, analogues of Wajsbergs's theorem on non-mutual-definability are proved.

We provide an algorithm for determining a categorial grammar from linguistic data that essentially uses unification of type-schemes assigned to atoms. The algorithm presented here extends an earlier one restricted to rigid categorial grammars, introduced in [4] and [5], by admitting non-rigid outputs. The key innovation is the notion of an optimal unifier, a natural generalization of that of a most general unifier.

Well-being is becoming an increasingly popular issue in economics. The aim of the article is to present the concept of well-being and the methods of its measurement and to examine the statistical significance between the results obtained by specific indicators. The article was written based on the meta-analysis of the books and scientific papers on the subject, as well as well-being and welfare measurement reports. The study shows that there is a very wide range of theories and concepts related to (...) well-being which are sometimes exceptive. The most important conclusion from the study is that the correlation between welfare and well-being represented respectively by GDP and HDI is very strong, while the correlation between welfare and life satisfaction as well as well-being and subjective well-being are negligible. (shrink)

This article reevaluates the origins of Kierkegaard’s concept of imitation. It challenges the general approach to the genealogy of the phenomenon in question, which privileges the influence of various religious traditions on the thinker and ignores his exposure to the non-Christian literature. I contend that a close reading of the Apology, the Sophist, the Republic, and the Phaedo alongside Kierkegaard’s texts from the so-called second authorship reveals in the dialogues of Plato the three crucial aspects of Kierkegaard’s concept of imitation, (...) namely the phenomenon of following after, the existential, and the non-imitative character of imitation. Lastly, I show that, apart from striving to be a follower/an imitator of Christ, Kierkegaard perceives himself as a follower/an imitator of Socrates. This means that the life of the imitator of Christ is the examined life in the Socratic sense. (shrink)

In this paper, I present a new account of Richard Rorty’s interpretation of Michel Foucault, which demonstrates that in the course of his career, Rorty presented several diverse (often mutually exclusive) criticisms of Foucault’s political thought. These give different interpretations of what he took to be the flaws of that thought, but also provide different explanations as to the sources of these flaws. I argue that Rorty’s specific criticisms can be divided into two overall groups. Sometimes he saw Foucault’s rejection (...) of bourgeois democracies and bourgeois utopias as a specific case of his general critique regarding the structures of social life as inherently oppressive. At other times he seemed to attribute to Foucault a view that—while not all forms of social life are inherently oppressive—bourgeois democracies certainly are, in a very specific and radical way. In conclusion I show that Rorty’s interpretation of Foucault should be understood in the context of his approach toward the ‘American Cultural Left.’. (shrink)

Compact Bilinear Logic , introduced by Lambek [14], arises from the multiplicative fragment of Noncommutative Linear Logic of Abrusci [1] by identifying times with par and 0 with 1. In this paper, we present two sequent systems for CBL and prove the cut-elimination theorem for them. We also discuss a connection between cut-elimination for CBL and the Switching Lemma from [14].

Action logic of Pratt [21] can be presented as Full Lambek Calculus FL [14, 17] enriched with Kleene star *; it is equivalent to the equational theory of residuated Kleene algebras (lattices). Some results on axiom systems, complexity and models of this logic were obtained in [4, 3, 18]. Here we prove a stronger form of *-elimination for the logic of *-continuous action lattices and the –completeness of the equational theories of action lattices of subsets of a finite monoid and (...) action lattices of binary relations on a finite universe. We also discuss possible applications in linguistics. (shrink)

An axiomatics of the product-free syntactic calculus L ofLambek has been presented whose only rule is the cut rule. It was alsoproved that there is no finite axiomatics of that kind. The proofs weresubsequently simplified. Analogous results for the nonassociativevariant NL of L were obtained by Kandulski. InLambek's original version of the calculus, sequent antecedents arerequired to be nonempty. By removing this restriction, we obtain theextensions L 0 and NL 0 ofL and NL, respectively. Later, the finiteaxiomatization problem for L (...) 0 andNL 0 was partially solved, viz., for formulas withoutleft (or, equivalently, right) division and an (infinite) cut-ruleaxiomatics for the whole of L 0 has been given. Thepresent paper yields an analogous axiomatics forNL 0. Like in the author's previous work, the notionof rank of an axiom is introduced which, although inessentialfor the results given below, may be useful for the expectednonfinite-axiomatizability proof. (shrink)

We prove the finite model property (fmp) for BCI and BCI with additive conjunction, which answers some open questions in Meyer and Ono [11]. We also obtain similar results for some restricted versions of these systems in the style of the Lambek calculus [10, 3]. The key tool is the method of barriers which was earlier introduced by the author to prove fmp for the product-free Lambek calculus [2] and the commutative product-free Lambek calculus [4].

Observations of azimuthal seismic anisotropy provide useful information, notably on stress orientation and the presence of preexisting natural fracture systems, during hydraulic fracturing operations. Seismic anisotropy can be observed through the measurement of S-wave splitting on waveforms generated by microseismic events and recorded on downhole geophone arrays. We have developed measurements of azimuthal anisotropy from a Lower Paleozoic shale play in northern Poland. The observed orthorhombic anisotropic symmetry system is dominated by a vertically transverse isotropy fabric, produced by the alignment (...) of anisotropic platy clay minerals and by thin horizontal layering and overprinted by a weak azimuthal anisotropy. Despite the dominating VTI fabric, we successfully identified a weaker horizontal-transverse isotropy fabric striking east–southeast. We do this by constraining the rock-physics model inversion with VTI background parameters incorporated from other geophysical methods: microseismic velocity model inversion, 3D reflection seismic, and borehole cross-dipole sonic logs. The obtained orientation is consistent with a preexisting natural fracture set that has been observed using X-ray micro-imaging image logs from a nearby vertical well. The present-day regional maximum horizontal stress direction differs from the observed fracture strike by approximately 45°. This implies that the SWS measurements recorded during hydraulic stimulation of a shale-gas reservoir are imaging the preexisting natural fracture set, which influences the treatment efficiency, instead of the present-day stress. (shrink)

In [5] we study Nonassociative Lambek Calculus augmented with De Morgan negation, satisfying the double negation and contraposition laws. This logic, introduced by de Grooté and Lamarche [10], is called Classical Non-Associative Lambek Calculus. Here we study a weaker logic InNL, i.e. NL with two involutive negations. We present a one-sided sequent system for InNL, admitting cut elimination. We also prove that InNL is PTIME.

The presentation of the formal conception of noemata is the main aim of the article. In the first section, three informal approaches to noemata are discussed. The goal of this chapter is specifying main controversies and their sources concerned with different ways of the understanding of noemata. In the second section, basic assumptions determining the proposed way of understanding noemata are presented. The third section is devoted to the formal set-theoretic construction needed for the formal comprehension of noemata. In the (...) fourth section, definitions of noemata and their various kinds, as well as definitions of other phenomenological notions are formulated. In the last section, possibilities of further developing the proposed formal conception are indicated. (shrink)

In Zielonka (1981a, 1989), I found an axiomatics for the product-free calculus L of Lambek whose only rule is the cut rule. Following Buszkowski (1987), we shall call such an axiomatics linear. It was proved that there is no finite axiomatics of that kind. In Lambek's original version of the calculus (cf. Lambek, 1958), sequent antecedents are non empty. By dropping this restriction, we obtain the variant L 0 of L. This modification, introduced in the early 1980s (see, e.g., Buszkowski, (...) 1985; Zielonka, 1981b), did not gain much popularity initially; a more common use of L 0 has only occurred within the last few years (cf. Roorda, 1991: 29). In Zielonka (1988), I established analogous results for the restriction of L 0 to sequents without left (or, equivalently, right) division. Here, I present a similar (cut-rule) axiomatics for the whole of L 0. This paper is an extended, corrected, and completed version of Zielonka (1997). Unlike in Zielonka (1997), the notion of rank of an axiom is introduced which, although inessential for the results given below, may be useful for the expected non-finite-axiomatizability proof. (shrink)

The paper continues a series of results on cut-rule axiomatizability of the Lambek calculus. It provides a complete solution of a problem which was solved partially in one of the author''s earlier papers. It is proved that the product-free Lambek Calculus with the empty string (L 0) is not finitely axiomatizable if the only rule of inference admitted is Lambek''s cut rule. The proof makes use of the (infinitely) cut-rule axiomatized calculus C designed by the author exactly for this purpose.

The main aim of this paper is to challenge the validity of the distinction between legal justice and social justice. It is argued that what we usually call legal justice is either an application of the more fundamental notion of social justice to legal rules and decisions or is not a matter of justice at all. In other words, the only correct uses of the notion of legal justice are derivative from the notion of social justice and, hence, the alleged (...) conflicts between criteria of social and legal justice result from the confusion about the proper relationship between these two concepts. Two views about the social justice/legal justice dichotomy are of particular importance and will provide the focus for the argument: this dichotomy is sometimes identified with a classical distinction between distributive and commutative justice and sometimes with the distinction between substantive and procedural justice. (shrink)