Theorems in automated theorem proving are usually proved by formal logical proofs. However, there is a subset of problems which humans can prove by the use of geometric operations on diagrams, so called diagrammatic proofs. Insight is often more clearly perceived in these proofs than in the corresponding algebraic proofs; they capture an intuitive notion of truthfulness that humans find easy to see and understand. We are investigating and automating such diagrammatic reasoning about mathematical theorems. Concrete, rather than general diagrams (...) are used to prove particular concrete instances of the universally quantified theorem. The diagrammatic proof is captured by the use of geometric operations on the diagram. These operations are the inference steps of the proof. An abstracted schematic proof of the universally quantified theorem is induced from these proof instances. The constructive -rule provides the mathematical basis for this step from schematic proofs to theoremhood. In this way we avoid the difficulty of treating a general case in a diagram. One method of confirming that the abstraction of the schematic proof from the proof instances is sound is proving the correctness of schematic proofs in the meta-theory of diagrams. These ideas have been implemented in the system, called Diamond, which is presented here. (shrink)

Surveys have confirmed the ubiquity of aggression in schools, and verbal aggression is not an exception. The identification of teasing as a frequent form of verbal aggression is an indispensable step towards diminishing it. The purpose of this study was to investigate teasing among primary school students in Slovenia. The research showed that teasing is common in schools: the most usual forms of teasing refer to the students’ appearance, and the victims mostly report negative feelings after being teased. Most teasing (...) was done to reciprocate, and the most frequent response to teasing was a verbal comeback. The research revealed some differences in teasing between students by sex and age and offers some useful implications for practice. (shrink)

Many surveys confirm a substantial number of discipline problems in schools, but not many surveys are aimed at their identification. Identification of discipline violations is indispensable for prudent planning of their interventions in and prevention of their occurrence. Earlier studies focused mostly on the teachers’ perceptions of discipline problems and they were not interested in how discipline problems are perceived by students. In this study, teachers and students identified the most frequent and disturbing discipline violations. Given the results of the (...) survey, it would be necessary to pay more attention to preventing disruption of lessons and improper attitude, which are, in the views of teachers and students alike, the most frequent and disturbing violations. (shrink)

In this paper we present an approach to automated learning within mathematical reasoning systems. In particular, the approach enables proof planning systems to automatically learn new proof methods from well-chosen examples of proofs which use a similar reasoning pattern to prove related theorems. Our approach consists of an abstract representation for methods and a machine learning technique which can learn methods using this representation formalism. We present an implementation of the approach within the ΩMEGA proof planning system, which we call (...) LEARNΩMATIC. We also present the results of the experiments that we ran on this implementation in order to evaluate if and how it improves the power of proof planning systems. (shrink)

Digital piracy as a continuing problem significantly impacts various stakeholders, including consumers, enterprises, and countries. This study develops a three-level mechanism of determinants of consumer digital piracy behavior, with personal risk as an individual factor, susceptibility to interpersonal influence as an inter-personal factor, and moral intensity as a broad societal factor. Further, it explores the role of rationalization and future piracy intent as outcomes of past piracy behaviors. The authors use survey data from four countries in the European Union to (...) test the system of structural relationships. With an exception of the effect of consumers’ susceptibility to interpersonal influence on piracy behavior, the conceptual model receives remarkably consistent support across the four countries. Specifically, perception of personal risk and moral intensity negatively affected the reported piracy behavior in all four countries. The results further support the negative influence of moral intensity and the positive influence of past digital piracy behavior on consumers’ use of rationalization. Lastly, personal risk, rationalization, and past digital piracy behavior directly influenced consumers’ intention to engage in digital piracy in the future. The study also discusses implications of the findings and identifies areas of future research. (shrink)

In this contribution we propose an agent architecture for theorem proving which we intend to investigate in depth in the future. The work reported in this paper is in an early state, and by no means finished. We present and discuss our proposal in order to get feedback from the Calculemus community.

Ovaj rad bavi se presjekom umjetnosti, imaginacije, emocija i etičkog obrazovanja iz perspektive inovativne sinteze kognitivne teorije emocija i Gestalt pedagogije. Jedan od elemenata ove sinteze kognitivna je teorija emocija kakvu podržava Martha Nussbaum. Emocije se shvaćaju kao procjene koje se odnose na percepciju svijeta oko nas. Emocije su naši stavovi, razumijevanja i evaluacije svijeta iz perspektive naših ciljeva i projekata. To se pokazalo kao odlična polazišna točka za proučavanje emocija i drugih domena unutar etike obrazovanja. U ovom radu uvodim (...) pojam ‘iskustvene imaginacije’ i ukazujem na njezine metodologije koje smo razvili kao dio istraživanja preklapanja Gestalt pedagogije, kognitivne teorije emocija i pristupa etici iz perspektive umijeća življenja. Potom predstavljam sintezu kognitivne teorije emocija i Gestalt pedagogije, nakon čega razjašnjavam koncept iskustvene imaginacije, naglašavam njezinu ulogu u etičkom obrazovanju te zaključujem s nekolicinom osvrta na pristup umijeća življenja etici i etičkom obrazovanju. The paper discusses the intersection between art, imagination, emotions, and ethical education from the perspective of an innovative synthesis of cognitive theory of emotion and Gestalt pedagogy. One of the elements of this synthesis is the cognitive theory of emotion as endorsed by Martha Nussbaum. Emotions are understood as evaluative judgments that are related to our perception of the world around us. Emotions are our attitudes, understandings, and assessments of the world from the perspective of our goals and projects. This proves an excellent starting point from which to address them as an essential part of ethics education. Next, art and imagination are considered as a vehicle by which to address emotions and other domains within ethics education. Here, I introduce the concept of “experiential imagining” and point to the methodologies that sustain it. I have developed this concept as part of my research on the overlap between Gestalt pedagogy, cognitive theory of emotion, and the art of life approaches to ethics. Next, I present the synthesis between cognitive theory of emotion and Gestalt pedagogy. I then illuminate the concept of experiential imagination, emphasise its role in ethics education, and conclude with some reflections on the art of life approach to ethics and ethics education. (shrink)

Arhitektura se kot veščina in kasneje kot lepa umetnost od antike naprej vpisuje v polje filozofskega raziskovanja. Namen članka je prikazati razumevanje arhitekture v sklopu hermenevtične filozofije s prikazom mišljenja njenih treh velikih mislecev: Heideggra, Gadamerja in Vattima, ki bodo na področje arhitekture stopali z ontološkega in z estetskega vidika. Heidegger tako arhitekturo razume kot temeljno potezo biti, Gadamerju je najodličnejša umetnostna forma, kjer je tudi oblika presežena z vsebino, Vattimo pa poda tri vidike arhitekture v postmoderni dobi, ki jih (...) poveže s simultanostjo, simulakri in vprašanjem ornamentalnosti.Architecture as a skill, and later as a form of fine art, has been included in the field of philosophical research since Antiquity. The purpose of this article is to present the understanding of architecture within the field of hermeneutic philosophy by describing the ideas of three great hermeneutic philosophers: Heidegger, Gadamer and Vattimo, who approach architecture from the ontological and aesthetic point of view. Heidegger interprets architecture as a fundamental trait of existence; Gadamer values it as the artistic form par excellence, with the form surpassed by the contents, too; and Vattimo discusses three possible ways of perceiving architecture in the postmodern society, related to simultaneity, simulacra and the question of ornamentality. (shrink)

In order to effectively communicate information, the choice of representation is important. Ideally, a chosen representation will aid readers in making desired inferences. In this paper, we develop the theory of observation: what it means for one statement to be observable from another. Using observability, we give a formal characterization of the observational advantages of one representation of information over another. By considering observational advantages, people will be able to make better informed choices of representations of information. To demonstrate the (...) benefit of observation and observational advantages, we apply these concepts to set theory and Euler diagrams. In particular, we can show that Euler diagrams have significant observational advantages over set theory. This formally justifies Larkin and Simon’s claim that “a diagram is worth ten thousand words”. (shrink)

In this paper, we introduce Speedith which is an interactive diagrammatic theorem prover for the well-known language of spider diagrams. Speedith provides a way to input spider diagrams, transform them via the diagrammatic inference rules, and prove diagrammatic theorems. Speedith’s inference rules are sound and complete, extending previous research by including all the classical logic connectives. In addition to being a stand-alone proof system, Speedith is also designed as a program that plugs into existing general purpose theorem provers. This allows (...) for other systems to access diagrammatic reasoning via Speedith, as well as a formal verification of diagrammatic proof steps within standard sentential proof assistants. We describe the general structure of Speedith, the diagrammatic language, the automatic mechanism that draws the diagrams when inference rules are applied on them, and how formal diagrammatic proofs are constructed. (shrink)

In recent decades, the development of sciences and technologies had a significant impact in society. This impact has been object of analysis from several standpoints, i.e., scientific, communication, historical and anthropological. Consequently, serious changes were required by the society. One of these has been the emerging relationship science in society and its foundations of applied sciences. A related foundational challenging is the educational process, which was and still is an unlimited challenge for teachers and professors: i.e., levels of understanding, curricula, (...) activing critical engagement, transfer knowledge—and—skills, management, classroom and subsequently pre-service teachers need special teacher education. Taking into account Joule’s bicentenary commemoration in physics and Nature of Science teaching this paper introduces to a level of inquiring within historical and NoS approaches in the pre-service teachers, typically science, technology, engineering and mathematics. In particular, history and historiography of Joule’s physics are dealt with. (shrink)

Hoerl and McCormack demonstrate that although animals possess a sophisticated temporal updating system, there is no evidence that they also possess a temporal reasoning system. This important case study is directly related to the broader claim that although animals are manifestly capable of first-order relational reasoning, they lack the capacity for higher-order, role-based relational reasoning. We argue this distinction applies to all domains of cognition.