141.

The Economics of Supply and Demand: An Important Challenge for Conceptual Graphs
- Simon Polovina; Harry S. Delugach
. Conceptual graphs have been used to model information in many complex domains, but the domain of economics is particularly difficult because its knowledge is based as much on perceptions of people as on physical laws. This paper addresses that problem using as a vehicle one well-known basic economic area: namely, the law of supply and demand. Employing Peirce logic negative contexts, we represent various parts of classical economic theory, e.g., over-supply, over-demand, and equilibrium states. It is shown how tacit knowledge is relevant to the modeling of this information, and why this knowledge requires the conceptual graphs to be...

142.

Linear Logic for Meaning Assembly
- Mary Dalrymple; John Lamping; Fernando Pereira; Vijay Saraswat
This paper provides a brief overview of our ongoing investigation in the use of formal deduction to explicate the relationship between syntactic analyses in Lexical-Functional Grammar (LFG) and semantic interpretations (Dalrymple, Lamping, and Saraswat, 1993; Dalrymple et al., 1993; Dalrymple et al., 1994a; Dalrymple et al., 1994b; Dalrymple et al., 1995; Dalrymple et

143.

Logic Program Specialisation: How To Be More Specific
- Michael Leuschel; Danny De Schreye
Standard partial deduction suffers from several drawbacks when compared to topdown abstract interpretation schemes. Conjunctive partial deduction, an extension of standard partial deduction, remedies one of those, namely the lack of side-ways information passing. But two other problems remain: the lack of success-propagation as well as the lack of inference of global success-information. We illustrate these drawbacks and show how they can be remedied by combining conjunctive partial deduction with an abstract interpretation technique known as more specific program construction. We present a simple, as well as a more refined integration of these methods. Finally we illustrate the practical relevance...

144.

Architecture of Centralized Field-Configurable Memory
- Steven J. E. Wilton; Jonathan Rose; Zvonko G. Vranesic
As the capacities of FPGAs grow, it becomes feasible to implement the memory portions of systems directly on an FPGA together with logic. We believe that such an FPGA must contain specialized architectural support in order to implement memories efficiently. The key feature of such architectural support is that it must be flexible enough to accommodate many different memory shapes (widths and depths) as well as allowing different numbers of independentlyaddressed memory blocks. This paper describes a family of centralized Field-Configurable Memory architectures which consist of a number of memory arrays and dedicated mapping blocks to combine these arrays. We...

145.

Transformation-Based Bottom-Up Computation of the Well-Founded Model
- Stefan Brass; Jürgen Dix; Burkhard Freitag; Ulrich Zukowski
We present a bottom-up algorithm for the computation of the well-founded model of non-disjunctive logic programs. Our method is based on the elementary program transformations studied by Brass and Dix [BD94, BD97, BD98a]. However, their "residual program" can grow to exponential size, whereas for function-free programs our "program reminder" is always polynomial in the size of the extensional database (EDB). As in the SLG-resolution of Chen and Warren [CW93, CW96, CSW95], we do not only delay negative but also positive literals if they depend on delayed negative literals. When disregarding goal-directedness, which needs additional concepts, our approach can be seen...

146.

AgentSpeak(L): BDI Agents speak out in a logical computable language
- Anand S. Rao
Belief-Desire-Intention (BDI) agents have been investigated by many researchers from both a theoretical specification perspective and a practical design perspective. However, there still remains a large gap between theory and practice. The main reason for this has been the complexity of theorem-proving or model-checking in these expressive specification logics. Hence, the implemented BDI systems have tended to use the three major attitudes as data structures, rather than as modal operators. In this paper, we provide an alternative formalization of BDI agents by providing an operational and proof-theoretic semantics of a language AgentSpeak(L). This language can be viewed as an abstraction...

147.

Compiling Intensional Sets in CLP
- Paola Bruscoli; Agostino Dovier; Enrico Pontelli; Gianfranco Rossi
Constructive negation has been proved to be a valid alternative to negation as failure, especially when negation is required to have, in a sense, an `active' role. In this paper we analyze an extension of the original constructive negation in order to gracefully integrate with the management of set-constraints in the context of a Constraint Logic Programming Language dealing with finite sets. We show that the marriage between CLP with sets and constructive negation gives us the possibility of representing a general class of intensionally defined sets without any further extension to the operational semantics of the language. The presence...

148.

Efficient Validity Checking for Processor Verification
- Robert Jones; David L. Dill; Jerry R. Burch
We describe an efficient validity checker for the quantifier-free logic of equality with uninterpreted functions. This logic is well suited for verifying microprocessorcontrol circuitry since it allows the abstraction of datapath values and operations. Our validity checker uses special data structures to speed up case splitting, and powerful heuristics to reduce the number of case splits needed. In addition, we present experimental results and show that this implementation has enabled the automatic verification of an actual high-level microprocessor description. 1 Introduction As microprocessor designs become more complex, the cost of validation becomes a larger fraction of the total design cost....

149.

How to Progress a Database
- Fangzhen Lin; Ray Reiter
One way to think about STRIPS is as a mapping from databases to databases, in the following sense: Suppose we want to know what the world would be like if an action, represented by the STRIPS operator ff, were done in some world, represented by the STRIPS database D 0 . To find out, simply perform the operator ff on D 0 (by applying ff's elementary add and delete revision operators to D 0 ). We describe this process as progressing the database D 0 in response to the action ff. In this paper, we consider the general problem of...

150.

An Inductive Logic Programming Framework to Learn a Concept from Ambiguous Examples
- Dominique Bouthinon; Henry Soldano; Atelier De Bioinformatique (abi
. We address a learning problem with the following peculiarity : we search for characteristic features common to a learning set of objects related to a target concept. In particular we approach the cases where descriptions of objects are ambiguous : they represent several incompatible realities. Ambiguity arises because each description only contains indirect information from which assumptions can be derived about the object. We suppose here that a set of constraints allows the identification of "coherent" sub-descriptions inside each object. We formally study this problem, using an Inductive Logic Programming framework close to characteristic induction from interpretations. In particular,...

151.

Fuzzy Constraint-based Controller Design
- Ching-yu Tyan; Robert Lai; Paul P. Wang; Dennis R. Bahler
This paper introduces a novel fuzzy logic controller design methodology based on the theory of fuzzy constraint network. Despite the successes of rule-based fuzzy logic controller design techniques, this approach represents only a very special case of the expressive power of the first order predicate calculus (FOPC). The notion of "constraint" has an extremely tie to the concept of the mathematical modeling in dynamic systems. This paper fully explains and demonstrates this concept. Furthermore, the inference methodology of "fuzzy local propagation" for reasoning about imprecise information in a network of constraints is also introduced. Finally, a performance comparison of the...

152.

Fixpoint Analysis of Type and Alias in AKL Programs
- Thomas Sjöland; Dan Sahlin
We defined and implemented a method for analysis of the CCP language AKL in the spirit of abstract interpretation that uses a static set of semantic equations which abstracts the concurrent execution of an AKL program. The method strictly separates the setting up of the equation system from the solving of the system with a fixpoint procedure. The computation strategies used, results for a number of test programs and the conclusions we draw from this experimental effort are reported. This report, together with the software implementing the system described herein, is deliverable number D.WP.1.6.1.M2 in the ESPRIT project ParForce 6707....

153.

Strongly Typed Inductive Concept Learning
- P. A. Flach; Flach Giraud-Carrier; J. W. Lloyd
. In this paper we argue that the use of a language with a type system, together with higher-order facilities and functions, provides a suitable basis for knowledge representation in inductive concept learning and, in particular, illuminates the relationship between attribute-value learning and inductive logic programming (ILP). Individuals are represented by closed terms: tuples of constants in the case of attribute-value learning; arbitrarily complex terms in the case of ILP. To illustrate the point, we take some learning tasks from the machine learning and ILP literature and represent them in Escher, a typed, higher-order, functional logic programming language being developed...

154.

A Database Interface for Complex Objects
- Marcel Holsheimer; Rolf A. de By; Hassan Aït-kaci
We describe a formal design for a logical query language using /-terms as data structures to interact effectively and efficiently with a relational database. The structure of /-terms provides an adequate representation for so-called complex objects. They generalize conventional terms used in logic programming: they are sorted attributed structures, ordered thanks to a subsort ordering. Unification of /-terms is an effective means for integrating multiple inheritance and partial information into a deduction process. We define a compact database representation for /-terms, representing part of the subsorting relation in the database as well. We describe a retrieval algorithm based on an...

155.

On the Relationship between Description Logic and Predicate Logic Queries
- Alex Borgida
Description Languages (DLs) are descendants of the kl-one [15] knowledge representation system, and form the basis of several object-centered knowledge base management systems developed in recent years, including ones in industrial use. Originally used for conceptual modeling (to define views), DLs are seeing increased use as query languages for retrieving information. This paper, aimed at a general audience that includes database researchers, considers the relationship between the expressive power of DLs and that of query languages based on Predicate Calculus. We show that all descriptions built using constructors currently considered in the literature can be expressed as formulae of the...

156.

Space Optimization in the Bottom-Up Evaluation of Logic Programs
- S. Sudarshan; Divesh Srivastava; Raghu Ramakrishnan; Jeffrey F. Naughton
In the bottom-up evaluation of a logic program, all generated facts are usually assumed to be stored until the end of the evaluation. Considerable gains can be achieved by instead discarding facts that are no longer required: the space needed to evaluate the program is reduced, I/O costs may be reduced, and the costs of maintaining and accessing indices, eliminating duplicates etc. are reduced. Thus, discarding facts early could achieve time as well as space improvements. Given an evaluation method that is sound, complete and does not repeat derivation steps, we consider how facts can be discarded during the evaluation...

157.

Generic System Support for Deductive Program Development
- Abdelwaheb Ayari; David A. Basin
We report on a case study in using logical frameworks to support the formalization of programming calculi and their application to deduction-based program synthesis. Within a conservative extension of higher-order logic implemented in the Isabelle system, we derived rules for program development that can simulate those of the deductive tableau proposed by Manna and Waldinger. We have used the resulting theory to synthesize a library of verified programs, focusing on sorting algorithms. Our experience suggests that the methodology we propose is well suited both to implement and use programming calculi, extend them, partially automate them, and even formally reason about...

158.

Automatic Parallelization of Irregular and Pointer-Based Computations: Perspectives from Logic and Constraint Programming
- Manuel Hermenegildo
. Irregular computations pose some of the most interesting and challenging problems in automatic parallelization. Irregularity appears in certain kinds of numerical problems and is pervasive in symbolic applications. Such computations often use dynamic data structures which make heavy use of pointers. This complicates all the steps of a parallelizing compiler, from independence detection to task partitioning and placement. In the past decade there has been significant progress in the development of parallelizing compilers for logic programming and, more recently, constraint programming. The typical applications of these paradigms frequently involve irregular computations, which arguably makes the techniques used in these...

159.

Logics for Cryptographic Protocols - Virtues and Limitations
- V. D. Gligor; Gligor Kailar; S. Stubblebine; L. Gong
In this note we offer a perspective on the virtues and limitations of several logics for cryptographic protocols focusing primarily on the logics of authentication. We emphasize the scope limitations of these logics rather than their virtues because (1) we consider their virtues to be better understood and accepted than their limitations, and (2) we hope to stimulate further research that will expand their scope. 1 Introduction Advances in the formal analysis of authentication protocols, based primarily on the logic of authentication of Burrows, Abadi, and Needham [2,4], have stimulated interest in the development of new logics for analysis of...

160.

Completeness Results for Linear Logic on Petri Nets
- Uffe Engberg; Glynn Winskel; Ny Munkegade
Completeness is shown for several versions of Girard's linear logic with respect to Petri nets as the class of models. The strongest logic considered is intuitionistic linear logic, with\Omega , (, & , \Phi and the exponential ! ("of course"), and forms of quantification. This logic is shown sound and complete with respect to atomic nets (these include nets in which every transition leads to a nonempty multiset of places). The logic is remarkably expressive, enabling descriptions of the kinds of properties one might wish to show of nets; in particular, negative properties, asserting the impossibility of an assertion, can...