| TBA | TBA | To be announced | ... |
| Adrian Nuradiansyah | The Implementation of the Conditions for the Existence of the Most Specific Generalizations w.r.t. General EL-TBoxes | The least common subsumer (lcs) and the most specific concept (msc) are two kinds of non-standard inference in description logic area that generalize a pair of concepts or a single individual into a complex concept. This computation deals with the situation when encountering general EL-TBox such that neither the lcs nor the msc need to exist. Moreover, there have been conditions were already devised to decide whether the lcs and the msc exist w.r.t. general EL-TBox. In this paper, we show how to implement the conditions for the existence of the most specific generalization w.r.t. general EL-TBox in PTime and polynomial bounds on the maximal role depth of the lcs- and the msc-concepts. | |
| Alina Aleksandrova | Engineering Data-Aware Commitment-Based Multiagent Systems | Every large company nowadays represents a complex system, containing distributed units interconnected by social relations. Such systems can be modeled using the Multiagent system (MAS) approach. However, in virtually all current approaches to MAS modeling, data and processes are completely isolated. The result is that the model of the system is not in line with the implementation used at execution time, and that the system components, including their social relation, are not properly captured. In particular, in the last decade the commitment-based approach has been extensively studied to model the social relations in a MAS, and consequently to capture business contracts and interactions at a high-level of abstractions. However, to the best of our knowledge, all existing infrastructures and approaches can operate only with propositional commitments, which leads to seriously downgrade their impact and effectiveness. In this thesis, we show how to build MAS that can be specified using a simple declarative language that accounts for both data and processes. We also attack the problem of using propositional commitments and show the necessity of lifting them to first-order commitments. For this purpose, we propose different possible architectures for modeling data-aware, commitment-regulated MAS, and show a concrete implementation that combines the advantages of the standard relational technology with the well-established JADE multiagent infrastructure. | |
| Adrián Rebola Pardo | Unsatisfiability Proofs for Parity Reasoning in SAT Solving | SAT solvers have become very efficient in the last two decades, due to the use
of many techniques. Because of the increase in code complexity, measures to
increase reliability of results reported by SAT solvers were implemented.
Currently, state-of-the-art SAT solvers are able to produce unsatisfiability
proofs when confronted with an unsatisfiable instance. However, it is not known
how to generate unsatisfiability proofs for a few very proficient techniques,
and this situation forces these techniques to be disabled when unsatisfiability
proofs are required.
One such technique is parity reasoning, which is essential to the application
of SAT solvers to cryptography. In this talk, we solve the problem of
generating unsatisfiability proofs for SAT solvers with integrated parity
reasoning. In doing so, some theoretical contributions are proposed, including
a generalized framework for proof systems that is able to model the DRAT proof
standard, currently used by state-of-the-art solvers.
| |
| Radityo Eko Prasojo | Entity and Aspect Extraction for Organizing News Comments | News websites give their users the opportunity to participate in discussions about published articles, by writing comments. Typically, these comments are unstructured making it hard to understand the flow of user discussions. Thus, there is a need for organizing comments to help users to (1) gain more insights about news topics, and (2) have an easy access to comments that trigger their interests. In this work, we address the above problem by organizing comments around the entities and the aspects they discuss. More specifically, we propose an approach for entity and aspect extraction from user comments through the following contributions. First, we extend traditional Named-Entity Recognition approaches, using coreference resolution and external knowledge bases, to detect more occurrences of entities in comments. Second, we exploit part-of-speech tag, dependency tag, and lexical databases to extract explicit and implicit aspects around discussed entities. Third, we evaluate our entity and aspect extraction approach, on manually annotated data, showing that it highly increases precision and recall compared to baseline approaches. | |
| Agata Ciabattoni | Non classical proofs: theory, applications and tools | Non classical logics provide adequate formalisms for reasoning, e.g., about time, knowledge, dynamic data structures, vague information, resources and algebraic varieties. As such, these logics have been increasingly applied in various disciplines including artificial intelligence, mathematics, and in computer science, where most of these logics originate.
Non classical logics are usually introduced or described in a declarative way in the proof framework due to Hilbert and Frege. However, the resulting systems are extremely cumbersome when it comes to finding or analyzing proofs. Moreover, a Hilbert-Frege system does not help answer useful questions about the formalized logic and the corresponding algebraic structure, such as 'Is the logic decidable?' or 'Does the algebra satisfy amalgamation or a certain order theoretic completion?'. These tasks call for algorithmic presentations of the logics especially in the form of analytic calculi. Analyticity is crucial here since proofs in such calculi proceed by a stepwise decomposition of the objects to be proved. The construction of analytic calculi for non classical logics has long been tailored to each specific logic and the solutions to fundamental questions about these logics and related algebras (decidability, complexity, ...) have largely been investigated on an individual basis.
Our aim is to develop theoretical and engineering tools for automatically extracting analytic calculi for non classical logics from Hilbert-style systems. The resulting tools will be utilized to systematically investigate non classical logics. Various results, currently proved in a logic-specific fashion, will be established in a uniform way for large classes of logics. Our focus will not be on particular calculi, logics or algebras, but on general and uniform results whose instantiations are expected (i) to help logic users in the spirit of 'logic engineering', and (ii) to solve open questions on specific logics, calculi or algebras. | logic.at/START2011 |
