Monday, April 21, 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 128,030

110721. Local Specification of Distributed Families of Sequential Objects - Hans-dieter Ehrich
. Fully concurrent models of distributed object systems are specified using linear temporal logic that does not per se cope with concurrency. This is achieved by employing the principle of local sequentiality: we specify from local viewpoints assuming that there is no intraobject concurrency but full inter-object concurrency. Local formulae are labelled by identity terms. For interaction, objects may refer to actions of other objects, e.g., calling them to happen synchronously. A locality predicate allows for making local statements about other objects. The interpretation structures are global webs of local life cycles, glued together at shared communication events. These interpretation structures are embedded in an interpretation frame that is a...

110722. Sorting on a Parallel Pointer Machine with Applications to Set Expression Evaluation - Michael T. Goodrich,S. Rao Kosaraju
We present optimal algorithms for sorting on parallel CREW and EREW versions of the pointer machine model. Intuitively, one can view our methods as being based on a parallel mergesort using linked lists rather than arrays (the usual parallel data structure). We also show how to exploit the "locality" of our approach to solve the set expression evaluation problem, a problem with applications to database querying and logic-programming, in O(log n) time using O(n) processors. Interestingly, this is an asymptotic improvement over what seems possible using previous techniques. Categories and Subject Descriptors: E.1 [Data Structures]: arrays, lists; F.2.2. [Analysis of Algorithms and Problem Complexity]: Nonnumerical Algorithms and Problems---sorting and searching General Terms:...

110723. Multi-Level Logic Optimization by Implication Analysis - Wolfgang Kunz,Prem R. Menon
This paper proposes a new approach to multilevel logic optimization based on ATPG (Automatic Test Pattern Generation). Previous ATPG-based methods for logic minimization suffered from the limitation that they were quite restricted in the set of possible circuit transformations. We show that the ATPG-based method presented here allows (in principle) the transformation of a given combinational network C into an arbitrary, structurally different but functionally equivalent combinational network C'. Furthermore, powerful heuristics are presented in order to decide what network manipulations are promising for minimizing the circuit. By identifying indirect implications between signals in the circuit, transformations can be derived which are "good" candidates for the minimization of the circuit. In particular, it...

110724. Decidability and Finite Model Property of Substructural Logics - Hiroakira Ono
this paper, we will give a short survey of results on decision problems and the finite model property of substructural logics. The paper is far from a complete list of these results, since a lot of results have been obtained already in some restricted classes of substructural logics, like relevant logics, and therefore it is impossible to cover all of them. ( As for surveys of decision problems and the finite model property of relevant logics, see e.g. [1, 2, 7]. Also, see [16] for a survey of decision problems of logics related to linear logic. ) Our aim of the present paper is to try...

110725. Inductive Logic Programming for Natural Language Processing - Raymond J. Mooney
. This paper reviews our recent work on applying inductive logic programming to the construction of natural language processing systems. We have developed a system, Chill, that learns a parser from a training corpus of parsed sentences by inducing heuristics that control an initial overly-general shift-reduce parser. Chill learns syntactic parsers as well as ones that translate English database queries directly into executable logical form. The ATIS corpus of airline information queries was used to test the acquisition of syntactic parsers, and Chill performed competitively with recent statistical methods. English queries to a small database on U.S. geography were used to test the acquisition of a complete natural language interface,...

110726. Built-in Chaining: Introducing Complex Components into Architectural Synthesis - Peter Marwedel,Birger L,Rainer Domer,Lehrstuhl Informatik Xii
: In this paper, we extend the set of library components which are usually considered in architectural synthesis by components with built-in chaining. For such components, the result of some internally computed arithmetic function is made available as an argument to some other function through a local connection. These components can be used to implement chaining in a data-path in a single component. Components with built-in chaining are combinatorial circuits. They correspond to "complex gates" in logic synthesis. If compared to implementations with several components, components with built-in chaining usually provide a denser layout, reduced power consumption, and a shorter delay time. Multiplier/accumulators are the most prominent example...

110727. Logic Programming in the LF Logical Framework - Frank Pfenning
this paper we describe Elf, a meta-language intended for environments dealing with deductive systems represented in LF. While this paper is intended to include a full description of the Elf core language, we only state, but do not prove here the most important theorems regarding the basic building blocks of Elf. These proofs are left to a future paper. A preliminary account of Elf can be found in [26]. The range of applications of Elf includes theorem proving and proof transformation in various logics, definition and execution of structured operational and natural semantics for programming languages, type checking and type inference, etc. The basic idea behind Elf...

110728. Programming with Logical Queries, Bulk Updates and Hypothetical Reasoning - Weidong Chen
This paper presents a language of update programs that integrates logical queries, bulk updates and hypothetical reasoning in a seamless manner. There is no syntactic or semantic distinction between queries and updates. Update programs extend logic programs with negation in both syntax and semantics. Users can specify bulk updates in which an arbitrary update is applied simultaneously for all answers of an arbitrary query. Hypothetical reasoning is naturally supported by testing the success or failure of an update. We describe an alternating fixpoint semantics of update programs and show that it can express all nondeterministic database transformations. Current techniques of logical query evaluation can be generalized for...

110729. Fuzzy Based Rate Control for Real-Time MPEG Video - Danny H. K. Tsang,Brahim Bensaou
In this paper, we propose a fuzzy logic based control scheme for real time MPEG video to avoid long delay or excessive loss at the user-network interface (UNI) in an ATM network. The system consists of a shaper whose role is to smooth the MPEG output traffic to reduce the burstiness of the video stream. The input and output rates of the shaper buffer are controlled by two fuzzy logic based controllers. To avoid a long delay at the shaper, the first controller aims to tune the output rate of the shaper based on the number of available transmission credits at the UNI and the occupancy of the shaper's buffer...

110730. Breaking Security Protocols as an AI Planning Problem - Fabio Massacci
. Properties like confidentiality, authentication and integrity are of increasing importance to communication protocols. Hence the development of formal methods for the verification of security protocols. This paper proposes to represent the verification of security properties as a (deductive or model-based) logical AI planning problem. The key intuition is that security attacks can be seen as plans. Rather then achieving "positive" goals a planner must exploit the structure of a security protocol and coordinate the communications steps of the agents and the network (or a potential enemy) to reach a security violation. The planning problem is formalized with a variant of dynamic logic where actions are explicit computation (such as...

110731. Towards the Functional Verification of Large Sequential Circuits - C. A. J. Van Eijk,J. A. G. Jess
Verifying the equivalence of sequential circuits is computationally expensive. Therefore it is interesting to investigate whether a divide-and-conquer strategy can be used to manage the complexity of this problem. This approach requires a verification method which combines an effective decomposition technique with a powerful base verification algorithm. In this paper, we discuss how functional dependencies can be used to find a good decomposition and to improve the performance of the base verification algorithm. 1. Introduction Formal verification methods are clearly gaining acceptance in industry. Especially for combinational equivalence checking, automated tools are being developed which are sufficiently powerful to verify the functional correctness of circuits generated by a logic synthesis tool or manually by a designer....

110732. Entrenchment Relations: A Uniform Approach to Nonmonotonicity - Konstantinos Georgatos
. We show that Gabbay's nonmonotonic consequence relations can be reduced to a new family of relations, called entrenchment relations. Entrenchment relations provide a direct generalization of epistemic entrenchment and expectation ordering introduced by Gardenfors and Makinson for the study of belief revision and expectation inference, respectively. Keywords: Nonmonotonic consequence, epistemic entrenchment, belief revision. 1 Introduction Nonmonotonicity has offered great promise as a logical foundation for knowledge representation formalisms. The reason for such a promise is that nonmonotonic logic completes in a reasonable way our (incomplete) knowledge and withdraws conclusions in the light of new information. Therefore, most approaches to central problems of Artificial Intelligence, such as belief revision, database updating,...

110733. Mathematical Models for Computing Science - C. A. R. Hoare
ion and Quantification 46 6.1 Transistor nets implement logic gates : : : : : : : : : : : : : : 49 6.2 Combinational logic implements natural numbers : : : : : : : 50 6.3 Sequential circuits implement combinational : : : : : : : : : : 50 6.4 From transistors to sequential circuits : : : : : : : : : : : : : 51 6.5 Functions implement relations : : : : : : : : : : : : : : : : : : 53 6.6 Sequential programs implement parallel : : :...

110734. A Natural Deduction Approach to Dynamic Logic - Furio Honsell
. Natural Deduction style presentations of program logics are useful in view of the implementation of such logics in interactive proof development environments, based on type theory, such as LEGO, Coq, etc. In fact, ND-style systems are the kind of systems which can take best advantage of the possibility of reasoning "under assumptions" offered by proof assistants generated by Logical Frameworks. In this paper we introduce and discuss sound and complete proof systems in Natural Deduction style for representing various "truth" consequence relations of Dynamic Logic. We discuss the design decisions which lead to adequate encodings of these logics in Coq. We derive in Dynamic Logic a set of rules...

110735. An Automata-Theoretic Decision Procedure for Propositional Temporal Logic with Since and Until - Y. S. Ramakrishna,L. E. Moser,L. K. Dillon,P. M. Melliar-smith,G. Kutty
We present an automata-theoretic decision procedure for Since/Until Temporal Logic (SUTL), a linear-time propositional temporal logic with strong non-strict since and until operators. The logic, which is intended for specifying and reasoning about computer systems, employs neither next nor previous operators. Such operators obstruct the use of hierarchical abstraction and refinement and make reasoning about concurrency difficult. A proof of the soundness and completeness of the decision procedure is given, and its complexity is analyzed. AMS Subject Classification: 03B25, 03B35, 03B45, 68Q40, 68Q68, 68T15 1 Introduction Since/Until Temporal Logic (SUTL) is a linear-time temporal logic based on propositional calculus and the temporal operators until U and since S. The U...

110736. An Industrial Strength Theorem Prover for a Logic Based on Common Lisp - Matt Kaufmann,J Strother Moore
ACL2 is a re-implemented extended version of Boyer and Moore's Nqthm and Kaufmann's Pc-Nqthm, intended for large scale verification projects. This paper deals primarily with how we scaled up Nqthm's logic to an "industrial strength" programming language --- namely, a large applicative subset of Common Lisp --- while preserving the use of total functions within the logic. This makes it possible to run formal models efficiently while keeping the logic simple. We enumerate many other important features of ACL2 and we briefly summarize two industrial applications: a model of the Motorola CAP digital signal processing chip and the proof of the correctness of the kernel of the floating point division algorithm on...

110737. An Algebraic Characterization of First-Order Definability - A. J. Kfoury,M. Wymann-boni
We give a variable-free relational calculus which defines exactly all first-order definable relations in a arbitrary structure. We then show that, over an arbitrary class C of finite ordered structures with signature f!!!; R 1 ; : : : ; R ff g, the unary relations uniformly defined by this calculus over C are characterized by a another simplified variable-free calculus which we call Q. Q is the least set of formal expressions such that: Q ' f?; R 1 ; : : : ; R ff g [ f(QPhiPhiPhix) j Q 2 Q; x 2 ! [ f1gg [ f(QPsiPsiPsix) j Q 2 Q; x...

110738. Toward the Optimization of a Class of Black Box Optimization Algorithms - Gang Wang,Erik D. Goodman,William F. Punch
Many black box optimization algorithms have sufficient flexibility to allow them to adapt to the varying circumstances they encounter. These capabilities are of two primary sorts: 1) user-determined choices among alternative parameters, operations, and logic structures, and 2) the algorithm-determined alternative paths chosen during the process of seeking a solution to a particular problem. This paper discusses the process of algorithm design and operation, with the intent of integrating the seemingly distinct aspects described above within a unified framework. We relate this algorithmic optimization process to the field of dynamic process control. An approach is proposed toward the optimization of a process for controlling a specific class of systems, and its application to dynamic adjustment...

110739. Pattern Independent Maximum Current Estimation in Power and Ground Buses of CMOS VLSI Circuits: Algorithms, Signal Correlations and Their Resolution - Harish Kriplani,Farid Najm,Ibrahim Hajj
Currents flowing in the power and ground (P&G) buses of CMOS digital circuits affect both circuit reliability and performance by causing excessive voltage drops. Excessive voltage drops manifest themselves as glitches on the P&G buses and cause erroneous logic signals and degradation in switching speeds. Maximum current estimates are needed at every contact point in the buses to study the severity of the voltage drop problems and to redesign the supply lines accordingly. These currents, however, depend on the specific input patterns that are applied to the circuit. Since it is prohibitively expensive to enumerate all possible input patterns, this problem has, for a long time, remained...

110740. Probabilistic Reasoning under Ignorance - Marco Ramoni,Alberto Riva,Vimla L. Patel
The representation of ignorance is a long standing challenge for researchers in probability and decision theory. During the past decade, Artificial Intelligence researchers have developed a class of reasoning systems, called Truth Maintenance Systems, which are able to reason on the basis of incomplete information. In this paper we will describe a new method for dealing with partially specified probabilistic models, by extending a logic-based truth maintenance method from Boolean truth-values to probability intervals. Then we will illustrate how this method can be used to represent Bayesian Belief Networks --- one of the best known formalisms to reason under uncertainty --- thus producing a new class of Bayesian Belief Networks, called Ignorant Belief...

 

Busque un recurso