Crypt-equivalent algebraic specifications

Summary Equivalence is a fundamental notion for the semantic analysis of algebraic specifications. In this paper the notion of crypt-equivalence is introduced and studied w.r.t. two loose approaches to the semantics of an algebraic specification T: the class of all first-order models of T and the class of all term-generated models of T. Two specifications are called crypt-equivalent if for one specification there exists a predicate logic formula which implicitly defines an expansion (by new functions) of every model of that specification in such a way that the expansion (after forgetting unnecessary functions) is homologous to a model of the other specification, and if vice versa there exists another predicate logic formula with the same properties for the other specification. We speak of first-order crypt-equivalence if this holds for all first-order models, and of inductive crypt-equivalence if this holds for all term-generated models. Characterizations and structural properties of these notions are studied. In particular, it is shown that first order crypt-equivalence is equivalent to the existence of explicit definitions and that in case of positive definability two first-order crypt-equivalent specifications admit the same categories of models and homomorphisms. Similarly, two specifications which are inductively crypt-equivalent via sufficiently complete implicit definitions determine the same associated categories. Moreover, crypt-equivalence is compared with other notions of equivalence for algebraic specifications: in particular, it is shown that first-order cryptequivalence is strictly coarser than abstract semantic equivalence and that inductive crypt-equivalence is strictly finer than inductive simulation equivalence and implementation equivalence.     

Adding a temporal dimension to a logic system

We introduce a methodology whereby an arbitrary logic system L can be enriched with temporal features to create a new system T(L). The new system is constructed by combining L with a pure propositional temporal logic T (such as linear temporal logic with Since and Until) in a special way. We refer to this method as adding a temporal dimension to L or just temporalising L. We show that the logic system T(L) preserves several properties of the original temporal logic like soundness, completeness, decidability, conservativeness and separation over linear flows of time. We then focus on the temporalisation of first-order logic, and a comparison is make with other first-order approaches to the handling of time.     

The Kreisel length-of-proof problem

A first-order system F has theKreisel length-of-proof property if the following statement is true for all formulas(x): If there is ak1 such that for alln0 there is a proof of(¯n) in F with at mostk lines, then there is a proof of x(x) in F. We consider this property for Parikh systems, which are first-order axiomatic systems that contain a finite number of axiom schemata (including individual axioms) and a finite number of rules of inference. We prove that any usual Parikh system formulation of Peano arithmetic has the Kreisel length-of-proof property if the underlying logic of the system is formulated without a schema for universal instantiation in either one of two ways. (In one way, the formula to be instantiated is built up in steps, and in the other way, the term to be substituted is built up in steps.) Our method of proof uses techniques and ideas from unification theory.     

Top-down development of layered fault tolerant systems and its problems — a deontic perspective

Although the top-down development paradigm has successfully been applied to master the complexity of large systems, it has not yet been accepted as a useful paradigm for fault tolerant system design. This is mainly due to a problem that is sometimes referred to as the lazy programmers paradox. The lazy programmer paradox was already present and solved in top-down development methods for non-critical systems. However, the problem has re-appeared in an even more serious variant for critical systems. A few toy examples concerning exception handling in an Ada-like language are used to explain and illustrate the paradox. One possible solution to the problem is to use a specification language in which one can express that certain behaviours of a system are preferred over others. This paper proposes deontic logic as such a specification language. Therefore, a short and rather informal introduction to deontic logic is included. A non-trivial example is included to illustrate how deontic logic can be used to solve the lazy programmer paradox.Supported by NWO/SION Project 612-316-022: Fault Tolerance: Paradigms, Models, Logics, Construction.     

Finite Presentations of Infinite Structures: Automata and Interpretations

We study definability problems and algorithmic issues for infinite structures that are finitely presented. After a brief overview over different classes of finitely presentable structures, we focus on structures presented by automata or by model-theoretic interpretations. These two ways of presenting a structure are related. Indeed, a structure is automatic if, and only if, it is first-order interpretable in an appropriate expansion of Presburger arithmetic or, equivalently, in the infinite binary tree with prefix order and equal length predicate. Similar results hold for -automatic structures and appropriate expansions of the real ordered group. We also discuss the relationship to automatic groups. The model checking problem for FO(), first-order logic extended by the quantifier there are infinitely many, is proved to be decidable for automatic and -automatic structures. Further, the complexity for various fragments of first-order logic is determined. On the other hand, several important properties not expressible in FO, such as isomorphism or connectedness, turn out to be undecidable for automatic structures. Finally, we investigate methods for proving that a structure does not admit an automatic presentation, and we establish that the class of automatic structures is closed under Feferman–Vaught-like products.     

Modal Logic over Finite Structures

We investigate properties of propositional modal logic over the classof finite structures. In particular, we show that certain knownpreservation theorems remain true over this class. We prove that aclass of finite models is defined by a first-order sentence and closedunder bisimulations if and only if it is definable by a modal formula.We also prove that a class of finite models defined by a modal formulais closed under extensions if and only if it is defined by a -modal formula.     

Parallelism in Deductive Inference on Graph Structures

Practical realization of the methods of parallel inference on connection graphs and semantic networks in the first-order predicate logic is described. A system of parallel inference with the steamroller test is studied and inference results are analyzed.     

Generalized finite automata theory with an application to a decision problem of second-order logic

Many of the important concepts and results of conventional finite automata theory are developed for a generalization in which finite algebras take the place of finite automata. The standard closure theorems are proved for the class of sets recognizable by finite algebras, and a generalization of Kleene's regularity theory is presented. The theorems of the generalized theory are then applied to obtain a positive solution to a decision problem of second-order logic.     

Expressibility of output equals input

We examine the common and seemingly simple specification that the output stream equals the input stream. We show that this is not in full generality expressible in first-order or temporal logic by an infinite set of sentences or a recursive specification, but requires certain extra assumptions, such as the existence of a clock or discrete input values.The main negative results are stated for first-order expressibility and have direct corollaries for inexpressibility in first-order temporal logic: output equals input with arbitrary delay is not expressible by a (perhaps infinite) theory (Theorems 2 and 3), even with a timestamp (Theorem 8), and is not expressible for an timeline by a sentence, even with a timestamp (Theorem 10). Output equals input with constant delay cannot be expressed for timeline by a sentence with extra unary predicates over the timeline.As an example of the positive results, we show output equals input can be expressed by a sentence in the language with a (weak) clock if the base model contains either an extra function (Theorem 14), or arithmetic (Theorem 15).Supported by Aerospace Sponsored Research     

Proof Reflection in Coq

We formalize natural deduction for first-order logic in the proof assistant Coq, using de Bruijn indices for variable binding. The main judgment we model is of the form d[:], stating that d is a proof term of formula under hypotheses it can be viewed as a typing relation by the Curry–Howard isomorphism. This relation is proved sound with respect to Coq's native logic and is amenable to the manipulation of formulas and of derivations. As an illustration, we define a reduction relation on proof terms with permutative conversions and prove the property of subject reduction.     

A logic for the specification and proof of regular controllable processes of CCS

Summary This work has been motivated by the following general problem: find logics for the specification and proof of programs, described by terms of some algebra with given congruence relation. This relation is supposed to define a satisfactory concept for the behavioural comparison of programs. We require these logics to be adequate with respect to the term language, in the sense that two programs, behaviourally equivalent satisfy the same formulas and conversely. The term language considered is the subset of controllable, regular terms of CCS, on a vocabulary of actions A, with observational congruence. A term is said to be controllable if it is congruent to some term without occurrence of . We obtain an adequate logic whose language of formulas is obtained from constants true, false and ¦Nil¦ by using operators , , fixpoint operators, + and a for aA; the latter can be considered as extensions of the operators + and a for aA of CCS. As a result, controllable CCS terms can be considered as formulas of this logic and the problem of program verification is reduced to the proof of the validity of a formula.     

Near-Horn Prolog and the ancestry family of procedures

The near-Horn Prolog procedures have been proposed as effective procedures in the area of disjunctive logic programming, an extension of logic programming to the (first-order) non-Horn clause domain. In this paper, we show that these case-analysis based procedures may be viewed as members of a class of procedures called the ancestry family, which also includes Model Elimination (and its variants), the Positive Refinement of Model Elimination, and SLWV-resolution. The common feature which binds these procedures is the extension of SLD-resolution to full first-order logic with the addition of an ancestor cancellation rule. Procedures in the ancestry family are all sound and complete first-order procedures that can be seen to vary along three parameters: (1) the number of clause contrapositives required, (2) the amount of ancestor checking that must occur, and (3) the use (if any) of a Restart rule. Using a sequent-style presentation format for all procedures, we highlight the close relationships among these procedures and compare their relative advantage.This research was partially supported by NSF Grants CCR-8900383 and CCR-9116203.     

Automated Deduction Techniques for the Management of Personalized Documents

This work is about a real-world application of automated deduction. The application is the management of documents (such as mathematical textbooks) as they occur in a readily available tool. In this Slicing Information Technology tool, documents are decomposed (sliced) into small units. A particular application task is to assemble a new document from such units in a selective way, based on the user's current interest and knowledge. It is argued that this task can be naturally expressed through logic, and that automated deduction technology can be exploited for solving it. More precisely, we rely on first-order clausal logic with some default negation principle, and we propose a model computation theorem prover as a suitable deduction mechanism. Beyond solving the task at hand as such, with this work we contribute to the quest for arguments in favor of automated deduction techniques in the real world. Also, we argue why we think that automated deduction techniques are the best choice here.     

Logic Control and “Reactive” Systems: Algorithmization and Programming

Algorithmization and programming principles for logic control and reactive systems are formulated, regarding algorithms and programs as finite automata. The application of finite automata to programming for other problems is also reviewed.     

Observational implementation of algebraic specifications

Summary An observational approach to the construction of implementations of algebraic specifications is presented. Based on the theory of observational specifications an implementation relation is defined which formalizes the intuitive idea that an implementation is correct if it produces correct observable output. To be useful in practice proof theoretic criteria for observational implementations are provided and a proof technique (called context induction) for the verification of implementation relations is presented. As an example an abstract specification of (the algebraic semantics of) a small imperative programming language is implemented by a state oriented specification of the language.In order to support the modular construction of implementations the approach is extended to parameterized observational specifications. Based on the notion of observable parameter context a proof theoretic criterion for parametrized observational implementations is presented and it is shown that under appropriate conditions observational implementations compose horizontally. The given implementation criteria are applied to examples.     

Algebraic and functional specification of an interactive serializable database interface

Summary A formal functional specification of a serializable interface for an interactive database is given and refined into two different versions with distinct strategies for solving read/write conflicts. The formalization is based on techniques of algebraic specification for defining the basic data structures and functional system specification by streams and stream processing functions for defining the properties concerning interaction. It is especially demonstrated how different specification techniques can be used side by side. Manfred Broy finished his studies with the Diplom in Mathematics and Computer Science at the Technical University of Munich. Till 1983 he was research and teaching assistant at the Institut für Informatik and the Sonderforschungsbereich 49 Programmiertechnik. At the Technical University of Munich he also did his Ph.D. (in February 1980 with the subject: Transformation parallel ablaufender Programme) and qualified as an university lecturer (in 1982 with the subject: A Theory for Nondeterminism, Parallelism, Communication and Concurrency). In April 1983 he became a Full Professor for Computer Science at the Faculty of Mathematics and Computer Science at the University of Passau. Since October 1989 he has been Full Professor for Computer Science at the Technical University of Munich. His fields of interests are: Programming languages, program development, programming methodology and distributed systems.This work was supported by the DFG Project Transformation paralleler Programme and by the Sonderforschungsbereich 342 Werkzeuge und Methoden für die Nutzung paralleler Architekturen     

Proof strategies in linear logic

Linear logic, introduced by J.-Y. Girard, is a refinement of classical logic providing means for controlling the allocation of resources. It has aroused considerable interest from both proof theorists and computer scientists. In this paper we investigate methods for automated theorem proving in propositional linear logic. Both the bottom-up (tableaux) and top-down (resolution) proof strategies are analyzed. Various modifications of sequent rules and efficient search strategies are presented along with the experiments performed with the implemented theorem provers.     

Practical Handling of Exception-Tainted Rules and Independence Information in Possibilistic Logic

This paper provides a survey of possibilistic logic as a simple and efficient tool for handling nonmonotonic reasoning, with some emphasis on algorithmic issues. In our previous works, two well-known nonmonotonic systems have been encoded in the possibility theory framework: the preferential inference based on System P, and the rational closure inference proposed by Lehmann and Magidor which relies on System P augmented with a rational monotony postulate. System P is known to provide reasonable but very cautious conclusions, and in particular, preferential inference is blocked by the presence of irrelevant properties. When using Lehmann's rational closure, the inference machinery, which is then more productive, may still remain too cautious, or on the contrary, provide counter -intuitive conclusions. The paper proposes an approach to overcome the cautiousness of System P and the problems encountered by the rational closure inference. This approach takes advantage of (contextual) independence assumptions of the form: the fact that is true (or is false) does not affect the validity of the rule normally if then . The modelling of such independence assumptions is discussed in the possibilistic framework. Moreover, we show that when a counter-intuitive conclusion of a set of defaults can be inferred, it is always possible to repair the set of defaults by adding suitable information so as to produce the desired conclusions and block unsuitable ones.