Saturday, November 29, 2014

 

 



Soy un nuevo usuario

Olvidé mi contraseña

Entrada usuarios

Lógica Matemáticas Astronomía y Astrofísica Física Química Ciencias de la Vida
Ciencias de la Tierra y Espacio Ciencias Agrarias Ciencias Médicas Ciencias Tecnológicas Antropología Demografía
Ciencias Económicas Geografía Historia Ciencias Jurídicas y Derecho Lingüística Pedagogía
Ciencia Política Psicología Artes y Letras Sociología Ética Filosofía
 

rss_1.0 Clasificación por Disciplina

Nomenclatura Unesco > (11) Lógica

Mostrando recursos 110,721 - 110,740 de 132,486

110721. The Journal of Functional and Logic Programming - Ch. Brzoska,J. Darlington,Y. Guo,M. Hagiya,M. Hanus,T. Ida,J. Jaffar,B. Jayaraman
We address the type and effect inference in higher-order concurrent functional programming languages `a la Concurrent ML. We present three extensions of the type and effect discipline. First, the discipline is extended to deal with infinite but recursive effects. Second, the inferred effects are structured, i.e., we keep track of the structure of effects (sequencing, choice, parallel composition, and recursion) instead of using an AC1I (associative, commutative, unitary, and idempotent) effect cumulation operator. Third, for the sake of flexibility, a subtyping relation is considered on the type and effect algebras. This is much more powerful than the classical subeffecting technique. This is meant to avoid type mismatches that may arise...

110722. Fat Estimation in Beef Ultrasound Images Using Texture and Adaptive Logic Networks - James Darrell Mccauley,Brian R. Thane,A. Dale Whittaker
Overviews of Adaptive Logic Networks and co-- occurrence image texture are presented. These tools are used for both prediction and classification of intramuscular fat in beef from ultrasonic images of both live beef animals and slaughtered carcasses. Results showed that Adaptive Logic Networks perform better than any fat prediction method for beef ultrasound images to date and are a viable alternative to statistical techniques. Keywords. Meat, Grading, Automation, Ultrasonic, Images. Instrument Grading of Beef In the United States, beef carcasses are subjectively evaluated by skilled human graders. One of the primary factors in determining beef grades, and thus market value, is the amount of intramuscular fat, or marbling. The method used by human graders to...

110723. Transformations of CLP Modules - Sandro Etalle,Maurizio Gabbrielli
We propose a transformation system for Constraint Logic Programming (CLP) programs and modules. The framework is inspired by the one of Tamaki and Sato for pure logic programs [37]. However, the use of CLP allows us to introduce some new operations such as splitting and constraint replacement. We provide two sets of applicability conditions. The first one guarantees that the original and the transformed programs have the same computational behaviour, in terms of answer constraints. The second set contains more restrictive conditions that ensure compositionality: we prove that under these conditions the original and the transformed modules have the same answer constraints also when they are composed...

110724. Verification of Logic Programs and Imperative Programs - Lee Naish
This paper explores the relationship between verification of logic programs and imperative programs with the aim of uncovering the kinds of reasoning used to construct logic programs. We discuss forward reasoning, such as that used for verifying imperative programs using the inductive assertion method, and backward reasoning, such as that used for verifying imperative programs using subgoal induction and logic programs using consequence verification. We argue that consequence verification is often inadequate for Prolog programs because programmers make implicit assumptions about how procedures are called. These assumptions can be made explicit using general type declarations. Verification of logic programs with type declarations can be done in two steps. We show...

110725. Specification and Verification of Communicating Systems with Value Passing - Dilian Borissov Gurov,C Dilian Borissov Gurov
The present Thesis addresses the problem of specification and verification of communicating systems with value passing. We assume that such systems are described in the well-known Calculus of Communicating Systems, or rather, in its value passing version. As a specification language we propose an extension of the Modal ¯-Calculus, a poly-modal first-order logic with recursion. For this logic we develop a proof system for verifying judgements of the form b ` E : Phi where E is a sequential CCS term and b is a Boolean assumption about the value variables occurring free in E and Phi. Proofs conducted in this proof system follow the structure of...

110726. Meta-Theory of Sequent-Style Calculi in Coq - A. A. Adams
We describe a formalisation of proof theory about sequent-style calculi, based on informal work in [DP96]. The formalisation uses de Bruijn nameless dummy variables (also called de Bruijn indices) [dB72], and is performed within the proof assistant Coq [BB + 96]. We also present a description of some of the other possible approaches to formal meta-theory, particularly an abstract named syntax and higher order abstract syntax. 1 Introduction Formal proof has developed into a significant area of mathematics and logic. Until recently, however, such proofs have concentrated on proofs within logical systems, and meta-theoretic work has continued to be done informally. Recent developments in proof assistants and automated theorem provers have opened...

110727. A Strong Correspondence between Description Logics and Open Logic Programming - Kristof Van Belleghem,Marc Denecker,Danny De Schreye
This paper formally investigates the relationship between Open Logic Programming (OLP) and Description Logics (DL). A description logic is designed to represent two different forms of knowledge. A T-Box represents definitional knowledge, i.e. definitions for a set of concepts. An A-Box represents assertional knowledge about specific domain objects. OLP is a declarative, terminological interpretation of the formalism of Abductive Logic Programming. In this interpretation, an abductive logic program is considered to consist of a T-Box providing definitions for non-abducible predicates and an A-Box providing assertional knowledge in the form of first order logic axioms. We define a provably correct mapping of DL theories to open logic programs, and identify sublanguages...

110728. DEE: a Tool for Genetic Tuning of Software Components on a Distributed Network of Workstations - Ernesto Damiani,Gianni Degli Antoni,Andrea G. B. Tettamanzi
: This paper presents DEE, the Distributed Evolutionary Engine, a complete framework for the off-line tuning of fuzzy-logic based software components using parallel adaptation algorithms. The system was implemented on a high-speed network of workstations by means of a general-purpose task distribution tool. After the description of DEE's architecture, the tuning of fuzzy software components is discussed as an alternative to maintenance, and some encouraging experimental results are described. 1. Introduction The idea of using evolutionary algorithms to tune parameters of fuzzy software components is relatively recent. The first attempts in this direction were aimed to the synthesis and optimization of fuzzy controllers (Karr 1991, Thrift 1991). Besides control, another area of...

110729. Learning from Paradox
The danger of paradoxes teaches us to check for consistency in (natural language) semantics. Paradoxes typically involve an element of self-reference (the set-theoretic paradoxes) or an element of self-reference combined with reference to truth (the semantic paradoxes). Self-reference need not be vicious and talking about truth need not be glib, but linguists who allow self-reference or a truth predicate in their representation languages should be aware of the dangers involved. 1 Russell's Paradox The logical and semantical paradoxes that were discovered at the beginning of this century arose in a context where formal languages were employed in a very loose sense. If Gottlob Frege is hailed in...

110730. Logic Programming and Reasoning with Incomplete Information - Michael Gelfond
The purpose of this paper is to expand the syntax and semantics of logic programs and disjunctive databases to allow for the correct representation of incomplete information in the presence of multiple extensions. The language of logic programs with classical negation, epistemic disjunction, and negation by failure is further expanded by new modal operators K and M (where for the set of rules T and formula F , KF stands for "F is known to be true by a reasoner with a set of premises T " and MF means " F may be believed to be true" by the same reasoner). Sets of rules in the extended...

110731. First-class Polymorphism with Type Inference - Mark P. Jones
Languages like ML and Haskell encourage the view of values as first-class entities that can be passed as arguments or results of functions, or stored as components of data structures. The same languages offer parametric polymorphism, which allows the use of values that behave uniformly over a range of different types. But the combination of these features is not supported--- polymorphic values are not first-class. This restriction is sometimes attributed to the dependence of such languages on type inference, in contrast to more expressive, explicitly typed languages, like System F, that do support first-class polymorphism. This paper uses relationships between types and logic to develop a type system, FCP, that supports first-class polymorphism, type...

110732. A Linear Programming Approach for the Estimation of an Upper Bound on the Maximum Power of CMOS Circuits - Etienne Jacobs,Michel Berkelaar
Maximum instantaneous power in VLSI circuits is of great importance to the design of power and ground lines in a VLSI circuit. Underestimating the maximum instantaneous power greatly reduces the circuits reliability. An accurate estimate of the maximum instantaneous power is therefore needed. Unfortunately, finding the input vectors which give the maximum power consumption is a combinational problem. An exhaustive search is very CPU-time intensive even for small circuits with few primary inputs. We therefore propose a novel linear programming approach, using variables denoting switching scenarios, instead of logic levels between possible switching events, to estimate an upper bound on the maximum power consumption in a CMOS circuit under an input vector change. We present...

110733. The Journal of Functional and Logic Programming
This paper proposes a number of models for integrating finitedomain stochastic constraint solvers into constraint logic programming systems to solve constraint-satisfaction problems e#ciently. Stochastic solvers can solve hard constraint-satisfaction problems very e#- ciently, and constraint logic programming allows heuristics and problem breakdown to be encoded in the same language as the constraints; hence their combination is attractive. Unfortunately, there is a mismatch between the kind of information a stochastic solver provides and that which a constraint logic programming system requires. We study the semantic properties of the various models of constraint logic programming systems that make use of stochastic solvers, and give soundness and completeness results for their use. We describe...

110734. The Arguments of Newly Invented Predicates in ILP - Irene Stahl,Irene Weber
The task of predicate invention in Inductive Logic Programming is to extend the hypothesis language with new predicates, in case the vocabulary given initially is insufficient for the learning task. Introducing new predicates involves searching for an appropriate argument structure. In this paper we investigate the problem of choosing arguments for a new predicate. We identify the relevant terms to be considered as arguments, and propose methods to choose among them based on propositional minimisation. 1 Introduction The aim of inductive learning is to hypothesize a general rule from specific examples. The success of this task strongly depends on the appropriate representation for both examples and rules. A rule that...

110735. Dynamic Control of Genetic Algorithms using Fuzzy Logic Techniques - Michael A. Lee,Hideyuki Takagi
This paper proposes using fuzzy logic techniques to dynamically control parameter settings of genetic algorithms (GAs). We describe the Dynamic Parametric GA: a GA that uses a fuzzy knowledge-based system to control GA parameters. We then introduce a technique for automatically designing and tuning the fuzzy knowledge-base system using GAs. Results from initial experiments show a performance improvement over a simple static GA. One Dynamic Parametric GA system designed by our automatic method demonstrated improvement on an application not included in the design phase, which may indicate the general applicability of the Dynamic Parametric GA to a wide range of...

110736. Fuzzy Logic Controllers Generated by Pseudo-Bacterial Genetic Algorithm with Adaptive Operator - Norberto Eiji Nawa,Tomonori Hashiyama,Takeshi Furuhashi,Yoshiki Uchikawa
This paper presents a new genetic operator called adaptive operator to improve local portions of chromosomes. This new operator is implemented into PseudoBacterial Genetic Algorithm (PBGA). The PBGA was proposed by the authors as a new approach combining a genetic algorithm (GA) with a local improvement mechanism inspired by a process in bacterial genetics. The PBGA was applied for the acquisition of fuzzy rules. The aim of the newly introduced adaptive operator is to improve the quality of the generated rules of the fuzzy models, producing blocks of effective rules and more compact models. The new operator adaptively decides the division points of each chromosome for the bacterial mutation and the cutting points...

110737. Goal Oriented Equational Theorem Proving Using Team Work - Jorg Denzinger,Matthias Fuchs
The team work method is a concept for distributing automated theorem provers and so to activate several experts to work on a given problem. We have implemented this for pure equational logic using the unfailing Knuth-Bendix completion procedure as basic prover. In this paper we present three classes of experts working in a goal oriented fashion. In general, goal oriented experts perform their job "unfair" and so are often unable to solve a given problem alone. However, as a team member in the team work method they perform highly efficient, even in comparison with such respected provers as Otter 3.0 or REVEAL, as we demonstrate by examples, some...

110738. On Specification Frameworks and Deductive Synthesis of Logic Programs - Kung-kiu Lau
this paper, we take a closer look at such frameworks. We shall explain what they are, and how they can be used to specify properties such as correctness and modularity (and hence reusability). Moreover, we shall show that there is a close two-way relationship between specification frameworks and deductive synthesis. In particular, a deductive synthesis process can provide a useful feedback mechanism which can not only check for desirable properties in the specification framework, but also improve the framework (with regard to such properties) using the result of the synthesis. In our approach to modularity, we borrow many of the basic ideas developed in the algebraic approach (e.g. [6, 7,...

110739. The BEAM: A first EAM Implementation - V'itor Santos Costa,Ricardo Lopes
Logic programming provides a high-level view of programming, giving implementors a vast latitude in what techniques to research towards obtaining the best performance for logic programs. One of the holy grails of logic programming has been to design computational models that could be executed efficiently and would allow for both a reduction of the search space and for exploiting all the available parallelism in the application. These goals have motivated the design of the Extended Andorra Model. We report on the design of a first implementation for the Extended Andorra Model with Implicit Control, the BEAM. 1 Introduction Logic programming provides a high-level view of programming where programs...

110740. Database Dependency Discovery: A Machine Learning Approach - Peter A. Flach,Iztok Savnik
this paper are designed such that they can easily be generalised to other kinds of dependencies. Like in current approaches to computational induction such as inductive logic programming, we distinguish between topdown algorithms and bottom-up algorithms. In a top-down approach, hypotheses are generated in a systematic way and then tested against the given relation. In a bottom-up approach, the relation is inspected in order to see what dependencies it may satisfy or violate. We give algorithms for both approaches. Keywords: Induction, attribute dependency, database reverse engineering, data mining. 1. Introduction

 

Busque un recurso