Indécidabilité de la théorie des anneaux de séries formelles à plusieurs indéterminées
Mechanization of inductive reasoning is an exciting research area in artificial intelligence and automated reasoning with many challenges. An overview of our work on mechanizing inductive reasoning based on the cover set method for generating induction schemes from terminating recursive function definitions and using decision procedures is presented. This paper particularly focuses on the recent work on integrating induction into decision procedures without compromising their automation.
Inf-Datalog extends the usual least fixpoint semantics of Datalog with greatest fixpoint semantics: we defined inf-Datalog and characterized the expressive power of various fragments of inf-Datalog in [16]. In the present paper, we study the complexity of query evaluation on finite models for (various fragments of) inf-Datalog. We deduce a unified and elementary proof that global model-checking (i.e. computing all nodes satisfying a formula in a given structure) has 1. quadratic data complexity...
Inf-Datalog extends the usual least fixpoint semantics of Datalog with greatest fixpoint semantics: we defined inf-Datalog and characterized the expressive power of various fragments of inf-Datalog in [CITE]. In the present paper, we study the complexity of query evaluation on finite models for (various fragments of) inf-Datalog. We deduce a unified and elementary proof that global model-checking (i.e. computing all nodes satisfying a formula in a given structure) has 1. quadratic data complexity...
An important field of probability logic is the investigation of inference rules that propagate point probabilities or, more generally, interval probabilities from premises to conclusions. Conditional probability logic (CPL) interprets the common sense expressions of the form “if ..., then ...” by conditional probabilities and not by the probability of the material implication. An inference rule is probabilistically informative if the coherent probability interval of its conclusion is not necessarily...
The information boundedness principle requires that the knowledge obtained as a result of an inference process should not have more information than that contained in the consequent of the rule. From this point of view relevancy transformation operators as a generalization of implications are investigated.
We investigate the logical systems which result from introducing the modalities L and M into the family of substructural implication logics (including relevant, linear and intuitionistic implication). Our results lead to the formulation of a uniform labelled refutation system for these logics.
In this article, we formalized the notion of the integral of a complex-valued function considered as a sum of its real and imaginary parts. Then we defined the measurability and integrability in this context, and proved the linearity and several other basic properties of complex-valued measurable functions. The set of properties showed in this paper is based on [15], where the case of real-valued measurable functions is considered.MML identifier: MESFUN6C, version: 7.9.01 4.101.1015
Based on [16], authors formalized the integral of an extended real valued measurable function in [12] before. However, the integral argued in [12] cannot be applied to real-valued functions unconditionally. Therefore, in this article we have formalized the integral of a real-value function.
We consider the families 𝓛 of propositional superintuitionistic logics (s.i.l.) and NE(K) of normal modal logics (n.m.l.). It is well known that there is a duality between 𝓛 and the lattice of varieties of pseudo-boolean algebras (or Heyting algebras), and also NE(K) is dually isomorphic to the lattice of varieties of modal algebras. Many important properties of logics, for instance, Craig's interpolation property (CIP), the disjunction property (DP), the Beth property (BP), Hallden-completeness...