Search

Graph normal form, introduced earlier for propositional logic, is shown to be a normal form also for first-order logic. It allows to view syntax of theories as digraphs, while their semantics as kernels of these digraphs. Graphs are particularly well suited for studying circularity, and we provide some general means for verifying that circular or apparently circular extensions are conservative. Traditional syntactic means of ensuring conservativity, like definitional extensions or positive occurrences guaranteeing exsitence of fixed points, emerge as special cases. [ABSTRACT FROM AUTHOR]

The article focuses on algebraic approaches to nondeterminism. Nondeterminism works with values, functions, sets and relations. In computing science, however, nondeterminism has been an issue from the very beginning, if only in the form of nondeterministic Turing machines or nondeterministic finite state machines. A great variety of theories and formalisms dealing with it have been developed during the last two decades. Nondeterminism arises in a natural way when discussing concurrency and models of concurrency typically also model nondeterminism. There are numerous variants of process languages and algebra, event structures, state transition systems. In terms of modeling, nondeterminism may be considered a purely operational notion. However, one of the main reasons for considering nondetermrnism in computer science is the need for abstraction, allowing one to disregard irrelevant aspects of actual computations. The nondeterminism of concurrent systems usually arises as an abstraction of time. Similarly nondeterminism is also a means of increasing the level of abstraction when describing sequential programs.