TY - JOUR A1 - Arnold, Holger T1 - A linearized DPLL calculus with learning N2 - This paper describes the proof calculus LD for clausal propositional logic, which is a linearized form of the well-known DPLL calculus extended by clause learning. It is motivated by the demand to model how current SAT solvers built on clause learning are working, while abstracting from decision heuristics and implementation details. The calculus is proved sound and terminating. Further, it is shown that both the original DPLL calculus and the conflict-directed backtracking calculus with clause learning, as it is implemented in many current SAT solvers, are complete and proof-confluent instances of the LD calculus. N2 - Dieser Artikel beschreibt den Beweiskalkül LD für aussagenlogische Formeln in Klauselform. Dieser Kalkül ist eine um Klausellernen erweiterte linearisierte Variante des bekannten DPLL-Kalküls. Er soll dazu dienen, das Verhalten von auf Klausellernen basierenden SAT-Beweisern zu modellieren, wobei von Entscheidungsheuristiken und Implementierungsdetails abstrahiert werden soll. Es werden Korrektheit und Terminierung des Kalküls bewiesen. Weiterhin wird gezeigt, dass sowohl der ursprüngliche DPLL-Kalkül als auch der konfliktgesteuerte Rücksetzalgorithmus mit Klausellernen, wie er in vielen aktuellen SAT-Beweisern implementiert ist, vollständige und beweiskonfluente Spezialisierungen des LD-Kalküls sind. KW - SAT KW - DPLL KW - Klausellernen KW - Automatisches Beweisen KW - SAT KW - DPLL KW - Clause Learning KW - Automated Theorem Proving Y1 - 2007 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-15421 ER - TY - JOUR A1 - Frank, Mario T1 - Axiom relevance decision engine : technical report N2 - This document presents an axiom selection technique for classic first order theorem proving based on the relevance of axioms for the proof of a conjecture. It is based on unifiability of predicates and does not need statistical information like symbol frequency. The scope of the technique is the reduction of the set of axioms and the increase of the amount of provable conjectures in a given time. Since the technique generates a subset of the axiom set, it can be used as a preprocessor for automated theorem proving. This technical report describes the conception, implementation and evaluation of ARDE. The selection method, which is based on a breadth-first graph search by unifiability of predicates, is a weakened form of the connection calculus and uses specialised variants or unifiability to speed up the selection. The implementation of the concept is evaluated with comparison to the results of the world championship of theorem provers of the year 2012 (CASC J6). It is shown that both the theorem prover leanCoP which uses the connection calculus and E which uses equality reasoning, can benefit from the selection approach. Also, the evaluation shows that the concept is applyable for theorem proving problems with thousands of formulae and that the selection is independent from the calculus used by the theorem prover. N2 - Dieser technische Report beschreibt die Konzeption, Implementierung und Evaluation eines Verfahrens zur Auswahl von logischen Formeln bezüglich derer Relevanz für den Beweis einer logischen Formel. Das Verfahren wird ausschließlich für die Prädikatenlogik erster Ordnung angewandt, wenngleich es auch für höherstufige Prädikatenlogiken geeignet ist. Das Verfahren nutzt eine unifikationsbasierte Breitensuche im Graphen wobei jeder Knoten im Graphen ein Prädikat und jede existierende Kante eine Unifizierbarkeitsrelation ist. Ziel des Verfahrens ist die Reduktion einer gegebenen Menge von Formeln auf eine für aktuelle Theorembeweiser handhabbare Größe. Daher ist das Verfahren als Präprozess-Schritt für das automatische Theorembeweisen geeignet. Zur Beschleunigung der Suche wird neben der Standard-Unifikation eine abgeschwächte Unifikation verwendet. Das System wurde während der Weltmeisterschaft der Theorembeweiser im Jahre 2014 (CASC J6) in Manchester zusammen mit dem Theorembeweiser leanCoP eingereicht und konnte leanCoP dabei unterstützen, Probleme zu lösen, die leanCoP alleine nicht handhaben kann. Die Tests mit leanCoP und dem Theorembeweiser E im Nachgang zu der Weltmeisterschaft zeigen, dass das Verfahren unabhängig von dem verwendeten Kalkül ist und bei beiden Theorembeweisern positive Auswirkungen auf die Beweisbarkeit von Problemen mit großen Formelmengen hat. KW - Relevanz KW - Graphensuche KW - Theorembeweisen KW - Preprocessing KW - Unifikation KW - relevance KW - graph-search KW - preprocessing KW - unification KW - theorem Y1 - 2012 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-72128 ER - TY - JOUR A1 - Nylén, Aletta A1 - Dörge, Christina T1 - Using competencies to structure scientific writing education JF - Commentarii informaticae didacticae : (CID) N2 - Scientific writing is an important skill for computer science and computer engineering professionals. In this paper we present a writing concept across the curriculum program directed towards scientific writing. The program is built around a hierarchy of learning outcomes. The hierarchy is constructed through analyzing the learning outcomes in relation to competencies that are needed to fulfill them. Y1 - 2013 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-64851 SN - 1868-0844 SN - 2191-1940 IS - 5 SP - 33 EP - 44 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - JOUR A1 - Lewin, Cathy A1 - McNicol, Sarah T1 - Supporting the Development of 21st Century Skills through ICT JF - KEYCIT 2014 - Key Competencies in Informatics and ICT N2 - The growing impact of globalisation and the development of a ‘knowledge society’ have led many to argue that 21st century skills are essential for life in twenty-first century society and that ICT is central to their development. This paper describes how 21st century skills, in particular digital literacy, critical thinking, creativity, communication and collaboration skills, have been conceptualised and embedded in the resources developed for teachers in iTEC, a four-year, European project. The effectiveness of this approach is considered in light of the data collected through the evaluation of the pilots, which considers both the potential benefits of using technology to support the development of 21st century skills, but also the challenges of doing so. Finally, the paper discusses the learning support systems required in order to transform pedagogies and embed 21st century skills. It is argued that support is required in standards and assessment; curriculum and instruction; professional development; and learning environments. KW - 21st century skills, KW - primary education KW - secondary education KW - pedagogy KW - innovation Y1 - 2015 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-82672 SN - 1868-0844 SN - 2191-1940 IS - 7 SP - 181 EP - 198 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - JOUR A1 - Magenheim, Johannes A1 - Nelles, Wolfgang A1 - Neugebauer, Jonas A1 - Ohrndorf, Laura A1 - Schaper, Niclas A1 - Schubert, Sigrid T1 - Expert Rating of Competence Levels in Upper Secondary Computer Science Education JF - KEYCIT 2014 - Key Competencies in Informatics and ICT N2 - In the project MoKoM, which is funded by the German Research Foundation (DFG) from 2008 to 2012, a test instrument measuring students’ competences in computer science was developed. This paper presents the results of an expert rating of the levels of students’ competences done for the items of the instrument. At first we will describe the difficulty-relevant features that were used for the evaluation. These were deduced from computer science, psychological and didactical findings and resources. Potentials and desiderata of this research method are discussed further on. Finally we will present our conclusions on the results and give an outlook on further steps. KW - Competence Modelling KW - Competence Measurement KW - Informatics System Application KW - Informatics System Comprehension KW - Informatics Modelling KW - Secondary Education Y1 - 2015 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-82683 SN - 1868-0844 SN - 2191-1940 IS - 7 SP - 199 EP - 216 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - JOUR A1 - Opel, Simone A1 - Kramer, Matthias A1 - Trommen, Michael A1 - Pottbäcker, Florian A1 - Ilaghef, Youssef T1 - BugHunt BT - A Motivating Approach to Self-Directed Problem-solving in Operating Systems JF - KEYCIT 2014 - Key Competencies in Informatics and ICT N2 - Competencies related to operating systems and computer security are usually taught systematically. In this paper we present a different approach, in which students have to remove virus-like behaviour on their respective computers, which has been induced by software developed for this purpose. They have to develop appropriate problem-solving strategies and thereby explore essential elements of the operating system. The approach was implemented exemplarily in two computer science courses at a regional general upper secondary school and showed great motivation and interest in the participating students. KW - Educational software KW - operating system KW - student activation KW - problem-solving KW - interactive course KW - interactive workshop KW - edutainment KW - secondary computer science education Y1 - 2015 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-82693 SN - 1868-0844 SN - 2191-1940 IS - 7 SP - 217 EP - 233 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - JOUR A1 - Passig, David A1 - Tzuriel, David A1 - Kedmi, Ganit Eshel T1 - Improving children’s Cognitive Modifiability through Mediated Learning and Dynamic Assessment within 3D Immersive Virtual Reality Environment JF - KEYCIT 2014 - Key Competencies in Informatics and ICT N2 - The objectives of this study were to examine (a) the effect of dynamic assessment (DA) in a 3D Immersive Virtual Reality (IVR) environment as compared with computerized 2D and noncomputerized (NC) situations on cognitive modifiability, and (b) the transfer effects of these conditions on more difficult problem solving administered two weeks later in a non-computerized environment. A sample of 117 children aged 6:6-9:0 years were randomly assigned into three experimental groups of DA conditions: 3D, 2D, and NC, and one control group (C). All groups received the pre- and post-teaching Analogies subtest of the Cognitive Modifiability Battery (CMB-AN). The experimental groups received a teaching phase in conditions similar to the pre-and post-teaching phases. The findings showed that cognitive modifiability, in a 3D IVR, was distinctively higher than in the two other experimental groups (2D computer group and NC group). It was also found that the 3D group showed significantly higher performance in transfer problems than the 2D and NC groups. KW - Dynamic assessment KW - mediated learning experience KW - cognitive modifiability KW - analogical thinking KW - virtual reality Y1 - 2015 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-82705 SN - 1868-0844 SN - 2191-1940 IS - 7 SP - 235 EP - 252 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - JOUR A1 - Saito, Toshinori T1 - The Key Competencies in Informatics and ICT viewed from Nussbaum’s Ten Central Capabilities JF - KEYCIT 2014 - Key Competencies in Informatics and ICT N2 - This article shows a discussion about the key competencies in informatics and ICT viewed from a philosophical foundation presented by Martha Nussbaum, which is known as ‘ten central capabilities’. Firstly, the outline of ‘The Capability Approach’, which has been presented by Amartya Sen and Nussbaum as a theoretical framework of assessing the state of social welfare, will be explained. Secondly, the body of Nussbaum’s ten central capabilities and the reason for being applied as the basis of discussion will be shown. Thirdly, the relationship between the concept of ‘capability’ and ‘competency’ is to be discussed. After that, the author’s assumption of the key competencies in informatics and ICT led from the examination of Nussbaum’s ten capabilities will be presented. KW - Capability approach KW - competency KW - teaching informatics in general education KW - philosophical foundation of informatics pedagogy KW - education and public policy Y1 - 2015 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-82718 SN - 1868-0844 SN - 2191-1940 IS - 7 SP - 253 EP - 266 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - JOUR A1 - Webb, Mary T1 - Considerations for the Design of Computing Curricula JF - KEYCIT 2014 - Key Competencies in Informatics and ICT N2 - This paper originated from discussions about the need for important changes in the curriculum for Computing including two focus group meetings at IFIP conferences over the last two years. The paper examines how recent developments in curriculum, together with insights from curriculum thinking in other subject areas, especially mathematics and science, can inform curriculum design for Computing. The analysis presented in the paper provides insights into the complexity of curriculum design as well as identifying important constraints and considerations for the ongoing development of a vision and framework for a Computing curriculum. KW - Curriculum KW - Computer Science KW - Informatics KW - curriculum theory Y1 - 2015 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-82723 SN - 1868-0844 SN - 2191-1940 IS - 7 SP - 267 EP - 283 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - JOUR A1 - Curzon, Paul T1 - Unplugged Computational Thinking for Fun JF - KEYCIT 2014 - Key Competencies in Informatics and ICT N2 - Computational thinking is a fundamental skill set that is learned by studying Informatics and ICT. We argue that its core ideas can be introduced in an inspiring and integrated way to both teachers and students using fun and contextually rich cs4fn ‘Computer Science for Fun’ stories combined with ‘unplugged’ activities including games and magic tricks. We also argue that understanding people is an important part of computational thinking. Computational thinking can be fun for everyone when taught in kinaesthetic ways away from technology. KW - Computational thinking KW - cs4fn KW - ‘unplugged’ computing KW - kinaesthetic teaching KW - fun Y1 - 2015 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-82575 SN - 1868-0844 SN - 2191-1940 IS - 7 SP - 15 EP - 27 PB - Universitätsverlag Potsdam CY - Potsdam ER -