169 research outputs found
T-satisfiability test problem for the VL1 logical language of the VRS system
No full textIn this paper we give a short introduction to the satisfiability modulo theories (SMT) problem and demonstrate how the methods developed in the SMT research field can be applied in the requirement verification tool VRS, which supports insertion modelling methodology. We formalize the logical language VL1 used for formal reasoning in VRS and justify decidability of satisfiability problem in that language. Besides we discuss the context of the problem being solved and indicate possible methods that can be used on different stages of solution. Finally, we present a satisfiable conjunction search method, which is based on a set-representation of logical connectives in formulas
Завдання перевірки Т-здійсненності для логічнї мови VL1 системи VRS
No full textIn this paper we give a short introduction to the satisfiability modulo theories (SMT) problem and demonstrate how the methods developed in the SMT research field can be applied in the requirement verification tool VRS, which supports insertion modelling methodology. We formalize the logical language VL1 used for formal reasoning in VRS and justify decidability of satisfiability problem in that language. Besides we discuss the context of the problem being solved and indicate possible methods that can be used on different stages of solution. Finally, we present a satisfiable conjunction search method, which is based on a set-representation of logical connectives in formulas.В данной работе дается короткое введение в задачу проверки T-выполнимости формул относительно логических теорий, и показывается, что разработанные методы решения этой задачи могут применяться в технологии инсерционного моделирования, которая представлена в системе верификации требований VRS. Дается формализация логического языка, используемого в VRS для проведения формальных рассуждений, и показывается разрешимость проблемы выполнимости формул в этом языке. Обсуждаются особенности применения используемых методов, и описывается альтернативный алгоритм поиска выполнимой конъюнкции, основанный на множественном представлении операций в формулах.У даній роботі дається короткий введення в задачу перевірки T-виконуваності формул щодо логічних теорій, і показується, що розроблені методи вирішення цього завдання можуть застосовуватися в технології інсерційного моделювання, яка представлена в системі верифікації вимог VRS. Дається формалізація логічної мови, використовуваного в VRS для проведення формальних міркувань, і показується можливість розв'язання проблеми здійсненності формул в цій мові. Обговорюються особливості застосування використовуваних методів, і описується альтернативний алгоритм пошуку здійсненним кон'юнкції, заснований на множині поданні операцій в формулах
Нарратологический анализ романа В. Вульф «На маяк»
No full textВ данном исследовании была предпринята попытка проанализировать роман Вирджинии Вульф «На маяк», используя основные инструменты нарратологии. Особое внимание в исследовании уделяется подробному анализу избранных Вульф способов фокализации. Исследуется модификация функции недиегетического нарратора, которая чаще всего сводится к простому связыванию потоков сознания различных персонажей. Нарратор оказывается замаскирован, убран на второй план. Особый интерес для анализа представляет звучащий в романе голос «неопределенного нарратора» – в таких случаях оказывается невозможным ответить на вопрос «кто сейчас говорит?». Была рассмотрена комбинация приемов, при помощи которых выстраивается нарратив произведения. Особенно подробно в работе разобраны такие нарративные техники, как метод «об одном через другое», техника прокладывания туннелей, уплотнение текстового материала. С помощью этих техник Вульф стремится зафиксировать поток сознания, формирующийся из множества впечатлений разных героев, собрать из этих разрозненных мыслей единый нарратив. В работе также рассматривается игра Вульф с дезантропоморфизацией нарратора Кроме того, была исследована работа Вульф с художественным временем романа. Важный для Вульф концепт «разлома нарратива» посреди произведения определяет структуру романа, сообщая каждой из его частей особую функцию. Отмечается, что наиболее интересная для нарратологического анализа вторая часть романа выполняет роль некой паузы, «коридором» между первой и третьей, которые, за счет особенностей сюжетопостроения, вовлечены в особые, зеркальные, временные отношения: первая часть направлена в будущее, третье в прошлое. Наиболее ценным источником при анализе романа стали дневники Вульф, в которых она нередко записывала идеи, которые позже легли в основу тех или иных художественных находок писательницы. Другой важной составляющей работы стало сравнение применения тех или иных нарративных техник в других произведениях Вульф, как более ранних («Комната Джейкоба», «Миссис Дэллоуэй»), так и более поздних («Волны»). Такой подход позволяет проследить эволюцию художественного метода Вульф. Особенно важна для такого диахронического анализа оказалась малая проза Вульф («Пятно на стене», «Дом с приведениями», «Королевский сад»), так как именно в своих рассказах Вульф часто отрабатывала те или иные нарративные техники, которые позже получат более масштабное развитие в романе «На маяк».The main purpose of this research is to analyze Virginia Woolf’s novel To the Lighthouse, using the basic concepts of narratology. The paper focuses mainly on the detailed analysis of focalization methods chosen by Woolf. The special modification of the nondiegetic narrator’s function is also an object of our analysis. This narrator tends to be veiled or paled into insignificance. Fragments in which so called unclaimed consciousness is present (in which it’s impossible to state whose voice, whose stream of consciousness is transmitted) are studied in detail. Our research also focuses on the combination of narrative strategies that form the narrative of Woolf’s novel. Such techniques as the principle of association, tunneling technique, and the “thickening” of the text are the main objects of this part of our research. Using these techniques, Woolf strives to represent the stream of consciousness, which is formed by the myriads of characters’ impressions. The ways of making the novel’s narrator unantropomorphic are also discussed in the research. Besides, the artistic time continuum of the novel is analyzed. An important for Woolf concept of “consequent break of unity” defines the specific structure of the novel. Every part of the book has its own function. The second part, which is the most interesting one for the narratological analysis, has the function of some kind of “the narrative pause”, the corridor between the first and the third parts, which are mirroring each other. The diaries of Virginia Woolf were the most important source of information for our analysis of the evolution of Woolf’s style. Another important part of this work was comparing narrative techniques in To the Lighthouse and in the other Woolf’s works (such as The Jacob’s Room, Mrs. Dalloway, The Waves). The short stories by Woolf (The Mark on the Wall, A Haunted House, Kew Gardens) were especially important for that kind of diachronic analysis In her early short stories Woolf often practiced narrative techniques, later used in To the Lighthouse
Techniques for Portraying a Main Character in Yakut Epic: Investigating Olonkho Texts of Nyurgun Bootur the Swift by P. Oyunsky and Kulun Kullustuur the Obstinate by I. Timofeev-Teploukhov
No full textIntroduction. The article examines Yakut heroic olonkho epics — Nyurgun Bootur the Swift by P. Oyunsky and Kulun Kullustuur the Obstinate by I. Timofeev-Teploukhov — for techniques employed to create portraits of main characters. According to N. Yemelyanov, the olonkho Kulun Kullustuur the Obstinate recorded from taleteller I. Timofeev-Teploukhov clusters with earliest patterns of archaic epic, while that of Yakut writer P. Oyunsky (Nyurgun Bootur the Swift) is the first literary adaptation of olonkho texts. The study attempts an insight into how and which particular portrayal techniques were used by P. Oyunsky and I. Timofeev-Teploukhov to depict main characters of theirs. The comparative approach to the narratives recorded in different periods shall make it possible to trace the use of portrayal techniques, which shall underline the unique artistic features characterizing each of the taletellers, and show how such portrayal patterns developed to gain deeper associative essentials in further olonkho texts. Goals. The study aims to identify some distinct features inherent to the techniques of creating main characters’ portraits in the olonkhos Nyurgun Bootur the Swift and Kulun Kullustuur the Obstinate, and outline ethnic specifics in portrayal characteristics. To facilitate this, the paper shall classify portrayals, articulate types of techniques and their functions in portraying a main character, identify stable formulas employed to depict heroes, determine specific features of portrayal as a key technique for the making of an epic hero. The work reviews the existing types of epic portraits, their functions and attributes, examines some visual means serving to unveil the images of main characters. Results. The study attests to the examined narratives are characterized by an increased stability of depictive portrayals with peripheral parts (artistic and emotional epithets) tending to vary. Each such depictive portrayal proves multifunctional, semantically wide, and technically relevant. The descriptions of the heroes’ appearances are somewhat idealized and rich in comparisons, repetitions, evaluative epithets. Portrayal agendas of P. Oyunsky vary through history and depend on actual artistic methods and style employed by the author who pays special attention to fictional details depicted in the context of folk traditions. The study of the techniques helps identify which innovative tools P. Oyunsky used when he was creating his Nyurgun Bootur the Swift
Проблема свободи волi у вченнi св. Бернарда Клервоського в контекстi захiдноєвропейської iсторiї фiлософiї
No full textClairvaux in context of the west-european history of philosophy The article is devoted to philosophical understanding of the problem of free will in the doctrine of French medieval theologian and the founder of the medieval philosophical mysticism Saint Bernard of Clairvaux. The author explores different approaches to the problem in a historical and philosophical discourse, marking thus the ethical and mystical understanding by St. Bernard of an individual free choice as a remedy for rising to God.У статтi розкривається фiлософське осмислення проблеми свободи волi у вченнi французького середньовiчного теолога та основоположника середньовiчної фiлософської мiстики Бернарда Клервоського. Виявлено вiдмiннiсть пiдходiв до вирiшення проблеми свободи в iсторико-фiлософському дискурсi, позначена етико-мiстична концептуальнiсть розумiння св. Бернардомвiльного вибору людини як засобу сходження до Бога
- …
