In ordine cronologico inverso

Ricerca per parola chiave

123-94

Automatic Thesaurus Construction Supporting Fuzzy Retrieval of Reusable Software
E. Damiani, M.G. Fugini
A bottleneck in software reuse is the effective selection of components based on the requirements of new applications. Particularly when large software libraries, or repositories of components are available, it is important to have a complete set of development functionalities oriented to reuse, including retrieval functionalities based both on a standard query language and on linguistic tools supporting imprecise queries. This paper presents a fuzzy retrieval model based on classification of reusable components in a object- oriented repository that is a part of a development Information System. The repository stores descriptors of the whole development process of reusable components; these descriptors include fuzzy-weighted keyword pairs describing components functionalities, such as provided services, needed data, required system architectures. Fuzzy weights are computed automatically by the system.The retrieval is supported by a Thesaurus where a fuzzy synonymia relationship is defined. Synonymia values are used to compute adaptability between components, i.e., how well the available components can be used in lieu of the ones requested by the user. A mechanism for the automatic construction of the Thesaurus is proposed. A query mechanism for the retrieval process is also outlined.

122-94

Conceptual Search among Distributed Knowledge Sources
S.A. Cerri, A.S. Fabiano
In the paper we describe how a common conceptual model of the application domain can be used to support a cooperative and concurrent search among loosely coupled knowledge sources distributed over a network with unknown topology. The introduction of a conceptual level, shared among all the knowledge sources in the net, allows to obtain independence from the logical data organization of each node, not only from the physical as it is in the case in DDBMS. The Navigation process is based on the conceptual model and has been designed and developed by means of a set of cooperative agents, with specific knowledge and abilities, that reason about the local data and and exchange information to ensure both the communication through the net and the information processing at each net node. In order to ensure the comprehension of the architecture we include a worked out example in the domain of pharmacology, where such a model and its associated domain specific language has been realized.

121-94

Le nuove tecnologie: una silenziosa rivoluzione cognitiva
G. Degli Antoni
Questa rassegna, che estende il precedente Rapporto Interno 81-90, raccoglie alcuni scritti di Giovanni Degli Antoni, pubblicati dal 1988 al 1994 sulle idee di Realtˆ Artificiale, Multimedialitˆ, Ipertesti, Reti, ed altro, al fine di analizzarne il significato all'interno della rivoluzione cognitiva in atto nei sistemi di comunicazione uomo-macchina e di indicarne le implicazioni tecnologiche, economiche e sociali.

120-94

Guidelines for the Identification of Basic Architectural Abstraction
F. De Paoli
The increasing interest in the architectural languages derives mainly from the lack of architectural abstractions capturing the basic concepts with a well- defined interface, including connectors which specify logical channels and user-defined communication protocols; Dynamic configuration; Control strategies, including the explicit management of time. The paper introduces a set of architectural abstractions defined according to the principles on minimality, completeness, and separation of concerns. After a brief survey of the evolution of architectural languages and models, four classes of abstractions modeling computing agents, connectors, configurators and controllers are presented in terms of independent abstract machines. Finally the status and the guidelines of a project, HyperReal aimed at definig and experimenting basic architectural abstractions, are presented.

119-94

A Proof-Theoretic Characterization of Constructive Negation throgh regular Splitting
A. Momigliano, M. Ornaghi
We present a form of constructive negation based on the notion or regular plitting, a simple tranformation technique where the failure axiom(s) of the predicate occurring negatively in the program are split into new clauses according to a covering of the underlying signature. This is pursued in the framework of the proof-theoretic analysis of Horn and normal clauses initiated in "A. Momigliano, based on the notion of regularity. We show how normal regular programs enjoy under negation-as-failure the same properties of Horn ones.

118-94

HyperRreal: the sw Lifecycle
F. Tisato, A. Verdino
HyperReal defines an architectural model for embedded systems. The model follows the Light-Weight Operating Software approach, that de-kernelises all the functionalities of the system. HyperReal One (HR1) is a prototype implementation of HyperReal. The Programming Environment consists of two major parts: the programming-in-the-small environment and the programming-in-large one. The programming-in-the-small environment supports the definition of the actor classes. The programming-in-the-large environment allows to specify the topology of a component and the planning of its activities. It relies on Metaclasses and Metaobjects. User friendly interfaces and specialised tools (e. g. for the scheduling analysis) are built on top of the metarepresentation and support the programming-in-the-large activity. The report overviews the general lifecycle of HyperReal applications and present in detail the HR1 environment for programming-in-the-large.

117-94

Approximation Complexity of Longest Common Subsequence and Shortest Common Supersequence over fixed alphabet
P. Bonizzoni, M. Duella, G. Mauri
We consider the complexity of the Longest Common Subsequence (LCS) and Shortest Common Supersequence (SCS) problems restricted to a fixed alphabet of size k. The LCS and SCS problems are shown to be MAXSNP- hard for strings over an alphabet of size 2, which proves that these problems over a fixed alphabet have a polynomial time approximation scheme iff P = NP.

116-94

Learning Computing: understanding Objects includes understanding Variables and Functions
S.A. Cerri
In the context of environments for learning computing, traditionally the model has been to consider "the role of variables" as central for the conception as well as for the implementation of software. A good example is the thesis of J.F. Brette, presenting PASCAL/V [Brette, 1994]. Let us limit ourselves to understanding computing in a single processor machine, therefore excluding parallel and concurrent computing. Our long term purpose is to introduce a distinction between learning programming and learning design; between an engineering and an architectural approach to systems. We identify this architectural view with the one called "experimental" in [Academy of Sciences, 1994]. While in the first case programming algorithms is the focus, in the second the issue is to identify and link software and hardware modules that include data and functionalities. At the moment, the most popular technology that embodies these notions is the Object Oriented one. If that is the case, the model to "learn" is the one shown by the behaviour of objects, i.e; a descriptive one that hides the private variables and activates private functionalities representing algorithms; where the overall control is modelled by the message exchange. We show in the lecture that it is rather easy to understand the behaviour of objects by means of a functional model such as the one in SCHEME. Although this, as a language, is by no means new, a reflection on the computational model of SCHEME gives a quite broad insight into what may be done for improving learning environments such as the one in [Brette, 1994]. We claim that an architectural approach is more general with respect to a purely engineering approach because it includes the engineering components at the level of the implementation of the algorithms representing methods in objects. Such a descriptive, intrinsically distributed approach allows to conceive more concise, abstract and modular solutions to specific problems, in a wide variety of domains.

115-94

Two-sided Quantales, Lattices and Sheaves
F. Miraglia, U. Solitro
In this work we study the theory of presheaves over a two-sided quantale Q, starting from a more general categorical definition of presheaf over a lattice. We concentrate our attention on a Q-valued equality obtaining a characterization of presheaves and their morphisms in terms of quantale- valued sets; with the results contained in this paper we emphasize the role of the separation property in this context. A non trivial example in the theory of (non commutative) rings is presented.

114-94

A Parallel Version of Earley's Algorithm
D. Bruschi, G. Pighizzini
In the world of sequential computation the most referenced algorithms for recognizing context--free languages are the CYK algorithm introduced in 1963by Cocke, Younger and Kasami, and Earley's algorithm introduced in 1970.The former only deals with grammars in Chomsky normal form while the latter deals with every context--free grammar.When in early 70's people started investigating parallel algorithms, immediately it appeared that obtaining efficient parallel parsers was not easy.In fact in 1977 Jones et al. proved thatthe construction of a context--free recognizer is a P--complete problem.In 1980 however Ruzzo and Rytter showed that when we restrict our attention to context--free grammars in Chomsky normal form, the P-- completeness result just mentioned can be overcome.In fact a parallel version of CYK can be obtained using Ruzzo and Rytter results.On the other hand, Jones et al. result seems to deny the possibility of having a ``parallel equivalent'' of Earley's algorithm.In this paper we show that this consideration is not true.More preciselywe will show how to obtain a parallel algorithm for recognizing a language specified by a whatever context--free grammar. Using such an algorithm we will further describe a parallel algorithm for the parsing phase. To our knowledge these are the first parallel algorithms which solve such problems.

113-94

HyperReal: Light-Weight Operating Software for Embedded Systems
A. Poli, F. Tisato
An architectural model for embedded systems is presented. The model follows the Light-Weight Operating Software approach, that de-kernelises all the functionalities of the system. The separation of concerns principle leads to the definition of a set of abstract machines, each supporting a specific issue. The ActorMachine supports the execution of Actors defined at the programming-in-the-small level. The ConnectorMachine supports the communication among actors by means of Connectors, which define logical links among actors and implement communication protocols. The ControlMachine manages the execution of actions, i.e., methods of actors, according to an Agenda where actions are scheduled in a temporal framework defined by virtualClocks. The PlanningMachine allows to define plans which specify when actions must be executed. The StarterMachine allows to initialise the system. A Component is a configured collection of actors, connectors and plans. The ComponentMachine provides the platform for the execution of a component and encapsulates the system dependent issues. Keywords: embedded applications, light-weight operating software, actors, connectors, communication models, control, planning, configuration

112-94

Un modello di automi cellulari per la fluidodinamica della percolazione in mezzi porosi a geometria variabile
G. Cattaneo, M. Rigotti, A. Sala
A bidimensional Cellular Automaton model for the hydrodynamics of percolating systems is presented. The model uses a set of rules that describe the same conservation principles of the Navier-Stokes equations. In particular a new transport rule describes the variability of a porous structure. The obtained simulations show, as emergent properties of the automation evolution, the same qualitative behaviors of the real system.

111-94

Random generation of words of an algebraic language in linear binary space
M. Goldwurm
For every unambiguous context-free language L, a uniform random string of length n in L can be generated in O(n) binary space. The procedure uses a number of memory entries proportional to the height of a suitable derivation tree of the output word. The algorithm is based on a general technique for random generation proposed by Flajolet, Zimmermann and Van Cutsem in a recent paper, that works in O(nlog n) time in the worst case. Our procedure obtains the same worst case time bound up to a constant factor.

110-94

A distributed model for selection in Evolutionary Algorithms
Andrea Tettamanzi
This paper introduces and studies a local selection scheme for Evolutionary Algorithms based on competition, particularly suited for implementation on massively parallel architectures. In many tasks, such as evolution of game strategies, Genetic Programming and evolution of control procedures, competition between two individuals on one problem instance chosen according to some probability can be a valid alternative to defining an appropriate fitness function that embeds a priori knowledge of the problem, which often is not within the reach of everybody, as it requires a deep insight of the problem along with some mathematical skills. The behaviour of a population subject to competitive selection is analysed probabilstically through the study of a statistical indicator under different assumptions about the distribution of fitness values.

109-93

An Integrated Environment for Distance Education supporting Multiple Interaction Styles
S. Pozzi, A. Tancredi, F. Tisato
The architecture of an open software platform supporting the set of different activities characterizing a typical complex educational process is presented. The architecture, which is based on a unifying data model, offers a set of services allowing to control co-operation activities based on either a synchronous or asynchronous interaction styles. These services allow to store the history of the interactions occuring among the actors of the educational process, and to plan the occurence of cooperating activities. The software platform built on top of the proposed architecture can be used for integrating both specialized tools supporting specific activities of the educational process. The paper introduces the general data model, discusses the cost-effective use of communication media in contrast with different co-operation styles, and exemplifies the proposed approach by illustrating two case-studies: an electronic mail-based system for distance tutoring (TEMPO), and a software environment for real-time multimedia conferencing (ImagineDesk).

108-93

A Maximal Intermediate Predicate Constructive Logic
A. Avellone, C. Fiorentini, P. Mantovani, P. Miglioli
We provide an example of maximal intermediate predicate logic with the disjunction property and the explicit definability property which contains the well known Medvedev's propositional logic of the finite problems. We also show that (differently from Medvedev's logic) our intermediate predicate logic cannot have a Kripke frames semantics. Indeed, we introduce an auxiliary nonstandard predicate logic by means of a special "non kripkean semantics", and characterize our logics in terms of such a nonstandard logic, according to a method which has been applied in previous papers to get maximal intermediate predicate logics with the disjunctions property. Our technique to single out maximal intermediate predicate logics with the disjunctions property and the explicit definability property starting from suitable auxiliary nonstandard predicate logics is not as general as the corresponding propositional one; however, we believe that it can be successfully applied also outside the context of the present paper.

107-93

Synchronic distances as Generalized Regions
L. Bernardinello, G. De Michelis, K. Petruni

106-93

A Probabilistic Model to Evaluate the Performances of Deflection Networks
E. Pagani, G. P. Rossi
In this report we present a probabilistic model to evaluate the performances of networks that use deflection routing on mesh topology. By considering each deflection network node as a system of queues and byassigning to each input traffic pattern the probability to enterone of the output links according to deflection routing policy, it is possible to estimate performance indexes for different topologies and traffic loads.To this purpose, we run the analytical model by using the Mathematica software.The results have been compared with those previously obtained through simulations. The comparison is encouraging and indicates that the analytical model properly describes the deflection network node's behaviours.

105-93

Un modello di automa cellulare per l'interazione radiazione- materia: il laser a semi-conduttore
G. Cattaneo, F. Magni, M. Milani, M. Rigotti
A two--dimensional Cellular Automaton (CA) model is proposed for a semiconductor laser system, showing qualitative behavior in agreement with actual performances.The description of this simple structure is preliminary to extending the CAapproach to more complex systems (External Cavity devices, or lasers with optical feedback) and to more complex radiation-matter interactions as those deriving from electrostriction and Kerr effects.

104-93

A tight lower bound for Primitivity in k-structures
P. Bonizzoni

103-93

A Ring Based Multicast Service over a High Speed Deflection Network
E. Pagani, G. P. Rossi
A simple ring support structure has been used to provide multicast service over a prototype of high speed network that uses deflection routing on mesh topology. By exploiting the behaviour of Deflection Networks it is possible to ensure, with a simple protocol, a significant performance improvement with respect to n-unicast communications and to obtain results that are close to those achievable with tree based multicasting. Further, the devised multicast protocol has a simple implementation that does not affect the on going prototype development. The paper shows that added value services can be provided on top of datagram Deflection Networks to extend the LAN services to larger geographical areas.

102-93

Computing Subsumption Between Action Descriptions
C. Bettini
We extend a recent proposal for a terminological language intended to represent actions and plans. We highlight an expressiveness problem regarding the representation of actions in that language. The absence of a universal quantifier over temporal variables does not allow a correct representation of a state and, therefore, the representation of an action. We provide a new operator - a restricted temporal universal quantifier - to overcome this problem. Computational issues are addressed proposing algorithms to compute subsumption between action representations in the original and extended languages.

101-93

The Structured Consequence Relation in Prolog
D. Fava

100-93

An Object-Oriented Approach to Logical Deduction
D. Fava

99-93

How to avoid duplications in refutation systems for intuitionistic logic and Kuroda logic
P. Miglioli, U. Moscato, M. Ornaghi
Both at the propositional and the predicate level, in tableaux systems of intuitionistic logic as well as in the corresponding sequent and natural calculi, the problem arises of reducing as much as possible the duplication of formulas, i.e., the reuse of formulas already used in a proof, in order to single out efficient proof search techniques. This problem has been analyzed by Dyckhoff, where a nearly optimal solution is given for intuitionistic propositional sequent and natural calculi, and in other our previuos papers where an improvement is proposed of Fitting's tableaux system for intuitionistic predicate logic. In the present paper we reanalyze our previous ideas in the light of Dyckhoff's results, which are considered from the point of view of a refutation calculus and in the frame of full first order logic. This gives rise to a tableaux system for intuitionistic predicate logic which should provide a good improvement of the previous systems with respect to the problem of duplication. The formal setting of the paper seems to be promising to treat further intermediate logics. In this line, we analyze Kuroda logic and provide for it a tableaux system involving a smaller amount of duplication than the one involved in the intuitionistic refutation calculus presented in the paper.

98-93

A method to single out maximal propositional logics with the disjunction propery.
M. Ferrari, P. Miglioli
We study a class of intermediate propositional logics with the disjunction property which cannot be properly extended into logics of the same kind, and are therefore called maximal. To deal with these logics, we use a method based on the search of suitable nonstandard logics. The method has an heuristic content and has allowed us to discover a wide family of logics, as well as to get their maximality proofs in a uniform way. In presenting our maximal logics, we will also propose some ideas for a classification of them.

97-93

Abstract parametric classes and abstract data types defined by classical and constructive logical methods
P. Miglioli, U. Moscato, M. Ornaghi
We introduce a methodology to treat abstract data types (ADT), abstract parametric classes (APC) and subclasses, together with appropriate inheritance properties, by means of first order theories. The notion of a first order theory axiomatizing an ADT is based on the notion of an isoinitial model and has been proposed by the authors in previous papers. A theory formalizing an APC is seen, in this paper, as a theory T incompletely axiomatizing an ADT. Given a class C of ADT's, the class formalized by T can be seen (under suitable soundness conditions on T) as the class of the instantiations of T over C. An instantiation of T over an ADT I of C completes T into a T' formalizing an ADT I', which extends I and inherits the properties of the APC T.We use both classical and constructive methods in the following sense: on the one hand, the semantics is based on classical model theory; on the other hand, the soundness of a consistent axiomatization can be analyzed by purely syntactical methods, in terms of provability within suitable constructive systems.A theory T formalizing an APC (or an ADT) is not given by a list of axioms, but by a suitable "APC-expression", which explicitly or implicitly (but effectively) defines the axioms of T. We have APC-expressions to define APC's, to extend already defined APC's and to instantiate APC's (into ADT's or subclasses). We allow also "recurrence APC-expressions". At the end of the paper we give some examples showing how the proposed methodology works.

96-93

Some uses of model theory to specify abstract data types and to capture their recursiveness
A. Bertoni, G. Mauri, P. Miglioli
In this paper we present a comparative analysis of some algebraic-categorial tools and of some model theoretic tools to characterize abstract data types: our aim is to show that, in order to capture a quite relevant feature such as the recursiveness of abstract data types, Model Theory works better than Category Theory. To do so, we analyze from a model theoretic point of view various notions such as "initiality", "finality", "monoinitiality", "epifinality", "weak monoinitiality" and "weak epifinality", the latter being also called "terminality": this analysis is carried out from the double point of view of "abstractness" (which of these notions gives rise to unque up to isomorphisms models) and of "cardinality". For the second aspect, in a general model theoretic frame the considered notions do not necessarily give rise to countable models. So, we state which of them allow to select countable models: it turns out that only "initiality", "monoinitiaity", "epifinality" and "terminality" capture countability if theories with a countable language are involved, while this is not the case for "finality" and "weak monoinitiality". Countability is seen as a necessary condition to get recursive data types. An extensive analysis is then devoted to the problem of the recursiveness of abstract data types: we provide a formal definition of recursiveness and show that it neither collapses, nor it is incompatible with the "abstractness requirement". We also show that none of the above quoted categorial notions captures recursiveness. Finally, we consider our own definition of "abstract data type", which has been already presented in previous works and is based on typically model theoretic notions, even if in there we have erroneously emphasized the notion of "monoinitiality": we analyze our definittion in the frame of the proposed formalization of recursiveness, and illustrate the sense according to which it captures recursiveness.

95-93

Un approccio alla Programmazione Metalogica Orientata agli Oggetti
S. Costantini, G. A. Lanzarone, F. Tiberi

95-92

Tecnologie informatiche e processo di istruzione : un approccio integrato
A. Tancredi, F. Tisato
English title: Information Technologies and Educational Process: An Integrated Approach The report introduces a model of the educational process that can be easily translated into the implementation of a real system, and that establishes a common language for the communication among computer and education scientists. The educational process is modeled as a collection of functions connected by feedbacks, and relies on informations represented as educational objects connected by relations. This representation is the basis for a platform thatt allows to build open-ended educational systems that cover all the phases of the educational process.

94-92

Metalevel Negation and Non Monotonig Reasoning
S. Costantini, G. A. Lanzarone

93-92

KBLab 1.7: user manual
A. Paccanaro
KBLab (Knuth-Bendix Laboratory) is an application for experimenting the use of rewriting techniques and for rewriting-based theorem proving. Its aim is to provide an highly interactive, user friendly tool to be used both for research and teching in rewriting. It implements Knuth-Bendix completion method and its extensions Unfailing Knuth-Bendix and S-Strategy. It supports the Knuth-Bendix Ordering, the Recursive Path Ordering and a number of different strategies for selecting axioms during the completion process. KBLab provides an easy-to-use environment which allows to edit theories, execute the completion procedures and store proof traces. The kernel of KBLab is coded in C and it is fully portable; the interface is made up of HyperCard stacks and it is available for all Macintosh systems.

92-91

Extending security models for frame based systems protection
S. Castano, G. Martella, P. Samarati
This paper contains describes a security model for the protection of frame based systems. The model enforces both a mandatory and a discretionary policy. A labelling policy is also provided to regulate the classification of objects semantically related. Acces controls against the mandatory and the discretionary policies are illustrated. Finally, the problems concerning the insertion and the deletion of multi-level objects are discussed.

91-91

A constructive logic approach to database theory
P. Miglioli, U. Moscato, M. Ornaghi
In this paper we propose an approach to database theory based on a constructive logic. The semantics here assumed is a particular one; it is based on the notion of info (K,F) (the information type of F), where K is the set of constants of a first order language L, F is a formula of L and info (K,F) is the set of all the possible pieces of information (within L) on the "truth" of F. This constructive sematics will be used to treat problems related to relational databases such as disjuntive information and null value.

90-91

Ambienti interattivi per la didattica
G. Degli Antoni
The note aims to present a very concise and abstract view on evolution of teaching-learning technologies. The emerging concepts (graphical user interfaces, multimedia, hypermedia) related to technologies are considered and shortly reinterpreted. The theater methapor is introduced where interactive actor (called interactors) play the role in a scene. The Hyper dimension is introduced as related to the user interaction hystories. The Hyper is investigated very shortly as a methapor in order to investigate the way to next developments in structural technologies related both the DWIM (Do What I Mean) paradigm and to the so called Intelligent Tutoring Systems.

89-91

Lezioni di meccanica del coordinamento (English text)
A. Holt
There follow notes prepared in conjunction with a set of eight lectures on coordination mechanics given in the spring of 1991 as part of the course called "Elaborazione dei Testi Letterari" of Prof. G. Degli Antoni. Coordination mechanics falls within the broad domain of systems theory, or cybernetics. It is a scientific approach to a certain aspect of organized human activity - namely "the achievement of coordination between a moltitude of operations carried out by a multitude of persons", in no matter what field of activity. Coordination in this sense is always required if a moltitude of operations is to compose a functionally meaningful whole. The achievement of coordination depends upon the existence of appropriate "causal connections" between operations, connections which, in their turn, depend upon the physical arragements and the persons involved. Much interest in coordination mechanics relates to improving the understanding of how to employ computers and computer networks in the context of particular human enterprises (for other, older forms of physical arrangement supporting organized activity, radition and experience can often take the place of systematic knowledge). The notes are divided in two parts. Part I is a beginner's introduction to coordination mechanics in condensed form. Part II consists of a set of three problems which provide exercise in the application of most of the concepts introduced in Part I. These problems, though small, have enough complexity and/or reality to be interesting.

88-91

A question answering system for ENProver
R. Virga
This paper describes the structure of a question answering system that uses a semantic-based reverse-skolomization process, which has been developed at the Computational Architecture Laboratory, University of Milano, as part of the ENProver theorem proving system.

87-91

AUTOMATA and NEURALWORKS: learning environments for Automata Theory and Neural Nets (documentation)
M.A. Alberti, P. Marelli, N. Nardini, A. Paviglianiti, M. Scagliotti
This paper documents the applications that have been developed in the COLOS Project with the goal of implementing a learning environment for the computation of finite automata and formal languages and for the design of neural nets. The environment makes use of computer graphic as a way of conveying information and concepts. Some modules implement different models of computations: Turing machines, finite state automata, both deterministic and non deterministic, deterministic pushdown automata and context free grammars; other ones implement different models of neural nets: McCulloc and Pitts neural nets and back error propagation learning algorithms. The applications are implemented in Objective-C under UNIX for HP workstation. The development is RMG.

86-91

Communicating Petri Nets
G. Degli Antoni
In this paper basic Petri Nets models are re-viewed. Their difficulties in modelling some real systems (cognitive and epistemological difficulties) are analyzed. In order to overcome these difficulties, the basic models (Conditio Event/Elementary Net) are extended. The proposed extension embodies a basic mechanism of communication, whereby the holding of a transmitting condition lets the receiving events fire, whenever these have concession in the classical sense. The corrisponding token rule suggested, leading itself to a natural extension of the notion of Petri Nets, where there is communication between different Nets (component) modelling parts of a single system. Simple examples are given in order to illustrate the easiness in modelling the proposed extension of Petri Nets. It is observed that the proposed extension fit with a general movement towards object orientation in modelling complex concurent systems.

85-91

Equational grammars
A. Tettamanzi
In this paper we suggest that a grammar may be viewed as an equational theory. Accordingly, the parsing or generating process taken the form of an algebraic simplification. As a consequence, conceptions and techniques which lia in the field of equational logic may be appliad to the study of grammars.

84-91

The category of weak pretopologies
S. Valentini, P. Virgili
This paper contains a brief introduction to formal topologies and weak pretopologies. These mathematical structures are the basis to present in a natural way Scott domains and to construct the usual compaund domains with a clear insight due to the topological intuition.

83-91

Technology and scientific thinking
G. Degli Antoni

82-90

Tecniche di theorem proving nella validazione dell'hardware
U. Pellizzari

81-90

Realtà artificiale: una silenziosa rivoluzione cognitiva
G. Degli Antoni
The paper presents a series of articles and (impublished) reports that the author has written since 1988. The overall aim has been to demonstrate how the versatility of computers is currently favoring the development of technologies oriented toward lending support in various ways to human cognitive activities. In the first way, computer become models interacting with reality. In second one, the cognitive acquisition of reality by means of interactive computerized models is facilitated by the iconic-graphic-graphemic nature of man-machine communication oriented toward dialogue with the models. Then the integration of models which interact with the corrisponding real systems transforms the model themselves into an alias of reality, thus allowing the users to integrated at a distance with a form of virtual telepresence. Lastly, the possibility of interfacing the users with the interactive models by menas of opportune devices makes it possible for users themselves to virtually be in the modeled reality, since they have a three- dimensional perception and can also perform actions and movements through the interpretation the computer makes of their gestures. Thus man-system communication becomes total-media, in the sense that voice, gestures, symbols, images, animation... become elements of the communication.

80-90

Una specifica del sistema ascensore con reti OBJSA
E. Battiston
The OBJSA Nets combine Petri Nets with algebraic specification techniques in order to allow both process abstraction and data abstraction. In particular, in this formalism, a real system is specified by a Superposed Automata and an OBJ module. In this report the new definition of an OBJSA Nets, given in 90-79, is applied to the specification of an example of not trivial size, the Lift system, included in the selected case studies of the ESPRIT-BRA # 3148 DEMON Project.

79-90

OBJSA Nets : definitions
E. Battiston
This report contains the new definition of OBJSA Nets, i.e. the definition of the class itself, of the notions of transition enabling and transition firing, of the linear form (the incidence matrix) togheter with all needed for defining S- and T- invariants and proving the corrisponding main theorems. This new definition maintains all the basic characteristics of the original definition and differs from it because of the following extensions and updating: 1) it introduces an arc weight and thus it allows an OBJSA Net to model mutual interactions among more istances of the same component; 2) the making function is defined by associating an OBJ module with each place; 3) some changes in the definition of the OBJ modules, which are built in a OBJSA Net, are due to heir careful checking on the OBJ3 interpreter.

78-90

OBJSA Nets : OBJ and Petri nets for specifying concurrent
systems
E. Battiston, F. De Cindio, G. Mauri
The paper provide an intuitive presentation of OBJSA Nets, a specification language which combines a specific class of Petri nets, namely Superposed Automata Nets, and the well-known algebraic specification language OBJ. The presentation is particularly addressed to people confident with algebraic specification techniques and focuses the composition mechanism which allow to designer to obtain an OBJSA specification (of a system) by combining a set of OBJSA components (the specification of system components).

77-90

Concurrent systems as a local state transformation algebras: the case of elementary net systems
L. Pomello, C. Simone
The paper presents an algebraic characterization of the state of space associated to an EN-system. The characterization captures the system behaviour in terms of local state transformation by means of which some system properties can be expressed. In addition, the paper shows ho to derive the algebra from the system and conversely the system from the algebra. On contact-free EN-system a preorder is defined by means of an injective morphism between the associated algebras. The set of contact-free EN-system with the above preorder is shown to be a complete partial order. The conclusion shown the connections with some related approaches.

76-90

About asynchronous cellular automata
G. Pighizzini
In this paper two models of distributed systems are compared: asynchronous automata and asynchronous cellular automata, whose behaviours characterize the class of recognizable trace language. It is proved that these models are polynomially related, by exhibiting a polynomial time rediction between them. Despite of that, it is shown that the structure of the categories associated to asynchronous automata and asynchronous cellular automata recognizing the same trace language are deeply different. In particular, it is exhibited a trace language that admits an unique minimum asynchronous automation, but infinitely many minimal (i.e. non reducible) asynchronous cellular automata recognizing it. Furthermore, it is characterized the class of free partially commutative monoids such that every trace language admits a minimum asynchronous cellular automation as the class of free totally commutative monoids.

75-90

A structural overview of NP optimization problems
D. Bruschi, D. Joseph, P. Young
This paper survey structural work on calculating optima solution for NP complete problems. This overview is not intended to be an exaustive description of the area, nor even of all the works in those papers which we discuss. Instead, it an attempt to provide a general introduction to the area. As a consequence the authors have freely unified notations and simplified statements of results. This survey will provide a guide to some of the more interesting ideas and problems in this area.

74-90

Generalized boolean hierarchies and boolean hierarchies over RP
A Bertoni, D. Bruschi, D. Joseph, M. Sitharam, P. Young
In this paper we study the complexity hierarchy formed by taking the Boolean closure of sets in RP, the class of sets decidable in random polynomial time. This hierarchy, which we call the Boolean hierarchy over RP and denote by RBH, is analogous to the difference hierarchy for r.e. sets studied by Ershšv end to the Boolean hierarchy studied by sevarl authors. ,RBH lies above RP and below BPP. It is of particular interest because so little is known about sets that might be in BPP-RP. In fact, since Adleman and Huang showed that primality testing lies in RP, (and hence in ZPP), there have been no natural candicates for the class BPP-RP. Thus , the examples we give for the Boolena hierarchy over RP should help renew the belief that the classes BPP and RP are truly different.

73-90

Strong separation of the polynomial hierarchy with oracles : constructive separations by immune and simple sets
D. Bruschi
In this paper we show that the ideas introduced by Furst, Saxe and Sipser which connected oracle separation results for the relativized polynomial time hierarchy to the problrm of proving lower bounds for constant depth circuits, and subsequent probabilistic argument introduced by Yao, Hastad and Ko in order to prove the existence of relativized polynomial time hierarchies with different structures can be adapted for resolving the main problems related to the existence of immune and simple stes in the relativized polynomial time hierarchy. In particular we construct oracles which witness the existence of immune and simple sets in the k-th level of a relativized polynomial time hierarchy for kł1. In this way we refuse the conjecture of Torenvliet and van Emde de Boas about the impossibility of constructing oracles witnessing strong separations of the relativized polynomial time hierarchy for level higher than the second. Also we show that the existence of simple or immune sets in the relativized polynomial time hierarchy is not contradictory with a finite polynomial hierarchy. The results solves in a strong sense an open question posed by Ko. We further show oracles relative to which the polynomial time hierarchy is finite but its k-th level, for any given k>0, does not contain simple or immune sets. This results extends to the k-th level, kł1, of the relativized polynomial time hierarchy a results obtained by Homer and Maas for k=1.

72-90

About infinite traces
P. Bonizzoni, G. Mauri, G. Pighizzini
In this paper we generalized the notion of Foata normal form to the case of infinite traces. We show that this normal for is consistent with the notion of equivalence introduced by Gastin and Rozoy, in the sense that two infinite traces are equivalent if and only if they have some normal form. Finally, we use this notion to introduce a metric on the infinitary partially commutative monoid F ° (ˇ,) and whe show that the resulting metric space is complete

71-90

On automata on infinite trees
P. Bonizzoni, G. Mauri
In the paper, first of all, we analyze new conditions for acceptance of sets of infinite trees recognized by Muller automata and for which equivalent BŸchi automata can be given. We define a new model of infinite tree automata, called "limited Muler" automata, and investigate their characterization in weak monadic logic. In the secon part, we extend the notion of control automation to the case where more than one language is used to control the set of infinite words labelling each path of a successful run on a tree. We prove that using boolean operators in defining acceptance conditions for control automata, a characterization for M-automata, introduced by Nivat and Saoudi, and other classes of automata can be given. We introduce the "And-control" automation and use this notion to prove properties of boolean closure of deterministic classes of automata.

70-90

Universal combination of equational unification algorithms
E. Ciapessoni, G. Mauri
The problem of first order unification in equational theories obtained by combination of simpler theories is studied and a new method, called universal combination , is presented as a set of transformation rules which give a non deterministic algorithm. The universal combination algorithm generalizes the transformation rules for universal unification methods, such as general equational unification of lazy narrowing to the problem of combining unification algorithms. In particular, the paper shows that universal combination allows to construct unification algorithms for a subclass of equational theories, called layerable theories, which include theories not covered by previous methods.

69-90

Flowshop e TSP : un approccio con reti neuronali
F. Gardin, G. Mauri, M.P. Pensini

68-90

Some errors estimates for approximate shape identification methods applied to inverse acoustic scattering
G Crosta
With reference to the inverse problem of identifying the shape of a sound soft acoustic scatterer, given the incident plane wave, the scattered far field and some constraints on the unknown shape, we compare three methods of solution, two of which have already been described in the literature. The common feature is that each method approximately solves the inverse problem by minimising an objective function. Comparison consist of some inequalities and relationships, by which the values of the objective functions are expressed through some other computable quantities.

67-90

Parameter identification methods in mass and heat flow models: some analytical examples covering conductivity and storage coefficient
G Crosta
This paper provide a number of analytical examples portaining to the identification of some coefficients appearing in the differential equations, which describe mass and heat flow in various gemetries and circumstances. For any given (potential, source, term) pair, two different domains are considered, in one of which at least the unknown coefficient can be uniquely found. By means of these examples, the performance of coefficient identification method can be evaluated.

66-90

Ranking and formal power series
A. Bertoni, D. Bruschi, M. Goldwurm
In this paper we prowe that the ranking problem for unanbiguous context-free languages is -reducible to the value problem for algebraic formal power series in noncommuniting variables. In the particular case of regular language we show that the problem of ranking is -reducible to the problem of counting the number of strings of given lenght in suitable regular languages. As a consequence ranking problems for regular languages is - reducible to integer division and hence it is computable by long-space uniform boolean circuits of polynomial size and depth O (log n log log n), or by P-uniform boolean circuits of polynomial size and depth O (log n).

65-89

Esame delle possibilitˆ di progettazione automatica di dispositivi per la protezione degli errori
E. Angeleri, M. Bruschi, M. Goldwurm

64-89

The judgement calculus for intuitionistic linear logic : proof theory and semantics
S. Valentini
This paper propose a new set of rules for a judgement calculus for intuitionistic linear logic that makes easier to define a suitable mathematical semantics. A proof of the canonical form theorem for this new system is given: it assures, beside the consistency of the calculus, the termination of the evaluation of every well-typed program. The definition of the mathematical semantics and the completeness theorem, that turns out to be a representation theorem, follows. This semantics is the basis to obtain a semantics for the evaluation process of any well-typed program.

63-89

Evaluation of the number of prefixes of traces : an application to algorithm analysis
M. Goldwurm
In this work we summarize some probabilistic results concerning the evaluation of the number of prefix in free partially commutative monoids (f.p.c.m.). As an application of these results we give a probabilistic analysis of time and space complexity of a class of algorithms for problems on trace languages including the Membership Problem for regular trace languages. This class of algorithms has been introduced in [BGS] by means of a recursive procedure scheme and here we study an interactive version of that scheme.

62-89

Bounds for permanents and latin square
M. Torelli
Permanentes are difficult to compute, therefore upper and lower bounds are particularly interesting. Such bounds also have intrinsic interest, since they are difficult to prove, sometimes requiring rather sophisticated approaches, as is the case for the van der Waerden bound, which stayed unproved for more than half a century. Lower and upper bounds have been proved which are a strict for the general class of matrices, but are somewhat loose for (0,1)- matrices having k1's in each line. In the paper some stricted bounds are conjectured, and an inequality is proved, refining an inequality by Minc and Sathre, which demonstrates that the conjuctures upper bound is stricter than Bregman's. By applying these bounds to the enumeration of Latin squares one obtains bounds which e.g. delimit the number of normalized Latin squares order 10 between 8.50x and 3.3x.

61-89

The expression with arity
A. Botti, S. Valentini
In the formal rules of Martin Lof's type theory both types and their elements are denoted by expressions with ariry. The ability to handle expressions and to decide on their equality is a prerequisite to verify the correct applications of the rules of the theory. In this paper we present a formal system to derive expressions with arity, we prove the decidability of definitional equality and we give the conditions to develop a correct algorithm to parse expressions in the presence of abbreviatory definitions.

60-89

KBLab 1.0: manuale d'uso
G. Sanna

59-89

A typed calculus based on quantifier _free instuitionistic logic
S. Valentini
A judgement calculus for the propositional intuitionistic linear logic is introduced. This calculus defines the axiomatic semantics for a typed functional language for which a set of reduction rules is given. The normalization proof for the judgement calculus assures the determination of the valuation of every correct (i.e. well-typed) program.

58-89

Punti e co_punti in topologia formale
S. Valentini
After the introduction of the main ideas of formal topology, the paper analyses the notions of point and co-point. It first presents some methods to construct points and co-points in suitable formal topologies and then gives some applications of such constructions in logic.

57-89

Design and devolopment of ENprover, an automated theorem proving system based on EN-strategy
F. Baj, D. Bruschi, A. Zanzi
The design and the implementation of ENprover, an automated theorem proving system for first order theories with equality, are discussed. A summary of EN-strategy - the underlying method based on rewrite technique - the analysis of the basical activities, the definition of a theorem bank as a frame to collect theorems and tools to automate program testing are given. A discussion of the main aspects involved in the Prolog implementation of the system and the related algorithms analysis concludes the work.

56-89

A class of convolutional codes to correct burst errors
L. Mazzei
This work describes a class of convolutional codes for correction of single errors burst which extends a particular description of the well-known Iwadare codes, while for a different description it demostrates that there is always better code bolonging to the class defines here. The codes are described through a parametric form of the generating polynomials which, when appropriately selected, allows generation of codes particularly efficient in relation to the guard and constraint lenght. This characteristic is useful for the construction of coders and decoders of low circuital complexity.

55-89

A numerical implementation of "Quantum Annealing"
B. Apolloni, N. Cesa-Bianchi, D. De Falco
"Quantum Annealing", a variant of the Simulated Annealing algorithm, simulates the quantum tunnel effect to find approximate solutions to the problem of minimizing real function of boolean variables. More precisely, the procedure carries out a Markov chain whose equilibrium distribution is associated with the ground state wave function of a particular Schrodinger Hamiltonian. A numerical implementation of the algorithm is presented and some applications are discussed. Experimental results show that Quantum Annealing and Simulated Annealing are comparable in terms of their performances even though significative difference have been found in their detailed behaviour.

54-89

The connection constants problem
E. Damiani, O. D'Antona, G. Naldi, L. Paravicino
In this paper explicit formulas for the connection constants between sequences of polynomials in terms of their roots have derived. As an application, some properties about the inversion of triangular matrices have given. By means of the concept of punctured partion ao an integer, here introduced to compute connection constants, we also obtain a new expression of the relationship between elementary and complete homogeneous symmetric functions.

53-89

Un sistema di deduzione logica per dimostrazioni automatiche in geometria
M.A. Alberti, P. Ferrari, M. Torelli
We describe a knowledge based system to prove theorems in Euclidean geometry. The prover, written in Prolog, can deal with problems involving circles and inequalities, which are not treated in other similar provers, reviewed in the paper. Provers of this kind, that use a knowledge data base are usually much less efficient than provers based on algebraic mathods, but they provide a proof trace that can be read to users. Therefore they are more interesting for educational purposes. A specification language for problem description is implemented.

52-89

Quantum tunnelling in stochastics mechanics and combinatorial optimization
B. Apolloni, N. Cesa-Bianchi, D. De Falco
In the Schrodinger-Nelson dynamics of the real time, the ground state processes performs, in the semiclassical limit, a motion in which long sojourns around a global minimum of the potential are interrupted by rare large fluctiations which carry the process from one minimum to another. We motivate here a partial extention of the above analysis to the dynamics of the Heisenberg spin chain, in view of applications to the combinatorial optimization problem of finding the global minima of a real valued function of many boolean variables.

51-89

Some limit distributions in analysis of algorithms for problem
M. Guldwurm
This paper study the limit distribution of the sequence of random variables { } where, for each n, is the number of prefixes of a trace of lenght n chosen in a given free partially commutative monoid under the assuption that all representative strings of lenght n are equiprobable. We determine such a limit distribution for every free partially commutative monoid defined on a concurrence alphabet < ˇ, C > such that the complementary relation is transitive. This paper prove that if the complementary alphabet < ˇ, > has k connected component of equal size, then { } (suitably normalized) converges in distribution to a chi-square with k-1 degrees of freedom. On the other hand, if at least two components of < ˇ, > have different number of vertices, then { } (suitably normalized) converges in distribution of the time complexity of several algorithms for problems trace languages, including algorithms for the Membership Problem of regular context-free trace languages.

50-89

Dimostrazione automatica di teoremi
M.A. Alberti, E. Calzolari, M. Torelli
After a general introduction to automated theorem proving in geometry, some features of the algebraic proof methods are considered. Wu's method is examined in detail together with Chou's simplifications which enabled Chou to prove over 500 theorems in elementary geometry. The prover is implemented in MuMath, a symbolic manipulation system for PC's. In the conclusion some comparative remarks are made with proof methods which are based on Gršbner basis techniques.

49-89

Formal definition of reflective Prolog
S. Costantini
In this paper the formal syntax and semantics of Reflective Prolog is presented. Semantics is defined in a model-theoretic fashion; namely, a least model semantic is provided, based on definition of a concept of "least reflective Herbrand model" of theory. The least reflective Herbrand model is then characterized (similarly to the classical Horn-clause language semantics) as the fixpoint of a suitable mapping, in order to provide a link between the declarative and procedural semantics of a program. Derivation by resolution is extended to deal with metalevel aspects of the language. Extended resolution is then proved to be correct and complete.

48-89

Definizione dell'interprete riflessivo
G. Casaschi, S. Costantini
The approach of Smith's procedural reflection, originally introduced in the context of functional languages, has first been extended to horn-clauses in the language Logic, developed at the Computer Science Dep. of the University of Milan by R. Ghislanzoni ang G. Tornielli, supervisor Prof. G. Degli Antoni, co-supervisor L. Spampinato. Logic was implemented in Lisp, so as to exploit its higher-order features for level-shifting. In this report we show the implementation of Prolog plus procedural reflection (which is a wider language than Logic, since it also contain extra-logical and metalogical built-in predicates) in Prolog itself. In particular, we have defined a tail-recursive circular metaprocessor for the horn-clause langauge, then augmented with level-shifting capabilities. The built-in predicates of Prolog have been finally defined by procedural reflection itself.

47-89

Asynchronous automata: analysis of a category that admits infinitely many minimal objects
G. Pighizzini
This paper explains some propreties of asynchronous automata, introduced by Zielonka in order to characterize the class of recognizable subsets of free partially commutative monoid (recognizable trace languages). In this paper it is proved that there exists a trace language T recognizable by infinitely many minimal finite state asynchronous automata and by infinitely many minimal infine state asynchronous automata.

46-89

Area e lunghezza media dei dati nei layouts di grafi generici
F. Arcelli, P. Campana, M. Guldwurm
The layouts of graphs and planar grid is studied with respect to the Thompsonn's "VLSI model of computation" extented to general graphs. Total area accupied by wires and nodes and average lenght of wires are studied as measures to evaluate the layouts. These values are estimated by a new key parameter for graph w, which extends the idea of minimum bisection width. This paper proves that the local area occupied by layout is () and the wires have average lenght (/) where / is teh area required by wires and is their cardinality. These results are applied to well know architectures, i.e. hypercube and d-shuffle.

45-89

Comportamenti di una classe di schemi di computazione concorrenti
A. Bertoni, M. Guldwurm, G. Mauri, N. Sabadini

44-89

A note on -moves elimination in finite state automata
E. Damiani, O. D'Antona
This paper explains an algorithmic proof of the equivalence of nondeterministic finite state automata (NFSA) with and without -moves and briefly discuss an implementation of this algorithm. In the last section it is show that this construction can be used to compute the automaton recognizing the homomorphic image of a regular language.

43-89

A combinatorial proof of an elementary property of finite difference
O. D'Antona
Consider n+1 consecutive integers and their n-th powers. Compute the n differences of the powers. Compute the n-1 differences of the difference and so on. A basic fact of the Calculus of Finite Differences tells us that the n-fold repetition of this operation ends up with n!, the very same result one obtains when deriving n times the function . In this report it is given a new proof of this formula by exploiting the so called "ball-into-the-boxes" technique. This approach is also used to prove a simple identity related to Abel polynomials.

42-89

Counting functions and formal series in noncommuniting variables
A. Bertoni, G. Goldwurm, P. Massazza
This work explanes the complexity of certain counting problems defined by means of formal series in noncommunicating variable. The subject is related to classical problems of combinatorial enumeration and other topics of computational complexity. In particular Lagrance Inversion formulas are used to design fast parallel algorithms for these counting problems. The main results in that, for any ambiguous context-free language L, the problem of computing the number of words of lenght n in L is NC1-reducible to integer division.

41-88

Matroidi: teoria e applicazioni
S. Donatelli, U. Solitro

40-88

Some models of computation from a proof-theoretical point of view
A. Bertoni, G. Mauri, P. Miglioli, M. Ornaghi

39-88

Decision problems and evaluation problems in an abstract data type
A. Bertoni, G. Mauri, P. Miglioli, M. Ornaghi

38-88

CHAOS: il modulo GLE
C. Bignoli, G. Carenini, C. Simone
Chaos is a system supporting conversations between people inside an organization. Users exchange semi-structured messages whose propositional content can be expressed in natural language. The system must interprete it, in order to estract information to up data a representation of the organizational structure and individual's and group's agenda. The paper reports on the architecture of the linguistic module of CHAOS. In particular, deails are given of the "Dictionary" and of the "Integrator" components. The Dictionary holds an IS-A hierarchy of classes and istances representing entities of the domain; besides the IS-A relation, IS-PART and IS-PREC relations are defined among entities. The Integrator is used during the phase of semantic analysis of the language, to solve reference ambiguities, such DEFNPs, ellipsis, anaphora; it is based on the Grosz's notion of "focus of attention".

37-88

An improved refutation system for intuitionistic predicate logic
P. Miglioli, U. Moscato, M. Ornaghi

36-88

Progetto ALICE: definizione dell'integrazione
S. Costantini
This report concerns the integration of the functional and logic components of the Alice system. Former approaches to this kind of integration are presented, and the chosen one is discused in detailed, also in the perspective of future developments. On the basis of the resulting architecture of the Alice system, constructs for the predicate demo(T,G,), which declaratively represents the metatheoretical assertion of provability of the proposition G from theory T. New versions of demo are defined, suitable for performing hypothetical reasoning.

35-88

Progetto ALICE: evoluzione e sperimentazione
S. Costantini
In previous reports about the Alice project, we have discussed the state of the art with respect to introspection and reflection (with particular attention to procedural reflection), and we have introduced some new ideas about the features that a language oriented to the declarative description of knowledge and metaknowledge over several, related levels, should exhibit. A first result of the evolution of those ideas is presented in this report. In particular, a new logic programming language, called Reflective Prolog, has been (still incompletely) defined. We present this new language, with some examples of application. The implementation of the interpreter, that should be based on procedural reflection, is finally discussed.

34-88

Progetto ALICE: definizione della parte funzionale
S. Costantini
In this report, a definition of metasystem, introspective system and reflection principle are introduced, taking the main approaches inthe literature into account. The approach of Smith's procedural reflection, that has been taken as a basis for the functional component of the Alice system, is examined in detail. Finally, the problem of the potential applicability of reflective language is discussed.

33-88

L'voluzione di un libro elettronico
Le Van Huu
This paper represents the evolution of a research activity, began ten years ago at the Department of Information (Computer) Science, relating the electronic book topic. The research objective is to use the computer as a tool for reading and analysing texts. The paper outlines the problems and the basic concepts of a electronic book, presenting the evolution of some prototypes realized at the Department, from a sample text editor to an electronic enciclopedia.

32-88

On the properties of relations in Prolog and beyond
S. Costantini, G.A. Lanzarone
Problem arising in representation and use of general properties of binary relations (such as refelexivity, symmetry and transitivity) in Prolog programming are examined. Different possible solutions are presented within a logic programming approach; their advantages and disadvantages, in terms of expressivity of the achieved representation, and of the linguistic and metalinguistic tool necessary for their definition, are discussed. In conclusion, it is pointed out how similar problems arise nont only in Prolog, but in other formalisms as well, also in connection with different problems of knowledge and metaknowledge representation.

31-88

Constructive validity and classical truth to assign meaning to programs: extended version
P. Miglioli, U. Moscato, M. Ornaghi, G. Usberti

30-88

On the prefixes of a random trace and the membership problem for context-free trace languages
A. Bertoni, M. Guldwurm
In this paper we study the complexity of algorithms for problem on free partially commutative monoids (f.p.c.m.). These monoids are widely studied in literature and their properties are used in several research areas. The elements of f.p.c.m. and its subsets are respectively called traces and trace languages. We first present some probabilistic estimations of the number of prefixes of trace. The proof technique is based on the analysis of generating functions of particular languages and is related to classical combinatorial methods. Then we apply these probabilistic results to the analysis of algorithms for problem s on trace languages. In particular, we describe an algorithm for the Membership Problem of context-free trace languages and determine its tima complexity both in the worst and in average case, assuming that all the imput strings of given lenght have the same probability. Moreover, we also show that, with probability tending to 1, the time complexity of this algorithm has the same order of growth of its mean value.

29-88

Probabilistic estimation of the number of prefixes of a trace
M. Goldwurm
We present a generating function technique to evaluate the number of strings of given length recognized by a particular kind of finite state automation. Using this method we determine some asymptotic estimation of number of prefixes in free partially commutative monoids. These combinatorial serults allow to determine the probabilistic behaviour of some algorithms for problem trace language, including the Membership Problem for regular context-free trace languages.

28-88

Neural networks, concurrency and hierarchical data
A. Bertoni, D. Bruschi, P. Campadelli, N. Sabadini
In this paper we present some ideas developed in the framework of theory of concurrency and abstract data types. We discuss their interest in the modelling of neural nets.

27-88

Traces and semitraces: applications to movement
A. Bertoni, D. Bruschi, P. Campadelli, N. Sabadini
An interesting field of application of concepts derived from the theory of concurrency is given by biological systems. In fact, many biological behaviours, such as speech and movements, require coordinated "sequences" of events with high degree of internal parallelism to be performed. It has been observed by many authors that a theory of "serial order" in behaviour is required, since the current formalisms are inadequate to deal with parallel aspects of this behaviour. In this paper we apply the theory of traces and semitraces to describe the possible pattern that represent the various modes of quadruped locomotion.

26-88

The complexity of computing the numberb of strings of given lenght in context-free languages
A. Bertoni, M. Guldwurm, N. Sabadini
Computing the number of strings of given length contained in a language is related to classical poroblems of Combinatorics, Formal Languages and Computational Complexity. Here we study the complexity of this problem in the case of context-free languages. It is shown that, for unanbiguous context- free languages such a computation is "easy" and can be carried out by efficient parallel algorithms. On the contrary, for some context-free languages of ambiguity degree two, the problem becomes intractable. These results are related to other classical subjects concerning counting problems, exponential time recognizable language and sparse sets.

25-88

Semantical analysis of some (standard or non standard) intermediate propositional constructive logics: maximality and smoothness results
P. Miglioli, U. Moscato, M. Ornaghi, G. Usberti.

24-88

A theory of molecula structures in qualitative simulation
S. Bandini, G. Cattaneo, P. Stofella
The molocular onthology approach to the modelling of physical systems is presented as a general theory to define molecular structures in a universe of places endowed with adjacency relations. The computational model of the proposed "Molecular Onthology Theory" is used in qualitative simulation. The specific example of the qualitative modelling of the behaviour of liquids will be presented in a bidimensional universe with a privileged direction of falling.

23-88

LOGIC: un interprete Prolog con una relazione di uguaglianza
L. Benassi, M.P. Bonacina, G. Fiori

22-88

A typed calculus based on a fragment of linear logic
U. Solitro

21-88

ProTalk: man-machine symmetry in Prolog
W. Vannini
ProTalk is a Prolog-based Prolog programming system whose task is achieving full symmetry in man-machine communication. It creates an environment ahere user and computer share a common communication language. Each part can send and receive knowledge concerning the topic of the dialogue, thus incrementally developing a logic program. Such knowledge can either be expressed in intensive (rules) or extensive (facts) form. The system can manage distinct databases (theories), which may be in contradiction with each other. Open or closed world assumption can be used in database, according to user's specifications. Non-monotonic reasoning can be achieved either by switching from one database to another, or by adding knowledge to the current one.

20-88

Lectures on automated theorem
M.P. Bonacina
These notes report the contents of three lectures given by Prof. Jieh Hsiang at Department of Information (Computer) Science during the first week of September 1987. The firs lecture gives and overview of Knuth-Bendix completion follow ing the proof ordering approach. The second one focuses on Knuth-Bendix completion as a semidecision procedure and the third one presents some rewriting techniques for the resolution style theorem proving.

19-87

Progetto ALICE: definizione della parte funzionale
S. Costantini
With the aim of identifying a candidate formalism for the logic component of the Alice system, in this report the programming language Logic is presented and discussed. Logic is a hor-clause language with procedural reflection, developed at the Comlputer Science Dept. of the University of Milano by G. Ghislanzoni and G. Tornielli, supervisor prof. G. Degli Antoni, co- supervisor L. Spampinato. Some examples of use of this language are introduced, and problems related to the implementation of the interpreter are examined. The general topic of the role of reflection in Logic Programming is discussed, and the other possible extensions to the Horn-clause language are outlined, mainly aimed at commonsense-reasoning and Artificial Intelligence applications.

18-87

Rappresentazione di metaconoscenza nei testi legislativi
R. Bertocchi
Law texts contain statements reffering both to real world situations and the law itself. The latter type of norms express a kind of metaknowledge which is formalized in logic terms by means of a metalevel extension of horn clause. The integration of language and metalanguage enables a knowledge representation resembling the law text structure and it reduces the amount of rules to be represented.

17-87

Formalization of norms in horn clause logic
R. Bertocchi
The concepts of permission, obligation and prohibition are usually represented within a specialized deontic logic. In this paper it is developed an alternative approch based on Horn clause formalism: the meaning of a norm is expressed in term of the concepts of regulation, violation, sanction and recovery. The concepts are formalized by a set of axioms that relate the representation of the norms to the Event Calculus.

16-87

OBJSA net systems: a class of high-level nets having objects as domains
E. Battiston, F. De Cindio, G. Mauri
In this paper, we define a class of high-level Petri nets, namely OBJSA net system, in which:1) the net can be composed into state-machine components, i.e. it preserves the main caracteristics of Superposed Automata (SA); 2) the domains to which individual tokens belong are defined as abstract data types by using the language OBJ2. For this class of nets two products (namely an S-product and a T-product) are then provided for defining, respectively, the S- and T- invariants as the first step for preserving in the resulting specification language the possibility, typical of nets, of deriving properties of the modelled system by using algebraic techniques.

15-87

A theorem proving review for proof system based programming
M.P. Bonacina
This is a collection of tables intended to give an easy and quick consultant review about automatic theorem proving. The list of tables titles gives the review's contents:early forerunners, resolution based theorem proving, equality reasoning, something about negation, term rewriting based, equational reasoning, term rewriting based clausal theorem proving, term rewriting based theorem proving

13-87

Petri nets knowledge representation
M.P. Bonacina
In this paper a relationship between Petri nets and modal logic is investigated. The research starts at the basic level for both formalisms: condition-event interpretation for nets and propositional calculus for modal logic. Nets provides the fundamental notions of case reachability between cases, which are mapped into the corrisponding modal semantics notion of worlds or state and accessibility. In the framework settled by corrisponding modal logic mapples with anlogy , i.e. the study of nets' enlogic structure. Enlogy plays such a fondamental role in general net theory foundations that being able to capture enlogic structure by modal propositions lets the choiche of modal logic look very promising.14-87First results of parallel execution of sequential programs through communications o partial evaluationsby M.P. Bonacina 9The basic definition of a mixed and partial computation are rephrased and compared; next some of their applications are presented in a concise and coherent formalism. Finally partial evaluation of Prolog programs is viewed as theories specialisation and mixed computation is applied to the concurrent processing of approximate data.

12-87

An implementation of Knuth-Bendix algorithm
M.P. Bonacina
This is a report of an implementation of the Knuth-Bendix algorithm realized by the autor in C language on a Macintosh at the Department of Information (Computer) Science. The main concepts underlying the algorithm are briefly sketched through the description of the implementation, oriented to give the user a feeling of wath he or she can do with the program. For this purpose a rich set of examples of runs is given. Finally the references provide suggestions to the reader interested in knowing more about algorithm.

11-87

Data-flow Knuth-Bendix algorithm as inferential engine on term rewriting systems
M.P. Bonacina
Historical remarks and basic definitions about Knuth-Bendix algorithm open this paper. The algorithms is presented as an inferential engine working on term rewriting systems and a survey of its applications and extension is given. A data flow Knuth-Bendix machine is speciefied through a top-down modular analysis. In the appendix and early forerunner of Knuth-Bendix algorithm is presented as a guarded command algorithm.

10-86

TeX TRA: un linguaggio per passare da Nroff a TeX
L. Mazzei
This work presents an experimental system for text translation from Nroff, the UNIX tex formatter, to TeX. The object is pursued by rendering the effects, i.e. the semantics; of Nroff commands by means of a specification language instead of verbatim translating commands or macros.

9-86

A language to describe formatting directives for SGML documents
Le Van Huu, E. Tirreni
SGML is a standard proposed by ISO for documents description based on generalized markup technique. The formatting process of a SGML document could consist in singling out markup elements and inserting formatting directives into the document in accordance with the class of the markup elements themselves, using a suitable map table. This paper will present an implementation of an environment of SGML documents production, emphasizing a special language, METAFONT, for the map table construction.

8-86

L'algoritmo di Knuth-Bendix come motore inferenziale di sistemi di riscrittura
M.P.Bonacina

7-86

Presentazione dell'algoritmo di Knuth-Bendix
M.P.Bonacina

6-86

Problemi di standardizzazione SGML e TeX
Le Van Huu

5-86

L'evoluzione di text processing vista attraverso STPL (Standard Text Processing Languages)
Le Van Huu
STPL is a component of the ISO Project called CLPT (Computer Language Processing Text), oriented to defined standars relating to languages and functionality for text processing activity, as defining the logical and physical text structure, editing, formatting, storing and retriving, interchanging of documents. In this paper we will present some of important STPL aspects and analyse its main components, with emphasis on the standard SGML (Standard Generalized Markup Language), a declarative markup language which provides a coherent and unambiguous sysntax for describing document elements.

4-86

TeX and ISO/STPL standard
Le Van Huu
This paper examines the most important STPL aspects and makes a comparison with those of TeX. An attempt to answering the question whether TeX could be integrated with STPL is also included.

3-86

Control model and management of a polluted aquifer
G. Crosta, D. Marini
In this papers we apply system theoretical methods to the modeling and management of the Milano aquifer, which is pollued by halocarbon compounds. The system we are dealing with is diveided into three main subsystems:1) the aquifer itself; 2) the water distribution networks; 3) the end users.Available data are declared to each physical process and worked at by some method, which allows the unknown model parameters to be identified. A data base is being created which shall contain all available hydrogeological information. Computer programs we have developed allow queries about all kinds of data. Application package have been written, which can be used also by non-computer experts. We have thus to model a system which is complex, as all environmental system are, and to design optimal control strategies.

2-86

Relazione finale dell'obiettivo METOD
M.Maiocchi

1-86

Funzione base di SFAX: una Software Factory su UNIX
G.Castelli, M. Maiocchi