
Atish Bagchi; Charles Wells
<F4.948e+05> This article discusses some methods of describing and referring to mathematical objects and of consistently and unambiguously signaling the logical structure of mathematical arguments.<F5.393e+05> Key words<F4.948e+05> Mathematical exposition, mathematical argument, formal reasoning, symbolic logic, proofs, terminology.<F5.393e+05> 1 Introduction<F4.948e+05> This article discusses some methods of describing and referring to mathematical objects and of consistently and unambiguously signaling the logical structure of mathematical arguments that, in many texts, remain buried under a few unsystematic hints. In section 2, we discuss the problems involved in referring to mathematical objects and properties. Section 3 discusses certain special aspects of definitions and makes some...

Kaushik De; John A. Chandy; Sumit Roy; Steven Parkes; Prithviraj Banerjee
Combinational logic synthesis is a very important but computationally expensive phase of VLSI system design. Parallel processing offers an attractive solution to reduce this design cycle time. In this paper, we describe ProperMIS, a portable parallel algorithm for logic synthesis based on the MIS multilevel logic synthesis system. As part of this work, we have developed novel parallel algorithms for the different logic transformations of the MIS system. Our algorithm uses an asynchronous messagedriven computing model with no synchronizing barriers separating phases of parallel computation. The algorithm is portable across a wide variety of parallel architectures, and is built around...

Michael Heather; B. Nick Rossiter
The processing of normative statements depends heavily on the embedding of higher order logic within natural language. This is a prime component of legal computer science that needs a theoretical basis which can be realized in practice both as good science and as good engineering. Scientific rigour expects the use of mathematics, and the engineering element needs that mathematics to be constructive. Theoretical computer science has recently seen developments in constructive mathematics satisfying these principles with the use of category theory. An example of this formalism is used to represent the normative statement: John gives Mary the ring and title...

Teodor C. Przymusinski
this paper we show that wellfounded models can also be defined as fixed points of a natural program transformation (factorization) which is completely analogous to the transformation used in the definition of stable models and is expressed entirely in terms of classical, 2valued logic. Subsequently, we use this result to provide a constructive definition of wellfounded models as fixed points of an iterative factorization procedure. We note that no such constructive characterization is available for stable models which are computationally intractable even in the class of propositional programs [KS89, MT88]. The results obtained in this paper, coupled with our earlier...

Andrea Bonarini
this paper, we present issues related to learn behaviors implemented as FLCs, and we propose our approach implemented in ELF (Evolutionary Learning for Fuzzy rules). We are using ELF to support the development of different types of agents. Finally, we present the results that we have obtained both in simulated and real environments.

J.M.E. Hyland; C. h. L. Ong
) 1 J. M. E. Hyland 2 C.H. L. Ong 3 University of Cambridge, England Abstract This paper is motivated by the discovery that an appropriate quotient SN 3 of the strongly normalising untyped 3terms (where 3 is just a formal constant) forms a partial applicative structure with the inherent application operation. The quotient structure satisfies all but one of the axioms of a partial combinatory algebra (pca). We call such partial applicative structures conditionally partial combinatory algebras (cpca). Remarkably, an arbitrary rightabsorptive cpca gives rise to a tripos provided the underlying intuitionistic predicate logic is given an interpretation in...

Florent De Dinechin; Doran K. Wilde; Sanjay Rajopadhye; Rumen Andonov
. We present an application specific, asynchronous VLSI processor array for the dynamic programming algorithm for the 0/1 knapsack problem. The array is derived systematically, using correctnesspreserving transformations, in two steps: the standard (dense) algorithm is first transformed into an irregular (sparse) functional program which has better efficiency. This program is then implemented as a modular VLSI architecture with nearest neighbor connections. Proving bounds on buffer sizes yields a linear array of identical asynchronous processors, each with simple computational logic and a pair of fixed size FIFOs. A modular solution can be obtained by additional loadtime control, enabling the processors...

Arnaud Lallouet; Lionel Martin
Inductive Logic Programming, which consists in learning clauses from examples, can be viewed as a cycle conception/validation leading to the acceptance of the induced program provided that it fulfills a certain criterion. We focus on the validation step in the context of empirical multipredicate learning of normal clauses. Thanks to a compositional semantics, the classical validation step of the complete induced program can be replaced by the verification of local properties for a cut out into units, considerably limiting the usual combinatorial explosion. Moreover, we provide a semanticspreservative transformation which allows to simplify the program and provides a further refinement...

Uwe Egly; Hans Tompits
. Although it has been shown that nonmonotonic reasoning is presumably harder than classical reasoning, there are cases where a nonmonotonic treatment actually simplifies matters. Indeed, one of the reasons for considering nonmonotonic systems is the hope of speeding up reasoning, and not to slow it down. In this paper, we consider proof lengths in a cutfree sequent calculus, and we show that the application of circumscription (or completion) to certain firstorder formulae leads to a nonelementary speedup of proof length. This is possible because the introduction of the completion formula can simulate the cut rule. 1 Introduction In the...

Kutty Moser; G. Kutty; L. E. Moser; P. M. Melliarsmith; L. K. Dillon; Y. S. Ramakrishna
. Future Interval Logic (FIL) is a lineartime temporal logic that is intended for specification and verification of reactive and concurrent systems. To make FIL useful for specifying and reasoning about practical systems, we present a firstorder extension of FIL, including equality and nary function and predicate symbols, and a set of sound proof rules for reasoning in the logic. We illustrate the use of the logic by specifying a sliding window protocol and proving that the specifications satisfy a set of correctness requirements. 1 Introduction Future Interval Logic (FIL) is a lineartime temporal logic, the textual counterpart of Graphical...

ChauShen Chen; TingTing Hwang; C. L. Liu
In this paper, technology mapping algorithms for minimizing power consumption in FPGA design are studied. The technology mapping problem for power minimization has been shown to be NPcomplete. Furthermore, there are other important objectives, such as the number of PLBs (Programmable Logic Blocks), the number of levels and so on, that should also be optimized simultaneously. We propose a transformational approach in which we start with a mapping solution which optimizes certain objective(s) (e.g., the number of PLBs.) The mapping solution is then transformed to reduce the power consumption while keeping the number of PLBs fixed. Our algorithm explores the...

Chris Hankin; Daniel Le Métayer
The role of nonstandard type inference in static program analysis has been much studied recently. Early work emphasised the efficiency of type inference algorithms and paid little attention to the correctness of the inference system. Recently more powerful inference systems have been investigated but the connection with efficient inference algorithms has been obscured. The contribution of this paper is twofold: first we show how to transform a program logic into an algorithm and, second, we introduce the notion of lazy types and show how to derive an efficient algorithm for strictness analysis. 1 Introduction Two major formal frameworks have been...

Jan Krajícek
1 LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives : and V ; W (both of unbounded arity). Then for every d 0 and n 2, there is a set T d n of depth d sequents of total size O(n 3+d ) which are refutable in LK by depth d + 1 proof of size exp(O(log 2 n)) but such that every depth d refutation must have the size at least exp(n\Omega\Gamma21 ). The sets T d n express a weaker form of the pigeonhole principle. It is a fundamental problem of mathematical...

Research Team; Ludek Matyska; David Toman
Machine (WAM) is provided. The second part is devoted to the presentation of a new solver for linear arithmetic constraints, specifically developed for the CLP(R) system. In the third part, results related to the operational semantics of full Prolog and WAM are presented. 2 Register Allocation in WAM The Warren Abstract Machine (WAM) is widely recognized as an excellent implementation schema for PROLOG on traditional architectures. Nevertheless many improvements have been suggested for the original WAM. One of the important parts for optimization is the register allocation in process of unification responsible for data assignment and parameter passing. Most improvements...

Volker Krebs; Rolf Böhm
A new direct design method for fuzzy controllers will be presented in this paper. It combines the lucid strategy of compensation used in conventional control systems and the straight forward determination of a fuzzy controller by means of the chain rule of propositional logic. The quality and potential of the proposed method is demonstrated by the design of a fuzzy controller for an automatic clutch management system for motorvehicles.

Neil Immerman
this paper a series of languages adequate for expressing exactly those properties checkable in a series of computational complexity classes. For example, we show that a property of graphs (respectively groups, binary strings, etc.) is in polynomial time if and only if it is expressible in the first order language of graphs (respectively groups, binary strings, etc.) together with a least fixed point operator. As another example, a property is in logspace if and only if it is expressible in first order logic together with a deterministic transitive closure operator. The roots of our approach to complexity theory go back...

F. Herrera; F. Herrera; E. Herreraviedma; E. Herreraviedma; J. L. Verdegay; J. L. Verdegay
Assuming a set of linguistic preferences representing the preferences of the individuals, a linguistic choice process is presented. This is developed using the concept of fuzzy majority for deriving a collective linguistic preference; and the concept of nondominated alternatives for deriving the selected alternatives in the linguistic choice process. The fuzzy majorities are equated with fuzzy linguistic quantifiers. The collective linguistic preference is derived by means of a linguistic ordered weighted averaging operator whose weights are defined using a fuzzy linguistic quantifier. In order to obtain the nondominated alternatives we present a novel reformulation of Orlovski's nondominance degree under linguistic...

Anoop Sarkar
This paper is a review of several results that connect the areas of theoretical computer science (particularly automata theory and contextfree grammars) and logic (particularly decidability results of the second order theories). In particular, the properties of the set of trees accepted by finite state tree acceptors  also called recognizable sets are studied. The results presented are interesting because they give rise to an alternate characterization of the notion of a contextfree grammar resulting in a descriptive complexity result for the theory of contextfree languages and on the other hand, the results presented give a novel decidability result for...

Gilles Dowek; Therese Hardin; Claude Kirchner
We give a firstorder presentation of higherorder logic based on explicit substitutions. This presentation is intentionally equivalent to the usual presentation of higherorder logic based on calculus, i.e. a proposition can be proved without the extensionality axioms in one theory if and only if it can in the other. Applying the Extended Narrowing and Resolution proofsearch method to this theory simulates higherorder resolution step by step. Hence expressing higherorder logic as a firstorder theory and applying a firstorder proof search method does not necessarily lead to inefficiencies. As we stay in a firstorder setting, extensions, such as equational higherorder resolution,...

Kathryn Fisler; Curriculum Vita; Advisors K. Jon Barwise; Steven D. Johnson; Advisor Moshe; Y. Vardi
ieber Outstanding Associate Instructor Award, Indiana University 1991, 1992 NSF Fellowship Honorable Mention 1991 Goldberg Award for Best Student Colloquium Speaker, Department of Computer Science, Williams College Journal Papers Fisler, Kathi. Timing Diagrams and Algorithmic Verification. Journal of Logic, Language, and Information. To appear, Spring 1999. Refereed Publications Fisler, Kathi and Moshe Y. Vardi. Bisimulation Minimization in an AutomataTheoretic Framework. International Conference on Formal Methods in ComputerAided Design (FMCAD), 1998. Fisler, Kathi and Claude Girault. Modelling and Model Checking of a Shared Memory Consistency Protocol. International Conference on Applications and Theory of Petri Nets, 1998. Fisler, Kathi. Containment of Regular...