the proceedings contain 23 papers. the topics discussed include: on the complexity of counting the Hilbert basis of a linear diophantine system;solving combinatorial problems with regular local search algorithms;evide...
ISBN:
(纸本)3540664920
the proceedings contain 23 papers. the topics discussed include: on the complexity of counting the Hilbert basis of a linear diophantine system;solving combinatorial problems with regular local search algorithms;evidence algorithm and sequent logical inference search;first order linear temporal logic over finite time structures;transforming conditional rewrite systems with extra variables into unconditional systems;cancellative superposition decides the theory of divisible torsion-free Abelian groups;regular sets of descendants for constructor-based rewrite systems;practical reasoning for expressive description logics;abstracting properties in concurrent constraint programming;a fixpoint semantics for reasoning about finite failure;extensions to the estimation calculus;Beth definability for the guarded fragment;and simplification of horn clauses that are clausal forms of guarded formulas.
TLA (the Temporal logic of Actions) is a linear temporal logic for specifying and reasoning about reactive systems. We define a subset of TLA whose formulas are amenable to validation by animation, withthe intent to ...
详细信息
ISBN:
(纸本)3540664920
TLA (the Temporal logic of Actions) is a linear temporal logic for specifying and reasoning about reactive systems. We define a subset of TLA whose formulas are amenable to validation by animation, withthe intent to facilitate the communication between domain and solution experts in the design of reactive systems.
this paper continues the line of research on representing actions, on the automation of commonsense reasoning and on planning that deals with causal theories and with action language C. We show here that many of the i...
详细信息
ISBN:
(纸本)3540667490
this paper continues the line of research on representing actions, on the automation of commonsense reasoning and on planning that deals with causal theories and with action language C. We show here that many of the ideas developed in that work can be formulated in terms of logic programs under the answer set semantics, without mentioning causal theories. the translations from C into logicprogrammingthat we investigate serve as a basis for the use of systems for computing answer sets to reason about action domains described in C and to generate plans in such domains.
Our aim is to define a new fixpoint semantics which correctly models finite failure. In order to achieve this goal a new fixpoint operator is derived from a "suitable" concrete semaoitics by defining a Galoi...
详细信息
ISBN:
(纸本)3540664920
Our aim is to define a new fixpoint semantics which correctly models finite failure. In order to achieve this goal a new fixpoint operator is derived from a "suitable" concrete semaoitics by defining a Galois insertion modeling finite failure. the corresponding abstract fixpoint semantics correctly models finite failure and is and-compositional.
the purpose of this paper is to establish some connections between precedent-based reasoning as it is studied in the field of Artificial Intelligence and Law, particularly in the work of Ashley, and two other fields: ...
详细信息
ISBN:
(纸本)9781581131659
the purpose of this paper is to establish some connections between precedent-based reasoning as it is studied in the field of Artificial Intelligence and Law, particularly in the work of Ashley, and two other fields: deontic logic and nonmonotonic logic. First, a deontic logic is described that allows for sensible reasoning in the presence of conflicting norms. Second, a simplified version of Ashley's account of precedent-based reasoning is reformulated within the framework of this deontic logic. Finally, some ideas from the theory of nonmonotonic inheritance are employed to show how Ashley's account might be elaborated to allow for a richer representation of the process of argumentation.
We present a denotational semantics for concurrent constraint programming based on derivations containing sequences of interactions of a process withthe environment. Our semantic is then used as collecting semantics ...
详细信息
ISBN:
(纸本)3540664920
We present a denotational semantics for concurrent constraint programming based on derivations containing sequences of interactions of a process withthe environment. Our semantic is then used as collecting semantics for abstracting properties of computations by applying techniques of abstract interpretation.
Data standardization is the commercially important process of extracting useful information from poorly structured textual data. this process includes correcting misspellings and truncations, extraction of data via pa...
详细信息
ISBN:
(纸本)3540667490
Data standardization is the commercially important process of extracting useful information from poorly structured textual data. this process includes correcting misspellings and truncations, extraction of data via parsing, and correcting inconsistencies in extracted data. Prolog programming offers natural advantages for standardizing: definite clause grammars can be used to parse data;Prolog rules can be used to correct inconsistencies;and Prolog's simple syntax allows rules to be generated to correct misspellings and truncations of keywords. these advantages can be seen as rudimentary mechanisms for knowledge representation and at least one commercial standardizer has exploited these advantages. However advances in implementation and in knowledge representation - in particular the addition of preferences to logical formalisms - allow even more powerful and declarative standardizers to be constructed. In this paper a simple preference logic, that of [7] is considered. A fixed point semantics is defined for this logic and its tabled implementation within XSB is described. Development of a commercial standardizer using the preference logic of [7] is then documented. Finally, detailed comparisons are made between the preference logic standardizer and the previous Prolog standardizer illustrating how an advance in knowledge representation can lead to improved commercial software.
the first part of this paper presents a logico-algebraic reconstruction of conceptual graph fundamentals using an appropriately extended binary relation algebra. the algebraisation comprises axioms which in a straight...
详细信息
We propose a framework for a collaborative legal information retrieval system based on dynamic logicprogramming. In order to be collaborative our system keeps the context of the interaction and tries to infer the use...
详细信息
We propose a framework for a collaborative legal information retrieval system based on dynamic logicprogramming. In order to be collaborative our system keeps the context of the interaction and tries to infer the user intentions. Each event is represented by logicprogramming facts which are used to dynamically update the previous user model. User intentions are inferred from this new model and are the basis of the interaction between the system and the legal texts knowledge base. As legal texts knowledge base we are using the documents from the Portuguese Attorney General (Procuradoria Geral da Republica). In this paper we will show some examples of the obtained collaborative behaviour.
the theory of programming languages is one of the core areas of computer sci- ence offering a wealth of models and methods. Yet the complexity of most real programming languages means that a complete formalization of ...
ISBN:
(纸本)3540662227
the theory of programming languages is one of the core areas of computer sci- ence offering a wealth of models and methods. Yet the complexity of most real programming languages means that a complete formalization of their semantics is only of limited use unless it is supported by mechanical means for reasoning about the formalization. this line of research started in earnest withthe seminal paper by Gordon [1] who dened the semantics of a simple while-language in the HOL system and derived Hoare logic from the semantics. Since then, an ever growing number of more and more sophisticated programming languages have been embedded in theorem provers. this talk surveys some of the important developments in this area before concentrating on a specic instance, Bali. Bali (http://***/Bali/) is an embedding of a subset of Java in Isabelle/HOL. So far, the following aspects have been covered:
暂无评论