## Institut für Informatik und Computational Science

### Refine

#### Has Fulltext

- no (754) (remove)

#### Year of publication

#### Document Type

- Article (480)
- Monograph/Edited Volume (133)
- Doctoral Thesis (115)
- Part of a Book (11)
- Conference Proceeding (5)
- Other (5)
- Preprint (4)
- Review (1)

#### Keywords

- Answer set programming (5)
- Answer Set Programming (3)
- answer set programming (3)
- Automata systems (2)
- E-learning (2)
- TPACK (2)
- Theory (2)
- cooperating systems (2)
- e-learning (2)
- formal languages (2)
- 3D modeling (1)
- 3D visualization (1)
- AODV (1)
- Abstraction (1)
- Access control (1)
- Active evaluation (1)
- Ad hoc routing (1)
- Adaptivity (1)
- Android Security (1)
- App (1)
- Apps (1)
- Augmentation (1)
- Backdoors (1)
- Barcode (1)
- Batch processing (1)
- Berliner Modell (1)
- Boolean logic models (1)
- CP-Logic (1)
- Campus (1)
- Chipkarten (1)
- Cloud (1)
- Cluster Computing (1)
- Cluster computing (1)
- Code generation (1)
- Coherent phonons (1)
- Combinatorial multi-objective optimization (1)
- Complex optimization (1)
- Computational complexity (1)
- Computational grid (1)
- Context awareness (1)
- Contextualized learning (1)
- Continuous Testing (1)
- Continuous Versioning (1)
- D-galactosamine (1)
- DRMAA (1)
- DRMS (1)
- Data federation (1)
- Deal of the Day (1)
- Debugging (1)
- Decidability (1)
- Design (1)
- Design for testability (DFT) (1)
- Deutschland (1)
- Digitale Medien (1)
- Dynamical X-ray theory (1)
- E-teaching (1)
- Educational game (1)
- Evaluation (1)
- Event mapping (1)
- Evolution (1)
- Experimentation (1)
- Explore-first Programming (1)
- Extensibility (1)
- Extreme Model-Driven Development (1)
- Fault Localization (1)
- Framework (1)
- Freshmen (1)
- Green computing (1)
- Grounded theory (1)
- Heat diffusion (1)
- Hierarchically configurable mask register (1)
- Hochschul-Apps (1)
- Hochschul-Cloud (1)
- Hochschullehre (1)
- Human Factors (1)
- Hybrid App (1)
- IaaS (1)
- Identifiers (1)
- Image and video stylization (1)
- Incoherent phonons (1)
- Incremental answer set programming (1)
- Information federation (1)
- Information integration (1)
- Information retrieval (1)
- Information security (1)
- Internet (1)
- Job monitoring (1)
- Job submission (1)
- Kernelization (1)
- Knowledge representation (1)
- Kommunismus (1)
- L systems (1)
- Landmark visibility (1)
- Lehre (1)
- Load Balancing (1)
- Localization (1)
- Location awareness (1)
- Logic programming (1)
- Loyalty (1)
- Markov processes (1)
- Masking of X-values (1)
- Massenklausuren (1)
- Meta-Programming (1)
- Mobile Campus Application (1)
- Mobile Learning (1)
- Mobile application (1)
- Mobile devices (1)
- Mobile learning (1)
- Model checking (1)
- Multimedia (1)
- Multiple interpretation scheme (1)
- N-temperature model (1)
- NFC (1)
- Nash equilibrium (1)
- Nonmonotonic reasoning (1)
- OBI (1)
- OCCI (1)
- Open Badge Infrastructure (1)
- Open Badges (1)
- Operation problem (1)
- Parallel job execution time estimation (1)
- Parameterized complexity (1)
- Pedestrian navigation (1)
- Peer-Review (1)
- Performance Evaluation (1)
- Personal Learning Environment (1)
- Personalization (1)
- Pervasive computing (1)
- Pervasive game (1)
- Pervasive learning (1)
- Preference Handling (1)
- Privacy Protection (1)
- Process mining (1)
- Process model analysis (1)
- Product lifecycle management (1)
- Professionalisierung (1)
- Prototyping (1)
- Prüfungsoptimierung (1)
- REST (1)
- RSA triangle (1)
- Ranking (1)
- Reflexion (1)
- SAMR (1)
- SOA (1)
- SaaSAbstract (1)
- Seamless learning (1)
- Semantic data (1)
- Semantic web (1)
- Service orientation (1)
- Service-oriented Architecture (1)
- Service-oriented architecture (1)
- Signaling transduction networks (1)
- Static Analysis (1)
- Statistical relational learning (1)
- Stochastic relational process (1)
- Structural equation modeling (1)
- Studieneinstieg (1)
- Studienorganisation (1)
- Systems biology (1)
- Teilnehmerzertifikate (1)
- Thermoelasticity (1)
- Time series (1)
- Tracking (1)
- Ubiquitous learning (1)
- Ultrafast dynamics (1)
- Unary languages (1)
- Uniform Access Principle (1)
- University Service Bus (1)
- Usability testing (1)
- User submission pattern (1)
- User-centred design (1)
- Verification (1)
- Webanwendung (1)
- Wireless Sensor Networks (1)
- X-masking (1)
- X-values (1)
- acute liver failure (1)
- adversarial classification (1)
- algorithm schedules (1)
- artistic rendering (1)
- behavioral abstraction (1)
- belief merging (1)
- belief revision (1)
- bioinformatics (1)
- block representation (1)
- bootstrapping (1)
- cellular automata (1)
- code generation (1)
- collaborative learning (1)
- combined task and motion planning (1)
- conductive argument (1)
- consistency (1)
- consistency checking (1)
- consistency measures (1)
- controlled vocabularies (1)
- course timetabling (1)
- decidability questions (1)
- declarative problem solving (1)
- diagnosis (1)
- domain-specific APIs (1)
- dynamic service binding (1)
- eLectures (1)
- educational timetabling (1)
- endothelin (1)
- endothelin-converting enzyme (1)
- evolution (1)
- external ambiguity (1)
- finite model computation (1)
- formal argumentation systems (1)
- geovisualization (1)
- informal logic (1)
- internal ambiguity (1)
- kidney cancer (1)
- loop formulas (1)
- loose programming (1)
- manipulation planning (1)
- metabolism (1)
- metabolomics (1)
- metadata (1)
- metastasis (1)
- mobile Applikationen (1)
- natural language generation (1)
- neighborhood (1)
- neutral endopeptidase (1)
- nonphotorealistic rendering (NPR) (1)
- o-ambiguity (1)
- plug-ins (1)
- portfolio-based solving (1)
- premise acceptability (1)
- process model alignment (1)
- process modeling (1)
- program encodings (1)
- proof complexity (1)
- quantum (1)
- real arguments (1)
- reference (1)
- referential effectiveness (1)
- regular language (1)
- relevance (1)
- semantic web (1)
- simplicity (1)
- stable model semantics (1)
- static prediction games (1)
- strong equivalence (1)
- sufficiency (1)
- tableau calculi (1)
- tele-teaching (1)
- test response compaction (1)
- theory of computation (1)
- triangulated irregular networks (1)
- unfounded sets (1)
- video annotation (1)
- xAPI (1)

"Deal of the Day" (DoD) platforms have quickly become popular by offering savings on local services, products and vacations. For merchants, these platforms represent a new marketing channel to advertise their products and services and attract new customers. DoD platform providers, however, struggle to maintaining a stable market share and profitability, because entry and switching costs are low. To sustain a competitive market position, DoD providers are looking for ways to build a loyal customer base. However, research examining the determinants of user loyalty in this novel context is scarce. To fill this gap, this study employs Grounded Theory methodology to develop a conceptual model of customer loyalty to a DoD provider. In the next step, qualitative insights are enriched and validated using quantitative data from a survey of 202 DoD users. The authors find that customer loyalty is in large part driven by monetary incentives, but can be eroded if impressions from merchant encounters are below expectations. In addition, enhancing the share of deals relevant for consumers, i.e. signal-to-noise ratio, and mitigating perceived risks of a transaction emerge as challenges. Beyond theoretical value, the results offer practical insights into how customer loyalty to a DoD provider can be promoted.

(Near-)inverses of sequences
(2006)

We introduce the notion of a near-inverse of a non-decreasing sequence of positive integers; near-inverses are intended to assume the role of inverses in cases when the latter cannot exist. We prove that the near-inverse of such a sequence is unique; moreover, the relation of being near-inverses of each other is symmetric, i.e. if sequence g is the near-inverse of sequence f, then f is the near-inverse of g. There is a connection, by approximations, between near- inverses of sequences and inverses of continuous strictly increasing real-valued functions which can be exploited to derive simple expressions for near-inverses

In recent years, there has been a large amount of disparate work concerning the representation and reasoning with qualitative preferential information by means of approaches to nonmonotonic reasoning. Given the variety of underlying systems, assumptions, motivations, and intuitions, it is difficult to compare or relate one approach with another. Here, we present an overview and classification for approaches to dealing with preference. A set of criteria for classifying approaches is given, followed by a set of desiderata that an approach might be expected to satisfy. A comprehensive set of approaches is subsequently given and classified with respect to these sets of underlying principles

We consider the problem of representing arbitrary preferences in causal reasoning and planning systems. In planning, a preference may be seen as a goal or constraint that is desirable, but not necessary, to satisfy. To begin, we define a very general query language for histories, or interleaved sequences of world states and actions. Based on this, we specify a second language in which preferences are defined. A single preference defines a binary relation on histories, indicating that one history is preferred to the other. From this, one can define global preference orderings on the set of histories, the maximal elements of which are the preferred histories. The approach is very general and flexible; thus it constitutes a base language in terms of which higher-level preferences may be defined. To this end, we investigate two fundamental types of preferences that we call choice and temporal preferences. We consider concrete strategies for these types of preferences and encode them in terms of our framework. We suggest how to express aggregates in the approach, allowing, e.g. the expression of a preference for histories with lowest total action costs. Last, our approach can be used to express other approaches and so serves as a common framework in which such approaches can be expressed and compared. We illustrate this by indicating how an approach due to Son and Pontelli can be encoded in our approach, as well as the language PDDL3.

Mobile devices and associated applications (apps) are an indispensable part of daily life and provide access to important information anytime and anywhere. However, the availability of university-wide services in the mobile sector is still poor. If they exist they usually result from individual activities of students and teachers. Mobile applications can have an essential impact on the improvement of students’ self-organization as well as on the design and enhancement of specific learning scenarios, though. This article introduces a mobile campus app framework, which integrates central campus services and decentralized learning applications. An analysis of strengths and weaknesses of different approaches is presented to summarize and evaluate them in terms of requirements, development, maintenance and operation. The article discusses the underlying service-oriented architecture that allows transferring the campus app to other universities or institutions at reasonable cost. It concludes with a presentation of the results as well as ongoing discussions and future work

A method of construction of combinational self-checking units with detection of all single faults
(1999)

We address the problem of belief change in (nonmonotonic) logic programming under answer set semantics. Our formal techniques are analogous to those of distance-based belief revision in propositional logic. In particular, we build upon the model theory of logic programs furnished by SE interpretations, where an SE interpretation is a model of a logic program in the same way that a classical interpretation is a model of a propositional formula. Hence we extend techniques from the area of belief revision based on distance between models to belief change in logic programs.
We first consider belief revision: for logic programs P and Q, the goal is to determine a program R that corresponds to the revision of P by Q, denoted P * Q. We investigate several operators, including (logic program) expansion and two revision operators based on the distance between the SE models of logic programs. It proves to be the case that expansion is an interesting operator in its own right, unlike in classical belief revision where it is relatively uninteresting. Expansion and revision are shown to satisfy a suite of interesting properties; in particular, our revision operators satisfy all or nearly all of the AGM postulates for revision.
We next consider approaches for merging a set of logic programs, P-1,...,P-n. Again, our formal techniques are based on notions of relative distance between the SE models of the logic programs. Two approaches are examined. The first informally selects for each program P-i those models of P-i that vary the least from models of the other programs. The second approach informally selects those models of a program P-0 that are closest to the models of programs P-1,...,P-n. In this case, P-0 can be thought of as a set of database integrity constraints. We examine these operators with regards to how they satisfy relevant postulate sets.
Last, we present encodings for computing the revision as well as the merging of logic programs within the same logic programming framework. This gives rise to a direct implementation of our approach in terms of off-the-shelf answer set solvers. These encodings also reflect the fact that our change operators do not increase the complexity of the base formalism.

In this article, we consider high-dimensional data which contains a low-dimensional non-Gaussian structure contaminated with Gaussian noise and propose a new linear method to identify the non-Gaussian subspace. Our method NGCA (Non-Gaussian Component Analysis) is based on a very general semi-parametric framework and has a theoretical guarantee that the estimation error of finding the non-Gaussian components tends to zero at a parametric rate. NGCA can be used not only as preprocessing for ICA, but also for extracting and visualizing more general structures like clusters. A numerical study demonstrates the usefulness of our method

Scheduling performance in computational grid can potentially benefit a lot from accurate execution time estimation for parallel jobs. Most existing approaches for the parallel job execution time estimation, however, require ample past job traces and the explicit correlations between the job execution time and the outer layout parameters such as the consumed processor numbers, the user-estimated execution time and the job ID, which are hard to obtain or reveal. This paper presents and evaluates a novel execution time estimation approach for parallel jobs, the user-behavior clustering for execution time estimation, which can give more accurate execution time estimation for parallel jobs through exploring the job similarity and revealing the user submission patterns. Experiment results show that compared to the state-of-art algorithms, our approach can improve the accuracy of the job execution time estimation up to 5.6 %, meanwhile the time that our approach spends on calculation can be reduced up to 3.8 %.

A polynomial translation of logic programs with nested expressions into disjunctive logic programs
(2002)

We present a new technique for uniquely identifying a single failing vector in an interval of test vectors. This technique is applicable to combinational circuits and for scan-BIST in sequential circuits with multiple scan chains. The proposed method relies on the linearity properties of the MISR and on the use of two test sequences, which are both applied to the circuit under test. The second test sequence is derived from the first in a straightforward manner and the same test pattern source is used for both test sequences. If an interval contains only a single failing vector, the algebraic analysis is guaranteed to identify it. We also show analytically that if an interval contains two failing vectors, the probability that this case is interpreted as one failing vector is very low. We present experimental results for the ISCAS benchmark circuits to demonstrate the use of the proposed method for identifying failing test vectors

Researchers and developers worldwide have put their efforts into the design, development and use of information and communication technology to support teaching and learning. This research is driven by pedagogical as well as technological disciplines. The most challenging ideas are currently found in the application of mobile, ubiquitous, pervasive, contextualized and seamless technologies for education, which we shall refer to as pervasive education. This article provides a comprehensive overview of the existing work in this field and categorizes it with respect to educational settings. Using this approach, best practice solutions for certain educational settings and open questions for pervasive education are highlighted in order to inspire interested developers and educators. The work is assigned to different fields, identified by the main pervasive technologies used and the educational settings. Based on these assignments we identify areas within pervasive education that are currently disregarded or deemed challenging so that further research and development in these fields are stimulated in a trans-disciplinary approach. (C) 2013 Elsevier B.V. All rights reserved.

We discuss the relaxation of a class of nonlinear elliptic Cauchy problems with data on a piece S of the boundary surface by means of a variational approach known in the optimal control literature as "equation error method". By the Cauchy problem is meant any boundary value problem for an unknown function y in a domain X with the property that the data on S, if combined with the differential equations in X, allow one to determine all derivatives of y on S by means of functional equations. In the case of real analytic data of the Cauchy problem, the existence of a local solution near S is guaranteed by the Cauchy-Kovalevskaya theorem. We also admit overdetermined elliptic systems, in which case the set of those Cauchy data on S for which the Cauchy problem is solvable is very "thin". For this reason we discuss a variational setting of the Cauchy problem which always possesses a generalised solution.

The ongoing digitalization leads to a need of continuous change of ICT (Information and Communi-cation Technology) in all university domains and therefore affects all stakeholders in this arena. More and more ICT components, systems and tools occur and have to be integrated into the existing processes and infrastructure of the institutions. These tasks include the transfer of resources and information across multiple ICT systems. By using so-called virtual environments for domains of re-search, education, learning and work, the performance of daily tasks can be aided. Based on a user requirement analysis different short- and long-term objectives were identified and are tackled now in the context of a federal research project. In order to be prepared for the ongoing digitalization, new systems have to be provided. Both, a service-oriented infrastructure and a related web-based virtual learning environment constitute the platform Campus.UP and creates the necessary basis to be ready for future challenges. The current focus lies on e-portfolio work, hence we will present a related focus group evaluation. The results indicate a tremendous need to extend the possibilities of sharing resources across system boundaries, in order to enable a comfortable participation of exter-nal cooperating parties and to clarify the focus of each connected system. The introduction of such an infrastructure implies far-reaching changes for traditional data centers. Therefore, the challenges and risks of faculty conducting innovation projects for the ICT organization are taken as a starting point to stimulate a discussion, how data centers can utilize projects to be ready for the future needs. We are confident that Campus.UP will provide the basis for ensuring the persistent transfer of innovation to the ICT organization and thus will contribute to tackle the future challenges of digitalization.

This paper describes the implementation of a workflow model for service-oriented computing of potential areas for wind turbines in jABC. By implementing a re-executable model the manual effort of a multi-criteria site analysis can be reduced. The aim is to determine the shift of typical geoprocessing tools of geographic information systems (GIS) from the desktop to the web. The analysis is based on a vector data set and mainly uses web services of the “Center for Spatial Information Science and Systems” (CSISS). This paper discusses effort, benefits and problems associated with the use of the web services.

Information integration across company borders becomes increasingly important for the success of product lifecycle management in industry and complex supply chains. Semantic technologies are about to play a crucial role in this integrative process. However, cross-company data exchange requires mechanisms to enable fine-grained access control definition and enforcement, preventing unauthorized leakage of confidential data across company borders. Currently available semantic repositories are not sufficiently equipped to satisfy this important requirement. This paper presents an infrastructure for controlled sharing of semantic data between cooperating business partners. First, we motivate the need for access control in semantic data federations by a case study in the industrial service sector. Furthermore, we present an architecture for controlling access to semantic repositories that is based on our newly developed SemForce security service. Finally, we show the practical feasibility of this architecture by an implementation and several performance experiments.

Evaluating the quality of ranking functions is a core task in web search and other information retrieval domains. Because query distributions and item relevance change over time, ranking models often cannot be evaluated accurately on held-out training data. Instead, considerable effort is spent on manually labeling the relevance of query results for test queries in order to track ranking performance. We address the problem of estimating ranking performance as accurately as possible on a fixed labeling budget. Estimates are based on a set of most informative test queries selected by an active sampling distribution. Query labeling costs depend on the number of result items as well as item-specific attributes such as document length. We derive cost-optimal sampling distributions for the commonly used performance measures Discounted Cumulative Gain and Expected Reciprocal Rank. Experiments on web search engine data illustrate significant reductions in labeling costs.

Owing to the loose coupling between replicas, the replica-exchange (RE) class of algorithms should be able to benefit greatly from using as many resources as available. However, the ability to effectively use multiple distributed resources to reduce the time to completion remains a challenge at many levels. Additionally, an implementation of a pleasingly distributed algorithm such as replica-exchange, which is independent of infrastructural details, does not exist. This paper proposes an extensible and scalable framework based on Simple API for Grid Applications that provides a general-purpose, opportunistic mechanism to effectively use multiple resources in an infrastructure-independent way. By analysing the requirements of the RE algorithm and the challenges of implementing it on real production systems, we propose a new abstraction (BIGJOB), which forms the basis of the adaptive redistribution and effective scheduling of replicas.

The introduction of columnar in-memory databases, along with hardware evolution, has made the execution of transactional and analytical enterprise application workloads on a single system both feasible and viable. Yet, we argue that executing analytical aggregate queries directly on the transactional data can decrease the overall system performance. Despite the aggregation capabilities of columnar in-memory databases, the direct access to records of a materialized aggregate is always more eﬃcient than aggregating on the ﬂy. The traditional approach to materialized aggregates, however, introduces signiﬁcant overhead in terms of materialized view selection, maintenance, and exploitation. When this overhead is handled by the application, it increases the application complexity, and can slow down the transactional throughput of inserts, updates, and deletes.
In this thesis, we motivate, propose, and evaluate the aggregate cache, a materialized aggregate engine in the main-delta architecture of a columnar in-memory database that provides eﬃcient means to handle costly aggregate queries of enterprise applications. For our design, we leverage the speciﬁcs of the main-delta architecture that separates a table into a main and delta partition. The central concept is to only cache the partial aggregate query result as deﬁned on the main partition of a table, because the main partition is relatively stable as records are only inserted into the delta partition. We contribute by proposing incremental aggregate maintenance and query compensation techniques for mixed workloads of enterprise applications. In addition, we introduce aggregate proﬁt metrics that increase the likelihood of persisting the most proﬁtable aggregates in the aggregate cache.
Query compensation and maintenance of materialized aggregates based on joins of multiple tables is expensive due to the partitioned tables in the main-delta architecture. Our analysis of enterprise applications has revealed several data schema and workload patterns. This includes the observation that transactional data is persisted in header and item tables, whereas in many cases, the insertion of related header and item records is executed in a single database transaction. We contribute by proposing an approach to transport these application object semantics to the database system and optimize the query processing using the aggregate cache by applying partition pruning and predicate pushdown techniques.
For the experimental evaluation, we propose the FICO benchmark that is based on data from a productive ERP system with extracted mixed workloads. Our evaluation reveals that the aggregate cache can accelerate the execution of aggregate queries up to a factor of 60 whereas the speedup highly depends on the number of aggregated records in the main and delta partitions. In mixed workloads, the proposed aggregate maintenance and query compensation techniques perform up to an order of magnitude better than traditional materialized aggregate maintenance approaches. The introduced aggregate proﬁt metrics outperform existing costbased metrics by up to 20%. Lastly, the join pruning and predicate pushdown techniques can accelerate query execution in the aggregate cache in the presence of multiple partitioned tables by up to an order of magnitude.

A multiple interpretation scheme is an ordered sequence of morphisms. The ordered multiple interpretation of a word is obtained by concatenating the images of that word in the given order of morphisms. The arbitrary multiple interpretation of a word is the semigroup generated by the images of that word. These interpretations are naturally extended to languages. Four types of ambiguity of multiple interpretation schemata on a language are defined: o-ambiguity, internal ambiguity, weakly external ambiguity and strongly external ambiguity. We investigate the problem of deciding whether a multiple interpretation scheme is ambiguous on regular languages.

Institutions are facing the challenge to integrate legacy systems with steadily growing new ones, using different technologies and interaction patterns. With the demand of offering the best potential of all systems, several not matching systems including their functions have to be aggregated and offered in a useable way. This paper presents an adaptive, generalizable and self-organized Personal Learning Environment (PLE) framework with the potential to integrate several heterogeneous services using a service-oriented architecture. First, a general overview over the field is given, followed by the description of the core components of the PLE framework. A prototypical implementation is presented. Finally, it’s shown how the PLE framework can be dynamically adapted to a changing system environment, reflecting experiences from first user studies.

An asymptotic analysis and improvement of AdaBoost in the binary classification case (in Japanese)
(2000)

Algorithm selection (AS) techniques - which involve choosing from a set of algorithms the one expected to solve a given problem instance most efficiently - have substantially improved the state of the art in solving many prominent AI problems, such as SAT, CSP, ASP, MAXSAT and QBF. Although several AS procedures have been introduced, not too surprisingly, none of them dominates all others across all AS scenarios. Furthermore, these procedures have parameters whose optimal values vary across AS scenarios. This holds specifically for the machine learning techniques that form the core of current AS procedures, and for their hyperparameters. Therefore, to successfully apply AS to new problems, algorithms and benchmark sets, two questions need to be answered: (i) how to select an AS approach and (ii) how to set its parameters effectively. We address both of these problems simultaneously by using automated algorithm configuration. Specifically, we demonstrate that we can automatically configure claspfolio 2, which implements a large variety of different AS approaches and their respective parameters in a single, highly-parameterized algorithm framework. Our approach, dubbed AutoFolio, allows researchers and practitioners across a broad range of applications to exploit the combined power of many different AS methods. We demonstrate AutoFolio can significantly improve the performance of claspfolio 2 on 8 out of the 13 scenarios from the Algorithm Selection Library, leads to new state-of-the-art algorithm selectors for 7 of these scenarios, and matches state-of-the-art performance (statistically) on all other scenarios. Compared to the best single algorithm for each AS scenario, AutoFolio achieves average speedup factors between 1.3 and 15.4.

An Extended Query language for action languages (and its application to aggregates and preferences)
(2006)

We address the problem of Finite Model Computation (FMC) of first-order theories and show that FMC can efficiently and transparently be solved by taking advantage of a recent extension of Answer Set Programming (ASP), called incremental Answer Set Programming (iASP). The idea is to use the incremental parameter in iASP programs to account for the domain size of a model. The FMC problem is then successively addressed for increasing domain sizes until an answer set, representing a finite model of the original first-order theory, is found. We implemented a system based on the iASP solver iClingo and demonstrate its competitiveness by showing that it slightly outperforms the winner of the FNT division of CADE's 2009 Automated Theorem Proving (ATP) competition on the respective benchmark collection.