The ability of providing and relating temporal representations at different 'grain levels' of the same reality is an important research theme in computer science and a major requirement for many applications, ...
详细信息
The ability of providing and relating temporal representations at different 'grain levels' of the same reality is an important research theme in computer science and a major requirement for many applications, including formal specification and verification, temporal databases, data mining, problem solving, and natural language understanding. In particular, the addition of a granularity dimension to a temporal logic makes it possible to specify in a concise way reactive systems whose behaviour can be naturally modeled with respect to a (possibly infinite) set of differently-grained temporal domains. Suitable extensions of the monadic second-order theory of k successors have been proposed in the literature to capture the notion of time granularity. In this paper, we provide the monadic second-order theories of downward unbounded layered structures, which are infinitely refinable structures consisting of a coarsest domain and an infinite number of finer and finer domains, and of upward unbounded layered structures, which consist of a finest domain and an infinite number of coarser and coarser domains, with expressively complete and elementarily decidable temporal logic counterparts. We obtain such a result in two steps. First, we define a new class of combined automata, called temporalized automata, which can be proved to be the automata-theoretic counterpart of temporalized logics, and show that relevant properties, such as closure under Boolean operations, decidability, and expressive equivalence with respect to temporal logics, transfer from component automata to temporalized ones. Then, we exploit the correspondence between temporalized logics and automata to reduce the task of finding the temporal logic counterparts of the given theories of time granularity to the easier one of finding temporalized automata counterparts of them.
We propose a new data structure for implementing delayed computations in Prolog as efficiently as commonly employed solutions, together with the optimal memory management needed for this data structure. It appears tha...
详细信息
The ability of providing and relating temporal representations at different 'grain levels' of the same reality is an important research theme in computer science and a major requirement for many applications, ...
详细信息
The ability of providing and relating temporal representations at different 'grain levels' of the same reality is an important research theme in computer science and a major requirement for many applications, including formal specification and verification, temporal databases, data mining, problem solving, and natural language understanding. In particular, the addition of a granularity dimension to a temporal logic makes it possible to specify in a concise way reactive systems whose behaviour can be naturally modeled with respect to a (possibly infinite) set of differently-grained temporal domains. Suitable extensions of the monadic second-order theory of k successors have been proposed in the literature to capture the notion of time granularity. In this paper, we provide the monadic second-order theories of downward unbounded layered structures, which are infinitely refinable structures consisting of a coarsest domain and an infinite number of finer and finer domains, and of upward unbounded layered structures, which consist of a finest domain and an infinite number of coarser and coarser domains, with expressively complete and elementarily decidable temporal logic counterparts. We obtain such a result in two steps. First, we define a new class of combined automata, called temporalized automata, which can be proved to be the automata-theoretic counterpart of temporalized logics, and show that relevant properties, such as closure under Boolean operations, decidability, and expressive equivalence with respect to temporal logics, transfer from component automata to temporalized ones. Then, we exploit the correspondence between temporalized logics and automata to reduce the task of finding the temporal logic counterparts of the given theories of time granularity to the easier one of finding temporalized automata counterparts of them.
The proceedings contain 38 papers. The special focus in this conference is on Conditional and Typed Rewriting Systems. The topics include: Conditional rewriting in focus;a maximal-literal unit strategy for horn clause...
ISBN:
(纸本)9783540543176
The proceedings contain 38 papers. The special focus in this conference is on Conditional and Typed Rewriting Systems. The topics include: Conditional rewriting in focus;a maximal-literal unit strategy for horn clauses;extended term rewriting systems (invited paper);a proof system for conditional algebraic specifications;conditional rewriting logic;on finite representations of infinite sequences of terms;infinite terms and infinite rewritings;testing confluence of nonterminating rewriting systems;meta-rule synthesis from crossed rewrite systems;completion of first-order clauses with equality by strict superposition (invited paper);knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation;proof by consistency in conditional equational theories;completion procedures as semi-decision procedures (invited paper);linear completion;clausal rewriting;adding algebraic rewriting to the calculus of constructions;on sufficient completeness of conditional specifications;functional plus logicprogramming. an integration of the fp and prolog languages;confluence of the disjoint union of conditional term rewriting systems;implementing term rewriting by graph reduction;compiling concurrent rewriting onto the rewrite rule machine;design strategies for rewrite rules;a simplifier for untyped lambda expressions;parallel graph rewriting on loosely coupled machine architectures;typed equivalence, type assignment and type containment;unique-sort order-sorted theories;compatibility of order-sorted rewrite rules;constrained equational deduction;higher-order unification, polymorphism, and subsorts;an inference system for horn clause logic with equality.
Nonmonotonic reasoning, in its broadest sense, is reasoning to conclusions on the basis of incomplete information. Given more information, we are prepared to retract previously drawn inferences. To exhibit the classic...
详细信息
ISBN:
(纸本)9783540564331
Nonmonotonic reasoning, in its broadest sense, is reasoning to conclusions on the basis of incomplete information. Given more information, we are prepared to retract previously drawn inferences. To exhibit the classic example: if all we know about Tweety is that he is bird, then we plausibly conclude that he can fly;on learning that Tweety is a penguin, we withdraw that conclusion. We call this reasoning nonmonotonic because the set of plausible conclusions does not grow monotonically with increasing information. As Tweety shows, commonsense reasoning has a nonmonotonic component, and it has been argued that almost all commonsense inferences are of this sort. The attempt to formalize nonmonotonic reasoning so that computer programs could use it as part of their reasoning repertoire was begun by John McCarthy in the 1970's, and the early 1980's saw the development of the major nonmonotonic families: circumscription, default logic, and modal nonmonotonic logics. At the same time, proof methods that were clearly nonmonotonic were also being developed: the so-called Truth Maintenance Systems, and negation-as-failure in logicprogramming and deductive databases. From the end of the 1980's to the present there has been an explosion in research in nonmonotonic reasoning. We now understand much better the properties of the major formalisms from a metatheoretic point of view, the relationships among the formalisms, and their connection to independently-developed proof methods. The goal of this monograph is to make this understanding more accessible. For those outside the area, the quantity and technical depth of the material can be a formidable barrier to understanding and applying nonmonotonic methods. For those actively pursuing research, it is often useful to have a concise guide to the major formalisms and their interrelationships. We intend this monograph to serve both purposes. We have tried to present the formalisms as simply and concisely as possible, stressing the c
暂无评论