### Refine

#### Year of publication

- 2004 (5) (remove)

#### Document Type

- Part of Periodical (3)
- Book (1)
- Conference Proceedings (1)

#### Language

- English (3)
- German (1)
- Multiple languages (1)

#### Keywords

- Bildverarbeitung (1)
- DPLL procedure (1)
- Data Analysis (1)
- Datenanalyse (1)
- Farbbildverarbeitung (1)
- KRHyper (1)
- Programm (1)
- Sozialwissenschaftliche Methodenlehre (1)
- Statistics , Social Science Methods (1)
- Statistik (1)
- XML (1)
- color image processing (1)
- e-learning (1)
- first-order logic (1)
- knowledge management system (1)
- living book (1)
- model generation (1)
- sequent calculi (1)

The Living Book is a system for the management of personalized and scenario specific teaching material. The main goal of the system is to support the active, explorative and selfdetermined learning in lectures, tutorials and self study. The Living Book includes a course on 'logic for computer scientists' with a uniform access to various tools like theorem provers and an interactive tableau editor. It is routinely used within teaching undergraduate courses at our university. This paper describes the Living Book and the use of theorem proving technology as a core component in the knowledge management system (KMS) of the Living Book. The KMS provides a scenario management component where teachers may describe those parts of given documents that are relevant in order to achieve a certain learning goal. The task of the KMS is to assemble new documents from a database of elementary units called 'slices' (definitions, theorems, and so on) in a scenario-based way (like 'I want to prepare for an exam and need to learn about resolution'). The computation of such assemblies is carried out by a model-generating theorem prover for first-order logic with a default negation principle. Its input consists of meta data that describe the dependencies between different slices, and logic-programming style rules that describe the scenario-specific composition of slices. Additionally, a user model is taken into account that contains information about topics and slices that are known or unknown to a student. A model computed by the system for such input then directly specifies the document to be assembled. This paper introduces the elearning context we are faced with, motivates our choice of logic and presents the newly developed calculus used in the KMS.

The model evolution calculus
(2004)

The DPLL procedure is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. The recent FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without resorting to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice. In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful litfing of the DPLL procedure, the new calculus contains a more systematic treatment of universal literals, one of FDPLL's optimizations, and so has the potential of leading to much faster implementations.

We aim to demonstrate that automated deduction techniques, in particular those following the model computation paradigm, are very well suited for database schema/query reasoning. Specifically, we present an approach to compute completed paths for database or XPath queries. The database schema and a query are transformed to disjunctive logic programs with default negation, using a description logic as an intermediate language. Our underlying deduction system, KRHyper, then detects if a query is satisfiable or not. In case of a satisfiable query, all completed paths -- those that fulfill all given constraints -- are returned as part of the computed models. The purpose of our approach is to dramatically reduce the workload on the query processor. Without the path completion, a usual XML query processor would search the database for solutions to the query. In the paper we describe the transformation in detail and explain how to extract the solution to the original task from the computed models. We understand this paper as a first step, that covers a basic schema/query reaÂsoning task by model-based deduction. Due to the underlying expressive logic formalism we expect our approach to easily adapt to more sophisticated problem settings, like type hierarchies as they evolve within the XML world.

Computers fundamentally changed the methods used by social scientists during the past decades. It is no exaggeration to state that the wide use and growing user-friendliness of computers and statistical analysis systems helped empirical social research as a subdiscipline to become mainstream. This made a new subdiscipline necessary which is mainly working on adapting and applying computer science methods for social research: social science informatics. This book originated from lecture courses given by the authors from the mid-1980s and developed for computer science students with a minor in social science. Unlike many other introductions to univariate and multivariate data analysis, this book is addressed to advanced scholars and students who apply "classical" statistical methods and who want to get an overview of the mathematical foundations of the methods they apply and who want to avoid the pitfalls of cookbook-like introduction when they interpret their results. The electronic document is a slightly revised version of the printed version of 1994 which has been out of stock for many years.