=ADD=
=reftype=
14
=number=
97-16
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/1997/97-16.ps.gz
=note=
PhD Thesis
=sponsor=
{\"O}AD,PARAGRAPH (Parallel Computer Graphics), 
MEDLAR II (ESPRIT Basic Research Project, nr. 6471, FWF), PfoFactor.  
=year=
1997
=author=
Sofronie-Stokkermans; Viorica
=title=
Fibered Structures in Computer Science and Applications to Automated Theorem Proving in Certain Classes of Finitely-Valued Logics and to Modeling Interacting Systems
=month=
03
=keywords=
automated theorem proving, non-classical logics, SHn-logics, universal algebra,
Priestley duality, fiberings, sheaves.
=abstract=
The goal of this thesis is to study the applications of 
{\em fibered structures} in computer science, more precisely 
in automated theorem proving in many-valued logics, 
and in modeling cooperating systems. 
We  present and study situations in which fibered structures and sheaves 
(possibly with respect to Grothendieck topologies on certain categories) 
arise. 

The thesis contains two main directions of work, strongly interrelated:

The first direction of work is concerned with finding 
{\em decompositions} of given structures in terms of 
simpler structures, in such a way that certain classes of properties of 
the given structure can be reduced to properties of the simpler structures.
The  main contribution in this direction of work 
concerns Priestley-type representation of
distributive lattices with operators, and its application for
reducing the complexity of 
automated theorem proving in classes of 
finitely-valued logics. 
These methods are first discussed for the case of $SHn$-logics and 
then extended to more general classes of logics. An implementation
in Prolog is given and comparisons with related approaches are made.

The second direction of work is concerned with {\em putting together}
(interconnecting) different structures and studying the properties of the 
result of this interconnection; in particular with studying the link 
between the properties 
of the component parts and the result of their interconnection.
We give a sheaf-theoretic approach to the study of concurrency.
In studying complex systems consisting of several interconnected 
``agents'', given a class of agents (a description of every agent, and 
a description of the  way they interact) it is often necessary to 
study the properties of the system obtained by the 
interconnection of the agents in this class. 
We propose a notion of {\em system} and several variants 
of a corresponding notion of morphism, depending on the extent
of the relationship between systems that we want to express. 
We define Grothendieck topologies on the categories defined this way, 
that express ``covering relationships'' between systems.
It turns out that much of the information relevant for expressing 
properties about systems can be 
expressed by sheaves with respect to these Grothendieck topologies: 
for instance states and parallel actions are modeled by 
sheaves $St, Act$; transitions are expressed by 
a subsheaf of $Act \times St \times St$;
and 
behavior over a fixed range of time (of the form $\{ 0, 1, \dots, n \}, 
n \in {\Bbb N}$ or ${\Bbb N}$)
can be modeled as a sheaf 
too.
We use geometric logic in order to explain the link between 
certain properties of a given family of 
interconnected systems and
the properties of the system that results from their interconnection.
=location=
2
=owner=
2
=source=
3