In this paper, we present the main lines and a first implementation of an open general parallel architecture that we propose for various computation problems about Quantified Boolean Formulae. One main feature of our approach is to deal with QBF without syntactic restrictions, as prenex form or conjunctive normal form. Another main point is to develop a general parallel framework in which we will be able in the future to introduce various specialized algorithms dedicated to particular subproblems.

The natural way to use Answer Set Programming (ASP) to represent knowledge in Artificial Intelligence or to solve a Constraint Satisfaction Problem is to elaborate a first order logic program with default negation. In a preliminary step this program, with variables, is translated in an equivalent propositional one by a first tool: the grounder. Then, the propositional program is given to a second tool: the solver. This last one computes (if they exist) one or many answer sets (models) of the program, each answer set encoding one solution of the initial problem. Until today, almost all ASP systems apply this two steps computation. In this work, our major contribution is to introduce a new approach of answer set computing that escapes the preliminary phase of rule instantiation by integrating it in the search process. Our methodology applies a forward chaining of first order rules that are grounded on the fly by means of previously produced constants. We have implemented this strategy in our new ASP solver ASPeRiX . The first benefit of our work is to avoid the bottleneck of instantiation phase arising for some problems because of the huge amount of memory needed to ground all rules of a program, even if these rules are not really useful in certain cases. The second benefit is to make the treatment of function symbols easier and without syntactic restriction provided that rules are safe.

We present the first version of our ASP solver ASPeRiX that implements a new approach of answer set computation. The main specifity of our system is to realize a forward chaining of first order rules that are grounded on the fly. So, unlike all others available ASP systems ASPeRiX does not need a pregrounding processing.

Answer Set Programming (ASP), via normal logic programs, is known as a suitable framework for default reasoning since it offers both a valid formal model and operational systems. However, in front of a real world knowledge representation problem, it is not easy to represent information in this framework. That is why the present article proposed to deal with this issue by generating in an automatic way the suitable normal logic program from a compact representation of the information. This is done by using a method, based on specificity, that has been developed for default logic and which is adapted here to ASP both in theoretical and practical points of view.

We propose in this article a translation from quantified Boolean formulae to answer set programming. The computation of a solution of a quantified Boolean formula is then equivalent to the computation of a stable model for a normal logic program. The case of unquantified Boolean formulae is also considered since it is equivalent to the case of quantified Boolean formulae with only existential quantifiers.

The goal of the present study was to develop and evaluate a new method for the prediction of unexplained syncope occurrences. Diagnosis of syncope is currently based on the reproduction of symptoms in combination with hypotension and bradycardia induced by a 45 min 60-70 degrees head-upright tilt test (HUTT). The main drawback of this widely used test concerns its duration that reaches 55 min if the patient does not faint. Our method is a first step in the avoidance of the HUTT. An electrocardiogram and a transthoracic impedance waveform were recorded for 10 min of supine rest of a HUTT in 128 patients with a history of unexplained recurrent syncope. Seven indices were computed on the transthoracic impedance and its first derivative. The prediction quality of every subset of these variables, mixed with age and sex, has been tested by a support vector machine in a retrospective group of 64 patients (100% of sensitivity and 100% of specificity was reached). The best subset obtained has been evaluated prospectively in a group of 64 patients (94% of sensitivity and 79% of specificity was reached). These results compare very favorably with published results for other unexplained syncope detectors.

The aim of this study is to develop a method to predict unexplained syncope. Its diagnosis is currently based on the reproduction of symptoms induced by a 45-min of 60-80deg head-upright tilt test (HUTT). The main drawback of this test concerns its duration which can reach 45 minutes, therefore our study proposes an analysis which is only based on the 10 first minutes of the test. An important number of variables is obtained during the HUTT. To reduce and to select the most relevant variables, many feature selection methods are used and compared to obtain groups of pertinent variables. We used classification tools to achieve significant syncope outcome prediction.

The aim of this study is to present a method that predicts unexplained syncope or presyncope occurrences induced by a head-upright tilt-test (HUTT). The HUTT is based on the reproduction of symptoms in combination with hypotension and bradycardia induced by a tilt at 70° during 45 minutes. The main drawback is the duration of this test because, by adding the supine position of 10 minutes, the test could reach 55 minutes. Therefore, this paper proposes a new method for syncope prediction by using only the supine position. We describe the signals used to extract the features employed for the prediction and we develop the preprocessing techniques of these signals in order to increase the quality interpretation of these features. We conclude by presenting the results obtained by the use of an artificial neural network.

Using Answer Set Programming in an Inference-Based approach to Natural Language Semantics

In this work, we introduce a new framework able to deal with a reasoning that is at the same time non monotonic and uncertain. In order to take into account a certainty level associated to each piece of knowledge, we use possibility theory to extend the non monotonic semantics of stable models for logic programs with default negation. By means of a possibility distribution we define a clear semantics of such programs by introducing what is a possibilistic stable model. We also propose a syntactic process based on a fix-point operator to compute these particular models representing the deductions of the program and their certainty. Then, we show how this introduction of a certainty level on each rule of a program can be used in order to restore its consistency in case of the program has no model at all. Furthermore, we explain how we can compute possibilistic stable models by using available softwares for Answer Set Programming and we describe the main lines of the system that we have developed to achieve this goal.

Possibilistic Stable model Semantics is an extension of Stable Model Semantics that allows to merge uncertain and non monotonic reasoning into a unique framework. To achieve this aim, knowledge is represented by a normal logic program where each rule is given with its own degree of certainty. By this way, it formally defines a distribution of possibility over atom sets that, on its turn, induces for each atom a possibility and a necessity measures. The latter underpins the definition of a possibilistic stable model in which every consequence of the program is given with a level of certainty. In this work we explain how we can compute the possibilistic stable models of a possibilistic normal logic program by using available softwares for Answer Set Programming and we describe the main lines of the system that we have developed.

We present a uniform framework for implementing the variety of consistency checks needed for an implementation platform for query-answering in default logics. Our approach is centered around the concept of local proof procedures that allow for validating each inference step when it is performed. The resulting system is unique in offering simultaneously the expressiveness of multiple default logics.

XRay is a theorem prover for default logics. Its deductive power is primarily due to our approach of integrating default reasoning into existing model elimination based provers using the well-known PTTP approach. We conceived and integrated a number of enhancements, such as lemma handling, regularity-based truncations of underlying search spaces and a model-based approach to consistency checking.

We present here a correct and complete theorem prover for a certain class of formulas in Lukaszewicz' default logic. Whereas many papers are concerned by calculus of extensions for some default logic, we have developed a theorem prover, that means a computation method to check whether a given formula belongs to some extension of a default theory. This theorem prover works in Lukaszewicz' default logic, which ensures that an extension always exists. More precisely, we define a class of formulas called range-restricted Horn default logic. The restriction to Horn logic enables to use SLD-resolution to build proofs. Moreover range restriction, the constraint on variables occurring in the formulas, enables to deal with open defaults by using the unification mechanism. This point is quite original since open defaults are usually replaced by a set of instanciated defaults. Another point is the fact that computing a proof (in a backward chaining way), instead of building an extension (in a forward chaining way or by eliminating conflicts between defaults), allows us to hope a better efficiency in presence of open defaults.

We present an implementation platform for query-answering in default logics. The overall approach along with its implementation, the XRay system, allows for query-answering from default theories supporting local proof procedures. The deductive power of XRay stems from it susage of Prolog Technology Theorem Proving Techniques (PTTP) supported by further enhancements, such as default lemma handling and regularity-based truncations of the underlying search space. The generality of the approach, allowing for a (simultaneous) treatment of different default logics, stems from a novel model-based approach to consistency checking.

Both in classical logic and in Answer Set Programming, inconsistency is characterized by non existence of a model. Whereas every formula is a theorem for inconsistent set of formulas, an inconsistent program has no answer. Even if these two results seem opposite, they share the same drawback: the knowledge base is useless since one can not draw valid conclusions from it. Possibilistic logic is a logic of uncertainty able to deal with inconsistency in classical logic. By putting on every formula a degree of certainty, it defines a way to compute, with regard to these degrees, a consistent subset of formulas that can be then used in a classical inference process. In this work, we address the treatment of inconsistency in Answer Set Programming by a possibilistic approach that takes into account the non monotonic aspect of the framework.

In this work, we define a new framework in order to improve the knowledge representation power of Answer Set Programming paradigm. Our proposal is to use notions from possibility theory to extend the stable model semantics by taking into account a certainty level, expressed in terms of necessity measure, on each rule of a normal logic program. First of all, we introduce possibilistic definite logic programs and show how to compute the conclusions of such programs both in syntactic and semantic ways. The syntactic handling is done by help of a fix-point operator, the semantic part relies on a possibility distribution on all sets of atoms and we show that the two approaches are equivalent. In a second part, we define what is a possibilistic stable model for a normal logic program, with default negation. Again, we define a possibility distribution allowing to determine the stable models.

In Answer Set Programming it is not possible to deduce any conclusion from an inconsistent program (ie: a program that has no model). The same issue occurs in classical logic where there exist some techniques to handle this inconsistency. In this work, we propose to manage inconsistent logic programs in a similar way as possibilistic logic does for classical logic. We compute a consistent subprogram keeping the most important rules of the original program. This importance is described by a necessity degree assigned to each rule.