We present a theory of proof denotations in classical propositional logic. the abstract definition is in terms of a semiring of weights, and two concrete instances are explored. Withthe Boolean semiring we get a theo...
详细信息
ISBN:
(数字)9783540320142
ISBN:
(纸本)3540255931
We present a theory of proof denotations in classical propositional logic. the abstract definition is in terms of a semiring of weights, and two concrete instances are explored. Withthe Boolean semiring we get a theory of classical proof nets, with a geometric correctness criterion, a sequentialization theorem, and a strongly normalizing cut-elimination procedure. this gives us a "Boolean" category, which is not a poset. Withthe semiring of natural numbers, we obtain a sound semantics for classical logic, in which fewer proofs are identified. though a "real" sequentialization theorem is missing, these proof nets have a grip on complexity issues. In both cases the cut elimination procedure is closely related to its equivalent in the calculus of structures.
Software agents are being produced in many different forms to carry out different tasks, with personal assistants designed to reduce the amount of effort it takes for the user to go about their daily tasks. Most perso...
详细信息
ISBN:
(纸本)9728865198
Software agents are being produced in many different forms to carry out different tasks, with personal assistants designed to reduce the amount of effort it takes for the user to go about their daily tasks. Most personal assistants work with user preferences when working out what actions to perform on behalf of their user. this paper describes a novel approach for modelling user behaviour in the application area of Diary Management withthe use of Inductive logicprogramming.
In this paper we describe the formal semantic frame and introduce the formal language LTN to express the time and the ability and right of an agent on selecting action and negotiation process in a Multi-Agent System, ...
详细信息
ISBN:
(纸本)9728865198
In this paper we describe the formal semantic frame and introduce the formal language LTN to express the time and the ability and right of an agent on selecting action and negotiation process in a Multi-Agent System, the change of the right over time, the free action of an agent and the time need by a agent to complete an action. Based on the above, the independent negotiation system has been further complete. In this paper, it is also addressed that the axiom system is rational, validate and negotiation reasoninglogic is soundness, completeness and consistent.
Mobile Agent system creates a new way for sharing distributed resources and providing multi-located services. Withthe idea of moving calculations towards resources, it occupies less network traffics than the traditio...
详细信息
ISBN:
(纸本)9728865198
Mobile Agent system creates a new way for sharing distributed resources and providing multi-located services. Withthe idea of moving calculations towards resources, it occupies less network traffics than the traditional Client/Server model and achieves more flexibilities than the Remote Procedure Call (RPC) architecture. In order to endow agents withthe ability of accessing remote data resources, in this paper we present the design strategies of the Database Interface between a logicprogramming language based Mobile Agent system and a remote DBMS.
In this paper, we present a current cooperative work involving different institutes around the world. Our aim is to provide an online Inductive logicprogramming tool. this is the first step in a more complete structu...
详细信息
ISBN:
(纸本)9728865198
In this paper, we present a current cooperative work involving different institutes around the world. Our aim is to provide an online Inductive logicprogramming tool. this is the first step in a more complete structure for enabling e-technology for machine learning and bio-informatics. We describe the main architecture of the project and how the data will be formatted for being sent to the ILP machinery. We focus on a biological application (yeast fermentation process) due to its importance for high added value end products.
Prepositional interval temporal logics are quite expressive temporal logics that allow one to naturally express statements that refer to time intervals. Unfortunately, most, such logics turned out to be (highly) undec...
详细信息
the so-called light logics [1,2,3] have been introduced as logical systems enjoying quite remarkable normalization properties. Designing a type assignment system for pure lambda calculus from these logics, however, is...
详细信息
In database systems, business logic is usually implemented in the forms of external processes, stored procedures, user-defined functions, components, objects, constraints, triggers, etc. In this paper, we advocate the...
详细信息
ISBN:
(纸本)9728865198
In database systems, business logic is usually implemented in the forms of external processes, stored procedures, user-defined functions, components, objects, constraints, triggers, etc. In this paper, we advocate the idea of storing business logic - in the form of functions - as data in tables. this idea gives a basis for applying the software-engineering methodology of table-driven programming in SQL. the query evaluation process then needs only to be extended with mechanical evaluation of "joined" data and functions. this approach can make understanding and maintenance of stored business logic transparent as relational data. In short, data and functions are integrated in a relational manner. Using a common enterprise application as an example, we demonstrate this methodology with an existing ORDBMS capable of storing polymorphic objects. We also discuss this approach's shortcomings and alternatives.
Refinement is a key concept in the B-Method. While refinement is at the heart of the B Method, so far no automatic refinement checker has been developed for it. In this paper we present a refinement checking algorithm...
详细信息
ISBN:
(纸本)3540297979
Refinement is a key concept in the B-Method. While refinement is at the heart of the B Method, so far no automatic refinement checker has been developed for it. In this paper we present a refinement checking algorithm and implementation for B. It is based on using an operational semantics of 13, obtained in practice by the PR,013 animator. the refinement checker has been integrated into PROB toolset and we present various case studies and empirical results in the paper, showing the algorithm to be Surprisingly effective. the algorithm checks that a refinement preserves the trace properties of a specification. We also compare our tool against the refinement checker FDR for CSP and discuss an extension for singleton failure refinement.
In the framework of intelligent information systems design, we present an intelligent data integration and user profile modelling. Our approach uses jointly Topic Maps and Description logics. Topic Maps are used to re...
详细信息
ISBN:
(纸本)9728865198
In the framework of intelligent information systems design, we present an intelligent data integration and user profile modelling. Our approach uses jointly Topic Maps and Description logics. Topic Maps are used to represent semantic of distributed data. Using the formalized semantic, the distributed data is merged into one repository. then, Description logics are used over this repository to compute implicit semantic relations using logicreasoning such as subsumption. We present then a new user profile management which uses qualifying attributes rather than identifying attributes. Description logics are used to formalize profiles in order to maintain consistency of right attribution to profiles.
暂无评论