Loading [MathJax]/extensions/MathZoom.js
In recent work we have proposed a novel approach to define idealized type systems for object-oriented languages, based on abstract compilation of programs into Horn formulas which are interpreted w.r.t. the coinductive (that is, the greatest) Herbrand model. In this paper we investigate how this approach can be applied also in the presence of imperative features. This is made possible by considering a natural translation of Static Single Assignment intermediate form programs into Horn formulas,...
In recent work we have proposed a novel approach to define idealized
type systems for object-oriented languages, based on abstract compilation of
programs into Horn formulas which are interpreted w.r.t. the coinductive (that is, the greatest) Herbrand model. In this paper we investigate how this approach can be applied also in
the presence of imperative features.
This is made possible by considering a natural translation of Static Single Assignment intermediate form programs into Horn formulas,...
In this paper, we define the set of incomparable elements with respect to the triangular order for any t-norm on a bounded lattice. By means of the triangular order, an equivalence relation on the class of t-norms on a bounded lattice is defined and this equivalence is deeply investigated. Finally, we discuss some properties of this equivalence.
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.
Currently displaying 1 –
20 of
35