All a b c d e f g h i j k l m n o p q r s t u v w x y z Other

Page 1 Next

Displaying 1 – 20 of 35

Showing per page

Idealized coinductive type systems for imperative object-oriented programs

Davide Ancona, Giovanni Lagorio (2011)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

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,...

Idealized coinductive type systems for imperative object-oriented programs

Davide Ancona, Giovanni Lagorio (2011)

RAIRO - Theoretical Informatics and Applications

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,...

Incomparability with respect to the triangular order

Emel Aşıcı, Funda Karaçal (2016)

Kybernetika

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.

Indicative propositions.

Purdea, Ioan, Both, Nicolae (2001)

Analele Ştiinţifice ale Universităţii “Ovidius" Constanţa. Seria: Matematică

Induction and decision procedures.

Deepak Kapur, Jürgen Giesl, Mahadevan Subramaniam (2004)

RACSAM

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, modal logic and complexities

Eugénie Foustoucos, Irène Guessarian (2009)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

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, Modal Logic and Complexities

Eugénie Foustoucos, Irène Guessarian (2007)

RAIRO - Theoretical Informatics and Applications

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...

Inference in conditional probability logic

Niki Pfeifer, Gernot D. Kleiter (2006)

Kybernetika

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...

Information boundedness principle in fuzzy inference process

Peter Sarkoci, Michal Šabo (2002)

Kybernetika

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.

Information frames, implication systems and modalities.

Marcello D'Agostino, Dov M. Gabbay, Alessandra Russo (1996)

Mathware and Soft Computing

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.

Integral of Complex-Valued Measurable Function

Keiko Narita, Noboru Endou, Yasunari Shidama (2008)

Formalized Mathematics

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

Integral of Real-Valued Measurable Function 1

Yasunari Shidama, Noboru Endou (2006)

Formalized Mathematics

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

Page 1 Next