A structure which generalizes formulas by including substitution terms is used to represent proofs in classical logic. These structures, called expansion trees, can be most easily understood as describing a tautologous substitution instance of a theorem. They also provide a computationally useful representation of classical proofs as first-class values. As values they are compact and can easily be manipulated and transformed. For example, we present an explicit transformations between expansion tree proofs and cut-free sequential proofs. A theorem prover which represents (...) proofs using expansion trees can use this transformation to present its proofs in more human-readable form. Also a very simple computation on expansion trees can transform them into Craig-style linear reasoning and into interpolants when they exist. We have chosen a sublogic of the Simple Theory of Types for our classical logic because it elegantly represents substitutions at all finite types through the use of the typed -calculus. Since all the proof-theoretic results we shall study depend heavily on properties of substitutions, using this logic has allowed us to strengthen and extend prior results: we are able to prove a strengthen form of the firstorder interpolation theorem as well as provide a correct description of Skolem functions and the Herbrand Universe. The latter are not straightforward generalization of their first-order definitions. (shrink)

In the original article published, the supplementary material is uploaded by mistake which has no association with the content of the article.

В книге говорится о творце, генерирующем творческие акты – непредсказуемые решения and (озарения and ), феномены, которыми обладает только человек-личность. Общественные институты, как и само общество в целом, не могут исключительно своими социальными усилиями генерировать творческий акт. Таким образом, без этого личностного, практически абсолютно автономного, творческого решения общество не может ни обойтись, ни чем-либо его заменить. Используя творческие акты, эти феномены, имманентные только человеку, общество консолидируется и развивается, и, таким образом, человек-творец становится двигателем истории человечества. В этом смысле категория личность (...) имеет не меньшую значимость, чем категория производительные силы или категория общество. Рассматривается концепция природы творчества по Вифляеву, с полным философским обоснованием. (shrink)

Appearing in the “Cairo Declaration on Human Rights in Islam” as an undefined referent for the limits on freedom of expression in Islam, Shariah is still to be chased as an indefinable referent which restricts freedom of the expression in the Islamic Republic of Iran. Iran’s Press Law as well as Constitution unveil Shariah’s referent to be a person: the Jurist-Ruler around whom a cult of personality is legalized in terms of “Imamate” and around whom all the limits on freedom (...) of expression revolve. Interpretation of Shariah is not a solution but part of the problem in Iran. Such problem can be dealt in terms of three modes of self-expression which were invented by the Iranian Reformists to avoid self-censorship. The notion of master-signifier can be the key to unraveling the problem of self-referentiality in freedom of expression and its Reformist solution in Iran’s legal system. (shrink)

Brain tumor classification plays a niche role in medical prognosis and effective treatment process. We have proposed a combined feature and image-based classifier for brain tumor image classification in this study. Carious deep neural network and deep convolutional neural networks -based architectures are proposed for image classification, namely, actual image feature-based classifier, segmented image feature-based classifier, actual and segmented image feature-based classifier, actual image-based classifier, segmented image-based classifier, actual and segmented image-based classifier, and finally, CFIC. The Kaggle Brain Tumor Detection (...) 2020 dataset has been used to train and test the proposed classifiers. Among the various classifiers proposed, the CFIC performs better than all other proposed methods. The proposed CFIC method gives significantly better results in terms of sensitivity, specificity, and accuracy with 98.86, 97.14, and 98.97%, respectively, compared with the existing classification methods. (shrink)

It is generally believed that an invariant notion of a global present or "Now" cannot be defined in special relativity, because of the relativity of optical simultaneity. I argue that this may be a non sequitur since it is not necessarily the case that the psychological "Now" should be thought of as associated with constant time slices in spacetime. By considering a science fictional version of the Twin Paradox due to Robert A. Heinlein, I argue that it is psychologically plausible (...) to associate the common specious present of several observers in relative motion with certain hypersurfaces of proper time of those observers corrected for acceleration history and relative motion in an obvious way. If this is correct then the relativity of optical simultaneity may be simply irrelevant to the question of the relativity of a globally distinguished "present". (shrink)

In the present paper, we introduce new models of pendulum motions for two cases: the first model consists of a pendulum with mass M moving at the end of a string with a suspended point moving on an ellipse and the second one consists of a pendulum with mass M moving at the end of a spring with a suspended point on an ellipse. In both models, we use the Lagrangian functions for deriving the equations of motions. The derived equations (...) are reduced to a quasilinear system of the second order. We use a new mathematical technique named a large parameter method for solving both models’ systems. The analytical solutions are obtained in terms of the generalized coordinates. We use the numerical techniques represented by the fourth-order Runge–Kutta method to solve the autonomous system for both cases. The stabilities of the obtained solutions are studied using the phase diagram procedure. The obtained numerical solutions and analytical ones are compared to examine the accuracy of the mathematical and numerical techniques. The large parameter technique gives us the advantage to obtain the solutions at infinity in opposite with the famous Poincare’s method which was used by many outstanding scientists in the last two centuries. (shrink)

Multiprofessional teams have become in recent years one of the distinguishing features of services, where professionals with different competences work together. The core of our interest is addressed to the équipe of a palliative care ward; in particular, to that series of working activities that consists of communicative acts, as équipe meetings, for instance. Our research focuses on the analysis of the process by which the development of knowledge in multiprofessional practice is built to establish more information on recurrent patterns (...) in the interaction and connect them to the specific context that these are shaped by. In this sense we will underline how components of knowing are shared among team members in constructing medical prognosis and we will analyse the connection among language processes, cognitive activities and social structures. More specifically, we will study the role of language and the context in the definition of linguistic acts in cognitive activities and in hierarchies involved in decision-making processes by exploring and pointing out how it is organised and structured. In particular through the study of talk-in-interaction where interchange of information is realised, we will emphasise how, in the multiprofessional équipe meeting, the realisation of practices and the knowledge useful to collaborative management of ward working life are established. To reach this aim, we adopted an ethnographic approach connected to the analysis of the situated interaction. (shrink)

If the current trend is any guide, it looks like we are heading towards a future in which relationships are determined and regulated by rights. In addition to the ?universal human rights? declared soon after the Second World War, other ?universal rights? have been declared and added to the list of rights, such as the rights of the child, the rights of indigenous peoples and so on. A question arises as to whether a world in which our relationships are governed (...) entirely on the basis of rights is an appealing one. I want to suggest that if our common future is regulated entirely by rights then we are moving in the wrong direction. By contrast, Tu Wei-ming believes that if Confucianism flourishes, we will move towards a society based on trust rather than rights, or what he calls a ?fiduciary society?. I will argue that while Tu's Confucian fiduciary society is perhaps an impractical ideal, a move towards it will provide a necessary counter-balance to the relentless march towards a rights-based society. (shrink)

A certain objection to belief in God is based on the intrinsic incoherence of the concept of Divine Being or God. In particular, it questions the major traditional characteristic, notably omniscience, and its relation to omnipotence, moral unassailability, and absence of embodiment on the part of the Divine Being. In this paper, an attempt is made to counter this objection by an appeal, not to natural theology, but rather to physicalism in its application to human beings, and by extension to (...) the possible consistency of God’s omniscience with the other divine attributes, which philosophers such as Michael Martin have found to be mutually inconsistent and therefore wanting. (shrink)