bluuebunny/crossref_metadata_2025_split huggingface dataset:
Philosophical Root of Moderation Discourse in Iran’s Eleventh Presidential Election
Authors: Jafari Leila , Alihosseini Ali , Emamjomehzadeh Seyyedjavad 
Published: January 2018

Abstract
Moderation was a triumphant discourse of Iran's eleventh presidential election. It’s a new attitude in the political realm and most of the movements relate themselves to it and each one interprete their actions according to moderation. For clarifying this ambiguous trend, we should refer to its philosophical root. It seems that Aristotle is the first one who represented this theory. In fact, moderation is one of the main principles of Aristotelian ethics. Understanding this concept requires understanding the basic concepts of the intellectual and moral theory of Aristotle. Moderation is the center of his theory of virtue. According to this principle, all the moral virtues are intermediates and excess, and defects in the actions and emotions cause moral vices. This theory could be the best way to pass excess and deficiencies in Iran's political sphere.
Empirical Investigation of Impediments to Returnees’ Entrepreneurship in Ghana: An Application of Structural Equation Modelling
Authors: Issifu Ibrahim 
Published: January 2018

AbstractIn recent years the issue of return migration and development has gained the unprecedented attention of practitioners, policymakers, and international organizations. In particular, the International Organization for Migration’s assisted voluntary return program seems to be the subject of increasing euphoria and optimism. However, the most overlooked aspect of return migration and entrepreneurship has been the binding constraints facing returnee entrepreneurs in their home countries. Drawing on field survey data, this study examines the impediments to returnees’ entrepreneurship in the Ghanaian capital city of Accra using Principal Component Analysis (PCA) and Structural Equation Modeling (SEM) techniques. The results show that only finance appears to be a key impediment, with a direct relationship with returnees’ entrepreneurial activities. Further synthesis of the path analysis of this study shows that access to credit and business training could facilitate returnees’ foreign acquired financial and human capital into sustainable entrepreneurial activities in Ghana.
Advancement of Tools Supporting Improvement of Work Safety in Selected Industrial Company
Authors: Gembalska-Kwiecień Anna 
Published: January 2018

Abstract
In the presented article, the advancement of tools to improve the safety of work in the researched industrial company was taken into consideration. Attention was paid to the skillful analysis of the working environment, which includes the available technologies, work organization and human capital. These factors determine the development of the best prevention activities to minimize the number of accidents.
Is Poland an Innovative Country?
Authors: Chybowska Dorota , Chybowski Leszek , Souchkov Valeri 
Published: January 2018

Abstract
The potential for innovativeness is difficult to measure, though many have attempted to do so. In order to look at Poland’s innovation potential, its current position and its opportunity to grow, compared with developing and developed countries, this study analysed the patent statistics of the Polish and European Patent Offices. Poland has been a member of the European Union for over a decade now. Therefore, we took into consideration the statistics for patent applications and grants for the last decade, up to the first quarter of 2016. The questions we wanted to answer concerned not only the technology fields that Poland patented its inventions in, but also the types of patent grantees and applicants. In order to determine why Poland is still considered to be only a moderate innovator by the Innovation Union Scoreboard, we also gathered information on Polish inventors abroad in 2015 and the first quarter of 2016, to see their number, technology fields, and types of patent grantees. Finally, we attempted to identify the main barriers that seem to inhibit Polish technology and innovation growth, despite significantly growing R&D intensities (up from 0.56 GDP and EUR 1,139 M in 2004 to 0.94 GDP and EUR 3,864 M in 2014).
Extinction of the initial within-compound association established in a blocked preexposure to two compound flavours
Authors: Cabo Fernando , Caramés José M. , Almaraz Julián , Espinet Alfredo 
Published: January 2018

Abstract
Extinction of the A↔X association after blocked preexposure to AX-BX was studied in two experiments. In Experiment 1, two groups of rats received long (14 trials) or short (4 trials) blocked preexposure to AX-BX and subsequent conditioning of X. The results showed that the AX association was equally preserved after long and short preexposure. Experiment 2 studied the effect of blocked preexposure to 0, 1 or 2 ruptures of the AX association on extinction. In this experiment a “rupture” is produced when, in subsequent blocks, one element of the original compound is presented in compound with a different element. A significant extinction was observed only when the AX association was broken twice
The influence of television stories on narrative abilities in children
Authors: Bermejo Berros Jesús , Aierbe Barandiaran Ana , Oregui González Eider , Bartau Rojas Isabel 
Published: January 2018

Abstract
This research explores the narrative abilities demonstrated by children aged between 8 and 12 in the production of television stories. The results reveal that not all television stories viewed by children foster the informal education process. One type of story, termed narrativizing, enables children to produce coherent stories which clearly articulate the causal, temporal and motivational relations, as well as the means-end structures, the proximal relations of the intrigue and the distal relations of the plot. Other television stories, denarrativizing stories, tend to induce disarrangements and incoherence at all structural levels of the stories produced by children. This in turn hampers the development of their narrative abilities, which are necessary to the correct development of narrative thought. These results indicate the need to exercise social control over this latter type of fictional television narrative, to which children are exposed throughout their development within the framework of informal education.
PENGARUH TEMPERATUR PENGERINGAN TERHADAP SWELLING DAN TENSILE STRENGTH EDIBLE FILM HASIL PEMANFAATAN PATI LIMBAH KULIT SINGKONG
Authors: Kanani Nufus , Wardalia Wardalia , Wardhono Endarto , Rusdi Rusdi 
Published: January 2018

ABSTRAKPengemasan merupakan proses perlindungan suatu produk pangan yang bertujuan menjaga keawetan dan konsistensi mutu. Bahan pengemas dari plastik banyak digunakan dengan pertimbangan ekonomis, namun penggunaan material sintesis tersebut berdampak pada pencemaran lingkungan. Salah satu alternatif untuk menangani permasalahan tersebut dengan menggunakan material ramah lingkungan (biodegradable) seperti edible film. Penelitian ini bertujuan untuk mengkaji pengaruh temperatur pengeringan terhadap swelling dan tensile strength edible film hasil pemanfaatan pati limbah kulit singkong dengan penambahan ekstrak jahe merah. Penelitian ini diawali dengan tahap pembuatan ekstrak jahe merah dan pati dari limbah kulit singkong, setelah itu dilanjutkan dengan pembuatan edible film dengan variasi penambahan ekstrak jahe merah (0.5-1.1% w/v) dan diberi plasticizer berupa gliserol (1% v/v). Selanjutnya dilakukan tahapan pembuatan dan pencetakkan edible film dan pengeringan pada temperatur ( 50;60;700C). Hasil yang diperoleh selanjutnya dilakukan analisa swelling dan tensile strength. Hasil menunjukkan nilai swelling dan tensile strength tertinggi diperoleh pada pada penambahan ekstrak jahe merah 1.1% dan temperatur pengeringan 700C yaitu masing-masing 88.89 % dan 50,66 kg/cm2.Kata Kunci : Kemuluran, Kuat tarik, Lapisan edibel ABSTRACTPackaging is a protection food product to maintain the quality and durability of food. Plastic packaging is widely used for economic consideration, but it leads to environmental pollution. The alternative way to handle this problem is by using biodegradable material such as edible film. This study aims to examine the effect of dying temperature on the swelling and tensile strength of edible cassava peel starch film with the addition of red ginger extract. This research was started with the extraction of red ginger and cassava peel starch, followed by edible film making with variation of red ginger extract addition (0.5-1.1% w/v) and glycerol (1% v/v) as plasticizer. The next stages were production and molding of the edible film. The edible films were then dried at the temperature of (50;60;700C). Furthermore swelling and tensile strength analysis was conducted to the product of edible film. The results showed that the highest swelling and tensile strength values were obtained on the addition of red ginger extract of 1.1% and the drying temperature of 700C which were 88.89% and 50,664 kg / cm2 respectively.Keywords : Edible film, Swelling, Tensile strength
GAYA KEPENGARANGAN GODI SUWARNA DALAM KUMPULAN CERPEN MURANG-MARING
Authors: Rahayu Taufik 
Published: January 2018

This research aims to reveal the style of author Godi Suwarna in the short stories collection buku Murang-Maring. In the universe of Sundanese literature, the Godi’s writing style is a new thing that contradicts the general style of Sundanese literature that is realism. Godi grew up in a rural area, and later as an adult continued in an urban environment. His short stories are the collaboration and mixing between the city and the village, traditional and modern. The ideas that are raised into his work are also mostly reconstruct the traditional stories that already exist, be it from folklore, pantun stories, wayang stories, fairy tales and so forth into a new, more modern form in accordance with the will of the author. Godi and his works are dissected by using expressive studies that focus the discussion to the collection of short stories Murang-Maring and the character of Godi himself. Based on the results of the research, Godi is an author who is upset with the surrounding social circumstances. The clash between rules and freedom also greatly influences Godi's self in his works. Godi's short story works are like a container for aspiration and criticism. In addition, the influence of wayang is very visible in the short stories, either from the stroytelling style or borrowing the characters with his nyeleneh and unique style.AbstrakRiset ini bertujuan untuk mengungkap gaya pengarang Godi Suwarna dalam buku kumpulan cerpen Murang-Maring. Di jagat kesusastraan Sunda, gaya mengarang Godi adalah hal baru yang bertolak belakang dari gaya umum sastra Sunda yang beraliran realis. Godi dibesarkan di lingkungan pedesaan, dan kemudian setelah dewasa berlanjut di lingkungan perkotaan. Cerpen-cerpennya adalah kolaborasi dan percampuran antara kota dan desa, tradisional dan modern. Ide-ide yang diangkat ke dalam karyanya pun kebanyakan merekonstruksi cerita-cerita tradisional yang sudah ada, baik itu dari foklor, cerita pantun, cerita wayang, dongeng, dan sebagainya ke dalam bentuk baru yang lebih modern sesuai dengan kehendak pengarang. Godi dan karyanya dibedah dengan memakai kajian ekspresif yang memfokuskan pembahasan kepada kumpulan cerpen Murang-Maring dan sosok Godi sendiri. Berdasarkan hasil penelitian, Godi termasuk pengarang yang gundah dengan keadaan sosial di sekitarnya. Benturan antara aturan dan kebebasan juga sangat memengaruhi diri Godi dalam karya-karyanya. Karya cerpen-cerpen Godi juga seperti wadah untuk menyalurkan aspirasi dan kritik. Selain itu, pengaruh wayang sangat kental terlihat dari cerpen-cerpennya, baik itu dari gaya penceritaannya maupun meminjam tokoh-tokoh dengan gayanya yang nyeleneh dan khas.
PEMELAJARAN TATA BAHASA BERBASIS TEKS SISWA KELAS V SEKOLAH DASAR DI KOTA MEDAN
Authors: Lubis Rehan Halilah , Nurelide Nurelide 
Published: January 2018

Penelitian ini mencoba menjawab permasalahan yang dihadapi guru tentang pemelajaran tata bahasa Indonesia yang tidak terdapat pada buku pegangan siswa maupun guru. Di samping itu, siswa kesulitan dalam membedakan imbuhan di- dan kata depan di yang terdapat pada teks. Permasalahan yang dibahas dalam penelitian ini yaitu bagaimana pemelajaran tata bahasa berbasis teks siswa sekolah dasar di Kota Medan dan bagaimana hasil belajarnya. Metode penelitian yang digunakan yaitu metode kualitatif dan kuantitatif dengan sumber data proses kegiatan belajar mengajar yang diambil dengan cara observasi langsung dan hasil belajar siswa yang diperoleh dari hasil tes. Lokasi penelitian adalah dua sekolah yang berada di Kecamatan Medan Selayang dan Medan Johor dengan jumlah siswa sebanyak 60 orang. Pemelajaran tata bahasa berbasis teks siswa kelas V sekolah dasar di Kota Medan menciptakan sistem pemelajaran berfokus pada siswa. Siswa dituntut untuk mampu mengidentifikasi, mengklasifikasi, serta mampu menemukan permasalahan dan menjawab permasalahan dengan tuntunan guru. Guru dijadikan sebagai fasilitator dan motivator dalam kegiatan belajar mengajar. Adapun nilai rata-rata hasil kegitan belajar mengajar belajar dengan menerapan model pemelajaran tata bahasa berbasis teks dengan cara belajar siswa aktif berjumlah 77,75. Nilai 77,75 dikategorikan baik.
PERJUANGAN PEREMPUAN PAPUA DALAM NOVEL <em>NAMAKU TEWERAUT</em> DAN <em>TANAH TABU</em>
Authors: Hidayat Sarip 
Published: January 2018

Novel Tanah Tabu dan Namaku Teweraut bercerita tentang kondisi perempuan Papua yang tengah berada dalam belenggu tradisi. Dalam kedua novel terdapat upaya perjuangan tokoh-tokohnya untuk berusaha keluar dari tradisi yang tidak memihak kepada perempuan. Penelitian ini bertujuan untuk menemukan persamaan dan perbedaan kedua novel tersebut dari segi struktur dan cara perjuangan para tokoh digambarkan serta memberikan alasan mengapa mereka melakukan perjuangan tersebut. Teori yang digunakan adalah teori sastra bandingan dan kajian gender. Metode yang digunakan dalam penelitian ini adalah metode deskriptif-analitis. Berdasarkan analisis dan perbandingan data dapat disimpulkan bahwa kedua novel yang diteliti memiliki persamaan latar, penokohan, alur, dan tema. Perbedaan di antara keduanya tampak dalam unsur sudut pandang. Berdasarkan temanya dapat disimpulkan lebih jauh bahwa perjuangan perempuan Papua dalam dua novel memiliki pandangan yang sama, yaitu pendidikan menjadi jalan keluar bagi perempuan Papua untuk memperoleh derajat yang setara dengan laki-laki.
Recursive Definitions of Monadic Functions
Authors: Krauss Alexander 
Published: January 2018

Using standard domain-theoretic fixed-points, we present an approach for defining recursive functions that are formulated in monadic style. The method works both in the simple option monad and the state-exception monad of Isabelle/HOL's imperative programming extension, which results in a convenient definition principle for imperative programs, which were previously hard to define.For such monadic functions, the recursion equation can always be derived without preconditions, even if the function is partial. The construction is easy to automate, and convenient induction principles can be derived automatically.
First-Order Interpolation and Interpolating Proof Systems
Authors: Kovács Laura , Voronkov Andrei 
Published: January 2018

It is known that one can extract Craig interpolants from so-called localproofs. An interpolant extracted from such a proof is a booleancombination of formulas occurring in the proof. However, standard completeproof systems, such as superposition, for theories having the interpolationproperty are not necessarily complete for local proofs: there are formulashaving non-local proofs but no local proof.In this paper we investigate interpolant extraction from non-local refutations(proofs of contradiction) in the superposition calculus and prove a numberof general results about interpolant extraction and complexity of extractedinterpolants. In particular, we prove that the number of quantifier alternationsin first-order interpolants of formulas without quantifier alternations isunbounded. This result has far-reaching consequences for using local proofsas a foundation for interpolating proof systems: any such proof system shoulddeal with formulas of arbitrary quantifier complexity.To search for alternatives for interpolating proof systems, we consider severalvariations on interpolation and local proofs. Namely, we give an algorithm forbuilding interpolants from resolution refutations in logic without equality anddiscuss additional constraints when this approach can be also used for logicwith equality. We finally propose a new direction related to interpolation vialocal proofs in first-order theories.
A Resolution Method for Modal Logic S5
Authors: Salhi Yakoub , Sioutis Michael 
Published: January 2018

The aim of this work is to define a resolution method for the modal logic S5. Wefirst propose a conjunctive normal form (S5-CNF) which is mainly based on using labelsreferring to semantic worlds. In a sense, S5-CNF can be seen as a generalization of theconjunctive normal form in propositional logic by using in the clause structure the modalconnective of necessity and labels. We show that every S5 formula can be transformedinto an S5-CNF formula using a linear encoding. Then, in order to show the suitabilityof our normal form, we describe a modeling of the problem of graph coloring. Finally, weintroduce a simple resolution method for S5, composed of three deductive rules, and weshow that it is sound and complete. Our deductive rules can be seen as adaptations ofRobinson’s resolution rule to the possible-worlds semantics.
Beyond DRAT: Challenges in Certifying UNSAT
Authors: Felgenhauer Bertram 
Published: January 2018

Contemporary SAT solvers are complex tools and may contain bugs. Inorder to increase the trust in the results of SAT solving, SAT solversmay produce certificates that can be checked independently. Forunsatisfiability certificates, DRAT is the de facto standard. As longas the checkers are not formalized, extending the certificate formatwould decrease the trust in the checker because its code complexityincreases. With the advent of formally verified checkers for DRATproofs, this is no longer the case. In this note I argue thatsymmetry breaking is not adequately supported by DRAT proofs, andpropose to have dedicated certification for symmetry breaking instead.
External Tools for the Formal Proof of the Kepler Conjecture
Authors: Hales Thomas C. 
Published: January 2018

The Kepler conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space has density greater than that of the familiar cannonball arrangement. The proof of the Kepler conjecture was announced in 1998, but it went several years without publication because of the lingering doubts of referees about the correctness of the proof. In response to these publication hurdles, the Flyspeck project seeks to give a complete formal proof of the Kepler conjecture using the proof assistant HOL Light.The original proof of the Kepler relies on long computer calculations, and these calculations present special formalization challenges. A major part of the Flyspeck project requires the integration of external computational tools with the proof assistant. Some of these external tools are the GNU linear programming kit, AMPL (a modeling language for mathematical programming), Mathematica calculations, nonlinear optimization, and custom code in C++, C, C#, Java, and Objective Caml.Earlier work by A. Solovyev has implemented efficient linear programming in HOL Light. This talk will include a description of his more recent work that automates the link between linear programming and the Flyspeck project.
Reasoning with Triggers
Authors: Dross Claire , Conchon Sylvain , Kanig Johannes , Paskevich Andrei 
Published: January 2018

SMT solvers can decide the satisfiability of ground formulas modulo a combination ofbuilt-in theories. Adding a built-in theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using first-order formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures.In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of first-order axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate using the theory of arrays, how such proofs can be achieved in our formalism.
A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
Authors: Tourret Sophie , Echenim Mnacho , Peltier Nicolas 
Published: January 2018

We describe an algorithm that generates prime implicates of equational clause sets without variables and function symbols. The procedure is based on constrained superposition rules, where constraints are used to store literals that are asserted as additional axioms (or hypotheses) during the proof search. This approach is sound and deductive-complete, and it is more ecient than previous algorithms based on conditional paramodulation. It is also more exible in the sense that it allows one to restrict the search space by imposing additional properties that the generatedimplicates should satisfy (e.g., to ensure relevance).
High-level Hybrid Systems Analysis with Hypy
Authors: Bak Stanley , Bogomolov Sergiy , Schilling Christian 
Published: January 2018

Hybrid systems play an important role in many application domains. A range of powerful analysis methods for this class of systems perform high-level analysis, where, iteratively, (1) a reachability computation is performed on a system model, (2) the result of the analysis is examined, and (3) the model is modified and the process repeats. For example, a well- known high-level analysis method is counter-example guided abstraction refinement (CEGAR), where, at each iteration, the model is refined based on the counter-example produced by the reachability computation.In this paper, we present hypy, a python library which strives to ease the development of high-level analysis approaches. Hypy provides the necessary machinery to run a number of up-to-date hybrid systems analysis tools, parse their outputs, and modify the models. The modifications are performed using HyST, a source-to-source model transformation framework, which supports output formats including SpaceEx, Flow*, dReach, and HyCreate. HyST, however, does not run reachability tools nor interpret their output. The developed hypy library fills this gap, providing an extendable and flexible architecture which simplifies development of complex analysis strategies. We demonstrate its practical potential on three non-CEGAR case studies: abstraction for parameter identification, generation of pseudo-invariants to reduce reachability overapproximation error, and completely automatic tool parameter tuning for the Flow* reachability tool.
Theorem Proving for Logic with Partial Functions Using Kleene Logic and Geometric Logic
Authors: De Nivelle Hans 
Published: January 2018

We introduce a theorem proving strategy for Partial Classical Logic (PCL) thatis based on geometric logic. The strategy first translates PCL theories into sets of Kleene formulas. After that, the Kleene formulas are translated into 3-valued geometric logic. The resulting formulas can be refuted by an adaptation ofgeometric resolution.The translation to Kleene logic does not only open the way to theorem proving, butit also sheds light on the relation between PCL, Kleene Logic, and classical logic.