Saturday, October 25, 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 131,932

110721. Is The Success Of Fuzzy Logic Really Paradoxical? Or: Towards The Actual Logic Behind Expert Systems - Olga M. Kosheleva,Vladik Kreinovich
. The formal concept of logical equivalence in fuzzy logic 8;25 , while theoretically sound, seems impractical. The misinterpretation of this concept has led to some pessimistic conclusions 4 . Motivated by practical interpretation of truth values for fuzzy propositions, we take the class (lattice) of all sub-intervals of the unit interval [0,1] as the truth value space for fuzzy logic, subsuming the traditional class of numerical truth values from [0,1]. The associated concept of logical equivalence is stronger than the traditional one. Technically, we are dealing with much smaller set of pairs of equivalent formulas, so that we are able to check equivalence algorithmically. The checking is done by showing that...

110722. A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses - Jos'e Miguel Rivero,Robert Nieuwenhuis,Miguel Angel Vallejo
. We present Dedam (Deduction Abstact Machine), a standard architecture around which high-performance theorem provers for clausal logic with equality can be built. It includes a WAM-like heap structure for storing terms as DAG's, several indexing data structures, and mechanisms for efficient memory management and demodulation. These data structures turn out to be surprisingly well combinable due to conceptual similarities. We provide statistics showing how we reduce two well-known bottlenecks in equational deduction. The first one, matching for demodulation is done by a new indexing method, substitution trees with equality constraints. Regarding the other bottle neck, memory management, WAM-based techniques allow us to completely avoid it during unification, matching, and demodulation. Static...

110723. Sequentiality, Monadic Second-Order Logic and Tree Automata - Hubert Comon
Given a term rewriting system R and a normalizable term t, a redex is needed if in any reduction sequence of t to a normal form, this redex will be contracted. Roughly, R is sequential if there is an optimal reduction strategy in which only needed redexes are contracted. More generally, G. Huet and J.-J. L'evy define in [9] the sequentiality of a predicate P on partially evaluated terms. We show here that the sequentiality of P is definable in SkS, the monadic second-order logic with k successors, provided P is definable in SkS. We derive several known an new consequences of this remark: 1--strong sequentiality, as defined in...

110724. Metamorphosis: State Assignment by Retiming and Re-encoding - Balakrishnan Iyer,Maciej Ciesielski
This paper presents Metamorphosis 1 -- a novel technique for optimal state assignment targeting multi-level logic implementations. We present a new formulation and synthesis techniques for the state assignment problem based on controlled retiming and re-encoding of a symbolically represented finite state machine (FSM) represented initially with a one-hot code. Metamorphosis is a new design paradigm that integrates the structural and behavioral design methodologies in a synergistic fashion and leverages the additional degrees of freedom to the synthesis of optimal FSM. The proposed technique differs drastically from previous approaches in that the encoding process is guided directly by the cost function (optimization criterion) rather than speculative estimates of the encoding...

110725. CLAM Specification for Provably Correct Compilation of - Egon B Orger,Rosario F. Salamone
The paper extends the correctness proof in [4] for compilation of Prolog programs on the WAM to CLP(R) programs on the Constraint Logic Arithmetic Machine (CLAM [8, 10]). This serves to illustrate, through a complex case study, how the evolving algebra specification methodology allows to incorporate modularity and extendability principles in system design. 1 1 Introduction This paper extends, to the Constraint Logic Arithmetic Machine (CLAM) and CLP(R) programs, the mathematical analysis of the Warren Abstract Machine (WAM) for executing Prolog and the resulting correctness proof for a general compilation scheme of Prolog to the WAM given in [4]. Starting from an abstract CLP(R) model---which paraphrases the primary model for Prolog defined in...

110726. Reasoning about Effects of Concurrent Actions - Chitta Baral,Gelfond Gelfond
this paper we extend the language A and its translation to allow reasoning about the effects of concurrent actions. The logic programming formalization of situation calculus with concurrent actions presented in the paper is of independent interest and may serve as a test bed for the investigation of various transformations and logic programming inference mechanisms. ! 1. INTRODUCTION

110727. Verifying Reachability in LOTOS Specifications by Temporal Logic - W. M. Mak,T. Y. Cheung,C. Lee
A method for verifying reachability properties of distributed system designs specified in the formal description technique LOTOS is proposed. It consists of a linear temporal propositional logic language and a compositional temporal semantics with linear temporal operators. Based on this semantics, both the design specified in LOTOS and its properties can be expressed as logical formulas. Proving the presence of a property in the design is then equivalent to logically deducing the formula representing the designated property from the formula representing the given LOTOS specification. This paper emphasizes on the application of the method to proving that the intended operations of a design are reachable. That is, they...

110728. Supporting Data Integration and Warehousing Using H2O - Richard Hull,Roger King,Jean-claude Franchitti
This paper presents a broad framework for data integration, that supports both data materialization and virtual view capabilities, and that can be used with legacy as well as modern database systems. The framework is based on "integration mediators", these are software components that use techniques generalized from active databases, such as triggering and rulebases. This permits the logic, especially for incremental maintenance of materialized data, of an integration mediator to be specified in a relatively declarative and modular fashion. One specific focus of this paper is the development of a taxonomy of the solution space for supporting and maintaining integrated views. A second focus concerns providing support for...

110729. Representing Autoepistemic Introspection in Terms of Default Rules - Tomi Janhunen
This paper addresses the relationship of Reiter's default logic, Moore's autoepistemic logic as well as Marek and Truszczynski's strong autoepistemic logic from a new point of view. Earlier research results on their interconnection support the view that default reasoning is a special case of autoepistemic reasoning. To the contrary, this paper shows how autoepistemic theories can be faithfully translated into default theories. Consequently, autoepistemic reasoning can be seen a form of default reasoning. This indicates together with the previous research results that autoepistemic logic and default logic are of equal generality. As a practical application of the presented translation, it...

110730. Restricting the hypothesis space, guiding the search, and handling the redundant information in Inductive Logic Programming - Uros Pompe
We developed and implemented an inductive logic programming system and the first order classifier, called ILP-R. It is capable of efficiently inducing theories in a restricted subset of function free normal programs. It is able to use the hypothesis to classify new instances, by using the naive Bayesian reasoning. The contributions of the system are threefold. First, we devised a weak syntactic declarative bias restricting the set of possible hypotheses. We discuss and prove its properties. The latter are then exploited to encode the current proof of a partially induced clause in such a way, that the encoding grows at most linearly with respect to the clause...

110731. F1.094e+06>The Journal of Functional and Logic Programming The MIT Press Volume 1998, Article 6
In this paper, we present an extension of the Ja#ar-Lassez constraint logic programming scheme that operates with unions of constraint theories with di#erent signatures and decides the satisfiability of mixed constraints by appropriately combining the constraint solvers of the component theories. We describe the extended scheme, and provide logical and operational semantics for it along the lines of those given for the original scheme. We then show how the main soundness and completeness results of constraint logic programming lift to our extension. 1 Introduction The constraint logic programming (CLP) scheme was originally developed by Ja#ar and Lassez [JL86] as a principled way to combine the computational paradigms of logic programming and...

110732. Developing Secure Applications: A Systematic Approach - C. Eckert,D. Marek
This paper presents parts of the SECREDS project which aims to bridge the gap between system modeling and implementation using a high-level programming language. Within SECREDS secure applications are developed top down starting with a top-level specification. Top-level specifications are given by our computational model and application-specific security policies are specified using our security requirement logic. To implement a top-level specification we developed a high-level programming language called INSEL + offering language concepts well adapted to our underlying model. We will present main features of INSEL + focusing on access control aspects and we will outline some guidelines to support the systematic implementation of a given top-level specification preserving specified security properties. Keywords Access Control, Security...

110733. TAO - A Model for the Integration of Concurrency and Synchronisation in Object-Oriented Programming - S. E. Mitchell
The integration of concurrency into inheritance has been attempted in a number of languages. However, some of the compromises made have seriously degraded the usefulness of these languages. Hence none of these languages have been totally successful. A particular problem has been the "inheritance anomaly" caused by interactions between synchronisation mechanisms and inheritance. This thesis introduces a new model, called TAO, for this integration. The model allows for (multiple) threads to be embedded in an object and provides details of how these threads are handled in inheritance. We also develop a new concurrency control mechanism, based on a combination of...

110734. Specialised Recombinative Operators for Timetabling Problems - Edmund Burke,David Elliman,Rupert Weare
. This paper discusses a series of recombination operators for the timetabling problem. These operators act upon a direct representation of the timetable and maintain the property of feasibility. That is that there are no conflicts and no overfilled rooms. Various approaches to solving the timetabling problem using evolutionary computing methods are first compared. The recombination operators are then presented and various alternatives for incorporating heuristic knowledge in the search are described. Finally, results are presented comparing the operators on a real timetabling problem. 1 Introduction Recently, there has been a lot of attention paid to the problem of automating...

110735. Oracles for Checking Temporal Properties of Concurrent Systems - Laura K. Dillon,Qing Yu
Verifying that test executions are correct is a crucial step in the testing process. Unfortunately, it can be a very arduous and error-prone step, especially when testing a concurrent system. System developers can therefore benefit from oracles automating the verification of test executions. This paper examines the use of Graphical Interval Logic (GIL) for specifying temporal properties of concurrent systems and describes a method for constructing oracles from GIL specifications. The visually intuitive representation of GIL specifications makes them easier to develop and to understand than specifications written in more traditional temporal logics. Additionally, when a test execution violates a GIL specification, the associated oracle provides information about a fault. This information can be displayed visually,...

110736. Specifying Filler-Gap Dependency Parsers in a Linear-Logic Programming Language - Joshua S. Hodas
An aspect of the Generalized Phrase Structure Grammar formalism proposed by Gazdar, et al. is the introduction of the notion of "slashed categories " to handle the parsing of structures, such as relative clauses, which involve unbounded dependencies. This has been implemented in Definite Clause Grammars through the technique of gap threading, in which a difference list of extracted noun phrases (gaps) is maintained. However, this technique is cumbersome, and can result in subtle soundness problems in the implemented grammars. Miller and Pareschi have proposed a method of implementing gap threading at the logical level in intuitionistic logic. Unfortunately that implementation itself suffered from serious problems, which the authors recognized....

110737. ERTL: An Extension to RTL for Requirements Analysis for Hybrid Systems
this paper we provide extensions to RTL which allow reasoning about absolute timings for both continuous and discrete time, and reasoning about system behaviour in the value and time domains by parametrising predicates in terms of system variables. Incorporating these features into RTL we obtain Extended Real-Time Logic (ERTL) which is suitable for the modelling and analysis of hybrid systems. The paper is organized as follows. In the next section we present the concepts of an event-action model, and discuss their formalisation in terms of RTL and ERTL. Section 3 defines the syntax and semantics of ERTL. Section 4 presents two case studies, the first is the...

110738. Phased Logic: Supporting the Synchronous Design Paradigm with Delay--Insensitive Circuitry - Daniel H. Linder,James C. Harden
Phased logic is proposed as a solution to the increasing problem of timing complexity in digital design. It is a delay--insensitive design methodology that seeks to restore the separation between logical and physical design by eliminating the need to distribute low--skew clock signals and carefully balance propagation delays. However, unlike other methodologies that avoid clocks, phased logic supports the cyclic, deterministic behavior of the synchronous design paradigm. This permits the designer to rely chiefly on current experience and CAD tools to create phased logic systems. Marked graph theory is used as a framework for governing the interaction of phased logic gates that operate directly on Level--Encoded two--phase...

110739. Answer Sets in General Nonmonotonic Reasoning (Preliminary Report) - Vladimir Lifschitz,Thomas Y. C. Woo
Languages of declarative logic programming differ from other modal nonmonotonic formalisms by lack of syntactic uniformity. For instance, negation as failure can be used in the body of a rule, but not in the head; in disjunctive programs, disjunction is used in the head of a rule, but not in the body; in extended programs, negation as failure can be used on top of classical negation, but not the other way around. We argue that this lack of uniformity should not be viewed as a distinguishing feature of logic programming in general. As a starting point, we take a translation from the language of disjunctive programs with negation as failure and classical negation into MBNF---the...

110740. Combining Temporal Logic Systems - Marcelo Finger,Dov Gabbay
This paper is a continuation of the work started in [FG92] on combining temporal logics. In this work, four combination methods are described and studied with respect to the transference of logical properties from the component one-dimensional temporal logics to the resulting two-dimensional temporal logic. Three basic logical properties are analysed, namely soundness, completeness and decidability. Each combination method is composed of three submethods that combine the languages, the inference systems and the semantics of two one-dimensional temporal logic systems, generating families of two-dimensional temporal languages with varying expressivity and varying degree of transference of logical properties. The temporalisation method and the independent combination method are shown to transfer...

 

Busque un recurso