Why Horn formulas matter in computer science: initial structures and generic examples. (English) Zbl 0619.68029
See the review of the preliminary version in Lect. Notes Comput. Sci. 185, 374-387 (1985; Zbl 0563.68013).
Citations:
Zbl 0563.68013References:
| [1] | Goguen, J. A.; Thatcher, J. W.; Wagner, E. G.; Wright, J. B., Abstract data types as initial algebras and the correctness of data representations, (Proceedings, Conf. on Computer Graphics, Pattern Recognition and Data Structures (1975)), 89-93 |
| [2] | Andreka, H.; Nemeti, I., The generalized completeness of Horn predicate-logic as a programming language, Acta Cybern., 4, No. 1, 3-10 (1978) · Zbl 0496.68021 |
| [3] | Börger, E., Decision problems in predicate logic, (Lolli, G.; Longo, G.; Marcja, A., Logic Colloquium ’82 (1984), North-Holland: North-Holland Amsterdam), 263-302 · Zbl 0556.03012 |
| [4] | Chang, C. C.; Keisler, H. J., Model Theory (1973), North-Holland: North-Holland Amsterdam · Zbl 0276.02032 |
| [5] | De Carvalho, R. L.; Maibaum, T. S.E.; Pequeno, T. H.C.; Pereda, A. A.; Veloso, P. A.S., A Model Theoretic Approach to the Theory of Abstract Data Types and Data Structures, (Research Report CS-80-22 (1980), Waterloo: Waterloo Ontario) |
| [6] | Chandrasekaran, B.; Radicchi, S., Computer Program Testing (1981), North-Holland: North-Holland Amsterdam · Zbl 0486.68005 |
| [7] | Colmerauer, A., Equations and inequations on fihite and infinite trees, (Proceedings, 2nd Internat. Conf on Fifth Generation Computer Systems. Proceedings, 2nd Internat. Conf on Fifth Generation Computer Systems, Tokyo (November 1984)), 85-99 · Zbl 0577.68001 |
| [8] | Degano, P.; Sirovich, F., An evaluation based theorem prover, IEEE Trans. Pattern Analysis and Machine Intelligence, 7, 70-79 (1985) · Zbl 0566.68075 |
| [9] | Davis, M. D.; Weynker, E. J., A formal notion of program-based test date adequacy, Inform. Comr., 56, 52-71 (1983) · Zbl 0537.68025 |
| [10] | Fagin, R., Horn clauses and data base dependencies, J. Assoc. Comput. Mach., 29, 252-285 (1982) |
| [11] | Goguen, J. A.; Burstall, R. M., Institutions: Abstract model theory for computer science, (Clarke, E.; Kozen, D., Proceedings, Logic Programming Workshop. Proceedings, Logic Programming Workshop, Lect. Notes in Comput. Sci., Vol. 164 (1984), Springer: Springer New York), 221-256 · Zbl 0543.68021 |
| [12] | Henschen, L.; Wos, L., Unit refutations and Horn sets, J. Asoc. Comput. Mach., 21, No. 4, 590-605 (1974) · Zbl 0296.68093 |
| [13] | Kreisel, G.; Krivine, J. L., Elements de logique mathématique (1966), Dunod: Dunod Paris · Zbl 0146.00703 |
| [14] | McKinsey, J. C.C., The decision problem for some classes of sentences without quantifiers, J. Symbolic Logic, 8, 61-76 (1943) · Zbl 0063.03864 |
| [15] | Mal’cev, A., Quasi primitive classes of abstract algebras, (The Metamathematics of Algebraic Systems, Collected Papers of A. I. Mal’cev (1971), North-Holland: North-Holland Amsterdam), 27-31 |
| [16] | Mahr, B.; Makowsky, J. A., Characterizing specification languages which admit initial semantics, (Proceedings, 8th CAAP. Proceedings, 8th CAAP, Lect. Notes in Comput. Sci., Vol. 159 (1983), Springer: Springer New York), 300-316 · Zbl 0522.68026 |
| [17] | Makowsky, J. A.; Vardi, M. Y., On the expressive power of data dependencies, Acta Inform. 23, 71-87 (1986) · Zbl 0617.68085 |
| [18] | Makowsky, J. A., Model theoretic issues in Computer science. Part I. Relational data bases and abstract data types, (Lolli, G.; Longo, G.; Marcja, A., Logic Colloquium ’82 (1984), North-Holland: North-Holland Amsterdam), 303-344 · Zbl 0553.68028 |
| [19] | Makowsky, J. A., Mathematical Foundations of Software Development, (Ehrig, H.; etal., Proceedings, International Joint Conference on Theory and Practice of Software Development (TAPSOFT). Proceedings, International Joint Conference on Theory and Practice of Software Development (TAPSOFT), Lect. Notes in Comput. Sci., Vol. 185 (1985), Springer: Springer New York), 374-387, extended abstract · Zbl 1099.03009 |
| [20] | Mostowski, A., Review of [Mal56], J. Symbolic Logic, 24, 57 (1959) |
| [21] | Rabin, M., Characterization of convex systems of axioms, Notices Amer. Math. Soc., 565-571, 505 (1960), Abstract |
| [22] | Rabin, M., Classes of models and sets of sentences with the intersection property, Ann. Fac. Sci. Univ. Clermont, 7, No. 1, 39-53 (1962) |
| [23] | Reiter, R., On closed world data bases, (Gallaire, H.; Minker, J., Logic and Data Bases (1978), Plenum: Plenum New York), 55-76 |
| [24] | Robinson, A., (Introduction to Model Theory and the Metamathematics of Algebra (1963), NorthHolland: NorthHolland Amsterdam) · Zbl 0118.25302 |
| [25] | Scholz, H.; Hasenjaeger, G., Grundzuege der mathematischen Logik (1961), Springer: Springer Berlin · Zbl 0137.00401 |
| [26] | Smorynski, C., Lectures on non-standard models of arithmetic, (Lolli, G.; Longo, G.; Marcja, A., Logic Colloquium ’82 (1984), North-Holland: North-Holland Amsterdam), 1-70 · Zbl 0663.03049 |
| [27] | Strassen, V., Polynomials with rational coefficients which are hard to compute, SIAM J. Comput., 3, No. 2, 128-149 (1974) · Zbl 0289.68018 |
| [28] | Tarski, A., Some notions and methods on the borderline of algebra and metamathematics, (Proceedings, Int. Congr. of Math., Cambridge, MA, Vol. 1 (1952), Amer. Math. Soc: Amer. Math. Soc Providence, R.I), 705-720 · Zbl 0049.00702 |
| [29] | Tarlecki, A., Free constructions in abstract algebraic institutions, draft (February 1984) |
| [30] | Tarnlund, S. A., Horn clause computability, BIT, 17 (1977) · Zbl 0359.02042 |
| [31] | Volger, H., On Theories Which Admit Initial Structures, (FNS-Bericht 85-1 (1985), Universität Tübingen) |
| [32] | Wu, W.-T., On the decision problem and the mechanization of theorem proving in elementary geometry, (Contemp. Math., Vol. 29 (1983), Amer. Math. Soc: Amer. Math. Soc Providence, R.I), 235-242 · Zbl 0578.68078 |
| [33] | Zloof, M. M., Office-by-example: A business language that unifies data and word processing and electronic mail, IBM Systems J., 21, No. 3, 272-304 (1982) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
