Name
Title | ||
|---|---|---|
On the Smooth Calculation of Relational Recursive Expressions out of First-Order Non-Constructive Specifications Involving Quantifiers |
Abstract | ||
|---|---|---|
The work presented here has its focus on the formal construction of programs out of non-constructive specifications involving quantifiers. This is accomplished by means of an extended abstract algebra of relations whose expressive power is shown to encompass that of first-order logic. Our extension was devised for tackling the classic issue of lack of expressiveness of abstract relational algebras first stated by Tarski and later formally treated by Maddux, Németi, etc. First we compare our extension with classic approaches to expressiveness and our axiomatization with modern approaches to products. Then, we introduce some non-fundamental operations. One of them, the relational implication, is shown to have heavy heuristic significance both in the statement of Galois connections for expressing relational counterparts for universally quantified sentences and for dealing with them. In the last sections we present two smooth program derivations based on the theoretical framework introduced previously. |
Year | DOI | Venue |
|---|---|---|
1993 | 10.1007/BFb0039715 | Formal Methods in Programming and Their Applications |
Keywords | Field | DocType |
smooth calculation,relational recursive,first-order non-constructive,first order logic,first order,expressive power,program derivation,relation algebra | Galois connection,Heuristic,Expression (mathematics),Algebra,Existential quantification,Computer science,Constructive,Algorithm,Theoretical computer science,Abstract algebra,Relational algebra,Recursion | Conference |
ISBN | Citations | PageRank |
3-540-57316-X | 10 | 1.29 |
References | Authors | |
7 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Armando Martin Haeberer | 1 | 81 | 11.05 |
| Gabriel Baum | 2 | 50 | 14.69 |
| Gunther Schmidt | 3 | 33 | 8.09 |