International Journal on Artificial Intelligence Tools

The Satisfiability Modulo Theories Competition (SMT-COMP) is an annual competition aimed at stimulating the advance of the state-of-the-art techniques and tools developed by the Satisfiability Modulo Theories (SMT) community. As with the first two editions, SMT-COMP 2007 was held as a satellite event of CAV 2007, held July 3-7, 2007. This paper gives an overview of the rules, competition format, benchmarks, participants and results of SMT-COMP 2007.

Reasoning with ontologies is a challenging task specially for non-logic experts. When checking whether an ontology contains rules that contradict each other, current description logic reasoners can only provide a list of the unsatisfiable concepts. Figuring out why these concepts are unsatisfiable, which rules cause conflicts, and how to resolve these conflicts, is all left to the ontology modeler himself. The problem becomes even more challenging in case of large or medium size ontologies, because an unsatisfiable concept may cause many of its neighboring concepts to be unsatisfiable.

The goal of this article is to empower ontology engineering with a user-friendly reasoning mechanism. We propose a pattern-based reasoning approach, which offers 9 patterns of constraint contradictions that lead to unsatisfiability in Object-role (ORM) models. The novelty of this approach is not merely that constraint contradictions are detected, but mainly that it provides the causes and suggestions to resolve contradictions. The approach is implemented in the DogmaModeler ontology engineering tool, and tested in building the CCFORM ontology. We discuss that, although this pattern-based reasoning covers most of contradictions in practice, compared with description logic based reasoning, it is not complete. We argue and illustrate both approaches, pattern-based and description logic-based, their implementation in the DogmaModeler, and conclude that both complement each other from a methodological perspective.

Video segmentation is one of the most important tasks in high-level video processing applications. Stationary cameras are usually used in applications such as video surveillance and human activity recognition. However, possible changes in the background of the video such as waving flags, fluctuating monitors, water surfaces, etc. make the detection of objects of interest particularly challenging. These types of backgrounds are called quasi-stationary backgrounds. In this paper we propose a novel, non-statistical technique to generate a background model and use this model for background subtraction and foreground region detection in the presence of such challenges. The main advantage of the proposed method over the state of the art is that unlike statistical techniques the accuracy of foreground regions is not limited to the estimate of the probability density. Also, the memory requirements of our method are independent of the number of training samples. This makes the proposed method useful in various scenarios including the presence of slow changes in the background. A comprehensive study is presented on the efficiency of the proposed method. Its performance is compared with various existing techniques quantitatively and qualitatively to show its superiority in various applications.

In this paper we study a graph-based approach to the task of Recognizing Textual Entailment between a Text and a Hypothesis. The approach takes into account the full lexico-syntactic context of both the Text and Hypothesis and is based on the concept of subsumption. It starts with mapping the Text and Hypothesis on to graph structures that have nodes representing concepts and edges representing lexico-syntactic relations among concepts. An entailment decision is then made on the basis of a subsumption score between the Text-graph and Hypothesis-graph. The results obtained from a standard entailment test data set were promising. The impact of synonymy on entailment is quantified and discussed. An important advantage to a solution like ours is its ability to be customized to obtain high-confidence results.

In this paper, we present a robust classification technique to disambiguate Greek polysemous words based on hierarchical probabilistic networks. Assuming that the linguistic data of a polysemous word is classified to equivalent classes according to the number of its senses, we try to disambiguate them by using a hierarchical mixture of experts' probabilistic model — a soft version of neural networks that permits overlapping between classes and which is successfully applied in classification tasks. The model is used in combination with an effective feature selection strategy based on a Chi-square test that enhances disambiguation performance. Due to the absence of previous similar work on Greek linguistic data, for comparison we also implement and apply the very popular naïve Bayes classifier to the same data. Comparing the two systems, we find that the Hierarchical Mixtures-of-Experts (HME) model is superior to the naïve Bayes classifier, mainly because of its ability to permit overlapping and the capture of non-linearity among the data. We believe that the system can be successfully applied on real linguistic data after training on a small amount of data.

In this paper we present a radical approach to obtaining a backtrack-free representation for a constraint satisfaction problem: remove values that lead to dead-ends. This technique does not require additional space but has the drawback of removing solutions. We investigate a number of variations on the basic algorithm including the use of seed solutions, consistency techniques, and a variety of pruning heuristics. Our experimental results indicate that a significant proportion of the solutions to the original problem can be retained especially when an optimization algorithm that specifically searches for such “good” backtrack-free representations is employed. Further extensions increase solution retention by searching for high-coverage backtrack-free representations, by removing tuples rather than values, and by combining multiple backtrack-free representations. Our approach elucidates, for the first time, a three-way trade-off between space complexity, potential backtracks, and solution loss and enables algorithms that can actively reason about the trade-off between space, backtracks, and solution loss.

Intensive search schemes are commonly adopted in patched-based texture synthesis to identity the proper neighbors of each patch. However, they do not always provide perfect solutions. This work presents a genetic algorithm in evolutionary computation for patch-based texture synthesis. The representation of an input source texture is first adjusted. Then, the synthesizing result is generated and refined by the selection of individuals based on their fitness and executing crossover and mutation until the criteria are met. After the entire execution, a large output texture is generated with texture features similar to the source texture. Because this approach optimizes the genetic algorithm, the results are satisfactory.

When a Constraint Satisfaction Problem (CSP) admits no solution, it can be useful to pinpoint which constraints are actually contradicting one another and make the problem infeasible. In this paper, a recent heuristic-based approach to compute infeasible minimal subparts of discrete CSPs, also called Minimally Unsatisfiable Cores (MUCs), is improved. The approach is based on the heuristic exploitation of the number of times each constraint has been falsified during previous failed search steps. It appears to enhance the performance of the initial technique, which was the most efficient one until now.

An improved fuzzy C-means (FCM) clustering method is proposed. It incorporates Otsu thresholding with conventional FCM to reduce FCM's susceptibility to local minima, as well as its tendency to derive a threshold that is biased towards the component with larger probability, and derive threshold values with greater accuracy. Thresholding is performed at the cluster boundary region in feature space. A comparison of the results produced by improved and conventional algorithms confirms the superior performance of the former.