Monday, July 6, 2015

 

 



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 145,801

110721. A Tableau Calculus for Temporal Description Logics: The Constant Domain Case (Preliminary Version) - Rwth Aachen,Lufg Theoretische Informatik,Carsten Lutz,Holger Sturm,Frank Wolter,Michael Zakharyaschev,Fachbereich Philosophie
We show how to combine the standard tableau system for the basic description logic ALC with Wolper's tableau calculus for propositional temporal logic PTL in order to design a terminating sound and complete tableau-based satisabilitychecking algorithm for the temporal description logic PTLALC of [19] interpreted in models with constant domains. We use the method of quasimodels [16, 14] to represent models with innite domains, and the technique of minimal types [9] to maintain these domains constant. The combination is exible and can be extended to more expressive description logics or even to decidable fragments of rst-order temporal logics. 1 Introduction The problem we deal with in this paper|the problem of...

110722. Logic and p-Recognizable Sets of Integers - Veronique Bruyere,Georges Hansel,Christian Michaux,Roger Villemaire
We survey the properties of sets of integers recognizable by automata when they are written in p-ary expansions. We focus on Cobham's theorem which characterizes the sets recognizable in different bases p and on its generalization to N^m due to Semenov. We detail the remarkable proof recently given by Muchnik for the theorem of Cobham-Semenov, the original proof being published in Russian.

110723. Clause Trees: a Tool for Understanding and Implementing Resolution in Automated Reasoning - J. D. Horton,Bruce Spencer
A new methodology/data structure, the clause tree, is developed for automated reasoning based on resolution in first order logic. A clause tree T on a set S of clauses is a 4-tuple , where N is a set of nodes, divided into clause nodes and atom nodes, E is a set of edges, each of which joins a clause node to an atom node, L is a labeling of N E which assigns to each clause node a clause of S, to each atom node an instance of an atom of some clause of S, and to each edge either + or -. The edge joining...

110724. DisLoP: A Research Project on Disjunctive Logic Programming - Rabose Aravindan,J Urgen Dix,Ilkka Niemel A
This paper gives a brief high-level description of what has been done in the Disjunctive Logic Programming-project (funded by Deutsche Forschungs-Gemeinschaft), undertaken by the University of Koblenz since July 1995. We present the main ideas, cite the relevant papers and point to the implemented systems and how to access them. This paper also serves as a brief survey of the current status of disjunctive logic programming by highlighting important developments and providing enough pointers for further reading.

110725. Group Principals and the Formalization of Anonymity - Paul F. Syverson,Stuart G. Stubblebine
. We introduce the concept of a group principal and present a number of different classes of group principals, including thresholdgroup -principals. These appear to naturally useful concepts for looking at security. We provide an associated epistemic language and logic and use it to reason about anonymity protocols and anonymity services, where protection properties are formulated from the intruder's knowledge of group principals. Using our language, we give an epistemic characterization of anonymity properties. We also present a specification of a simple anonymizing system using our theory. 1 Introduction Though principals are typically viewed as atomic, there is no reason we cannot consider the knowledge and actions taken by a group....

110726. Comprehension Syntax - Peter Buneman,Leonid Libkin,Dan Suciu,Val Tannen,Limsoon Wong
. The syntax of comprehensions is very close to the syntax of a number of practical database query languages and is, we believe, a better starting point than first-order logic for the development of database languages. We give an informal account of a language based on comprehension syntax that deals uniformly with a variety of collection types; it also includes pattern matching, variant types and function definition. We show, again informally, how comprehension syntax is a natural fragment of structural recursion, a much more powerful programming paradigm for collection types. We also show that a very small "abstract syntax language" can serve as a basis for the implementation and optimization of comprehension syntax. 1...

110727. A Logical Representation of a Negotiation Protocol for Autonomous Agents in Multi-Agent Systems - Eduardo Alonso
We propose a logical framework to represent a bilateral incentive negotiation protocol about task distribution over the space of pure deals. We first extend Bell's logic [3] to represent autonomous agents by adding utilities to his many-sorted first-order modal logic, and then introduce a strategic model of negotiation that takes into consideration goal relationships. In so doing we represent not just a communication mechanism but the process through which two agents reason about what agreements to propose, accept or reject. Keywords: autonomous agent, multi-agent systems, negotiation protocol, goal relationships, modal logic. 1 Introduction In Multi-Agent (MA) systems, where researchers must build agents without having the luxury of designing their interaction...

110728. Topic, Focus and Weak Quantifiers - Gerhard Jager
The paper tries to establish dynamic semantics, in particular the Dynamic Modal Predicate Logic of Groenendijk et al. 1996, as a tool for the analysis of information structure phenomena. It is argued that the common distinction between familiar and novel discourse referents/file cards that can be found in DRT, File Change Semantics, or Dynamic Predicate Logic, is not fine--grained enough to cover a certain "quasi-anaphoric" behavior of Weak Quantifiers in one of their readings. Firstly, it is investigated under which syntactic and prosodic circumstances this reading arises. Secondly, the usage of two distinct layers of discourse entities is explained and justified. It turns out that this gives...

110729. A Temporal Logic Based Approach for Querying Lists, Trees, and - Peter Becker
Although lists, trees, and directed acyclic graphs (dags) are of fundamental interest in computer science, they have scarcely been noticed as data types by existing database systems and database models. In this article I present query language concepts for (object-oriented) database systems offering such non-traditional data resp. object types. For the main task of such a query language, namely the specification of predicates on instances of these types, a temporal logic approach is used. For this, an existing timely oriented approach for querying lists is extended by incorporating concepts from the area of branching-time logics. This article mainly presents the logic concepts of the query language and an...

110730. Verification and Optimization of a PLC Control Schedule
We report on the use of the SPIN model checker for both the verification of a process control program and the derivation of optimal control schedules. This work was carried out as part of a case study for the EC VHS project (Verification of Hybrid Systems), in which the program for a Programmable Logic Controller (PLC) of an experimental chemical plant had to be designed and verified. The intention of our approach was to see how much could be achieved here using the standard model checking environment of SPIN/Promela. As the symbolic calculations of real-time model checkers can be quite...

110731. Automated Equational Deduction with Otter - William Mccune,R. Padmanabhan
Algebras, pages 263-- 297. Pergamon Press, Oxford, U.K., 1970. [18] K. Kunen. Single axioms for groups. J. Automated Reasoning, 9(3):291--308, 1992. [19] J. McCharen, R. Overbeek, and L. Wos. Complexity and related enhancements for automated theorem-proving programs. Computers and Mathematics with Applications, 2:1--16, 1976. [20] J. McCharen, R. Overbeek, and L. Wos. Problems and experiments for and with automated theorem-proving programs. IEEE Transactions on Computers, C-25(8):773--782, August 1976. [21] W. McCune. Automated discovery of new axiomatizations of the left group and right group calculi. Journal of Automated Reasoning, 9(1):1--24, 1992. [22] W. McCune. Single axioms for groups and Abelian groups with various operations. J. Automated Reasoning, 10(1):1--13, 1993. [23] W. McCune. Single axioms for...

110732. Michael J. Maher - Joxan Jaffar,Michael J. Maher,Peter J. Stuckey,Roland H. C. Yap
The presentation of constraints in a usable form is an essential aspect of Constraint Logic Programming (CLP) systems. It is needed both in the output of constraints, as well as in the production of an internal representation of constraints for meta-level manipulation. Typically, only a small subset ~ x of the variables in constraints is of interest, and so an informal statement of the problem at hand is: given a conjunction c(~x; ~ y) of constraints, express the projection 9~y c(~x; ~ y) of c onto ~ x in the simplest form. In this paper, we consider the constraints of the CLP(R) system and describe the essential features...

110733. A Formal Approach to Practical Software Verification
Interpretation and Partition Refinement for Model Checking. Ph. D. Thesis, Eindhoven University of Technology, 1996. [DDR00] J. Katoen D. Distefano and A. Rensink. On a temporal logic for object-based systems. Proceedings of Formal Methods for Open Object-Based Distributed Systems, 2000. [DH99] M. Dwyer and J. Hatcliff. Slicing software for model construction. Proceedings of ACM SIGPLAN Partial Evaluation and Program Manipulation, January 1999. [DP98] M. Dwyer and C. Pasareanu. Filter-based model checking of partial systems. Software Engineering Notes, Volume 23, pp. 189 -- 202, November 1998. [DPD00] J. Skakkebaek D. Park, U. Stern and D. Dill. Java model checking. Proceedings of the First International Workshop on Automated Program Analysis, Testing and Verification,...

110734. Quantitative Constraint Logic Programming for Weighted Grammar Applications - Stefan Riezler
Constraint logic grammars provide a powerful formalism for expressing complex logical descriptions of natural language phenomena in exact terms. Describing some of these phenomena may, however, require some form of graded distinctions which are not provided by such grammars. Recent approaches to weighted constraint logic grammars attempt to address this issue by adding numerical calculation schemata to the deduction scheme of the underlying CLP framework. Currently, these extralogical extensions are not related to the modeltheoretic counterpart of the operational semantics of CLP, i.e., they do not come with a formal semantics at all. The aim of this paper is to...

110735. Proving Termination of GHC Programs - M. R. K. Krishna Rao,D. Kapur,R. K. Shyamasundar
A transformational approach for proving termination of parallel logic programs such as GHC programs is proposed. A transformation from GHC programs to term rewriting systems is developed; it exploits the fact that unications in GHC-resolution correspond to matchings. The termination of a GHC program for a class of queries is implied by the termination of the resulting rewrite system. This approach facilitates the applicability of a wide range of termination techniques developed for rewrite systems in proving termination of GHC programs. The method consists of three steps: (a) deriving moding information from a given GHC program, (b) transforming the GHC program into a term rewriting system using...

110736. Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling - Annalisa Bossi,Sandro Etalle,Sabina Rossi,Jan-georg Smaus
In logic programming, dynamic scheduling refers to a situation where the selection of the atom in each resolution (computation) step is determined at runtime, as opposed to a fixed selection rule such as the left-to-right one of Prolog. This has applications e.g. in parallel programming. A mechanism to control dynamic scheduling is provided in existing languages in the form of delay declarations. Input-consuming derivations were introduced to describe dynamic scheduling while abstracting from the technical details. In this paper, we first formalise the relationship between delay declarations and inputconsuming derivations, showing in many cases a one-to-one correspondence. Then, we define...

110737. Relational Interpretation and Geometrical Form - Glyn Morrill,Jordi Girona Salgado
We describe the possibility of a systematic correspondence between combined algebraic and relational interpretation of categorial logic, and the form of proof structures and paths in proof nets, illustrating with reference to medial extraction, in situ binding and discontinuity. Type logic for linguistic description (e.g. Moortgat 1988, 1997; Morrill 1994; Carpenter 1997) is based on what we may refer to as a Lambek-van Benthem correspondence: (logical) formulas as (linguistic) categories. Lexical signs are classified by category formulas, and the language model projected by a lexicon is determined by the consequence relation induced on category formulas by their interpretation. In this logical model of language, (logical) proofs correspond to (linguistic) derivations, but...

110738. GraphLog: a Visual Formalism for Real Life Recursion - Mariano P. Consens,Alberto O. Mendelzon
We present a query language called GraphLog, based on a graph representation of both data and queries. Queries are graph patterns. Edges in queries represent edges or paths in the database. Regular expressions are used to qualify these paths. We characterize the expressive power of the language and show that it is equivalent to stratified linear Datalog, first order logic with transitive closure, and non-deterministic logarithmic space (assuming ordering on the domain). The fact that the latter three classes coincide was not previously known. We show how GraphLog can be extended to incorporate aggregates and path summarization, and describe briefly our current prototype implementation. 1 Introduction The literature on...

110739. Cofactoring-Based Upper Bound Computation for Covering Problems - Congguang Yang,Maciej Ciesielski
This paper introduces an efficient technique to compute a tight upper bound for the unate and binate covering problems. It is known that a covering problem can be solved by finding a shortest path on a BDD representing a satisfiability formula. Our technique is based on finding an approximation to the shortest path by identifying a path on a BDD composed of as many negative edges as possible. This operation is performed by iterative cofactoring without actually building a BDD. The results show that our technique generates very tight upper bound, with more than half of the test cases resulting in the optimum solution in just...

110740. A Computational Model of Belief - Aaron N. Kaplan,Lenhart K. Schubert
We propose a logic of belief in which the expansion of beliefs beyond what has been explicitly learned is modeled as a finite computational process. The logic does not impose a particular computational mechanism; rather, the mechanism is a parameter of the logic, and we show that as long as the mechanism meets a particular set of constraints, the resulting logic has certain desirable properties. Chief among these is the property that one can reason soundly about another agent's beliefs by simulating its computational mechanism with one's own. We also give a detailed comparison of our model with Konolige's deduction model, another model of belief in...

 

Busque un recurso