×

zbMATH — the first resource for mathematics

Herbrand theorems in arbitrary institutions. (English) Zbl 1178.68132
Summary: The basic logic programming semantic concepts, query, solutions, solution forms, and the fundamental results such as Herbrand theorems, are developed over any logical system, formalised as institution, by employing ‘institution-independent’ concepts of variable, substitution, quantifier, and atomic formulae. This sets semantical foundations for a uniform development of logic programming over a large variety of computing science logics, allowing for a clean combination of logic programming with other computing paradigms.
Reviewer: Reviewer (Berlin)

MSC:
68N17 Logic programming
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
CASL
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Goguen, J.; Burstall, R., Institutions: abstract model theory for specification and programming, J. ACM, 39, 1, 95-146, (1992) · Zbl 0799.68134
[2] Sannella, D.; Tarlecki, A., Specifications in an arbitrary institution, (), 76, 165-210, (1988), earlier version · Zbl 0654.68017
[3] Astesiano, E.; Bidoit, M.; Kirchner, H.; Krieg-Brückner, B.; Mosses, P.; Sannella, D.; Tarlecki, A., CASL: the common algebraic specification language, Theoret. comput. sci., 286, 2, 153-196, (2002) · Zbl 1061.68103
[4] Meseguer, J., A logical theory of concurrent objects and its realization in the maude language, ()
[5] Diaconescu, R.; Futatsugi, K., Logical foundations of cafeobj, Theoret. comput. sci., 285, 289-318, (2002) · Zbl 1001.68079
[6] Diaconescu, R.; Futatsugi, K., Behavioural coherence in object-oriented algebraic specification, Universal comput. sci., 6, 1, 74-96, (2000), first version appeared as JAIST Technical Report IS-RR-98-0017F, June 1998 · Zbl 0963.68104
[7] Goguen, J.; Roşu, G., Hiding more of hidden algebra, (), 1704-1719 · Zbl 0953.68094
[8] Hennicker, R.; Bidoit, M., Observational logic, (), 263-277
[9] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoret. comput. sci., 96, 1, 73-155, (1992) · Zbl 0758.68043
[10] Lloyd, J., Foundations of logic programming, (1988), Springer Berlin · Zbl 0547.68005
[11] O’Donnell, M.J., Computing in systems described by equations, Lecture notes in computer science, vol. 58, (1977), Springer Berlin · Zbl 0421.68038
[12] Goguen, J.; Meseguer, J., Eqlog: equality, types, and generic modules for logic programming, (), J. logic programming, 1, 2, 179-210, (1984), an earlier version appears · Zbl 0575.68091
[13] Goguen, J.; Meseguer, J., Models and equality for logical programming, (), 1-22
[14] Goguen, J.; Malcolm, G.; Kemp, T., A hidden Herbrand theorem: combining the object, logic and functional paradigms, J. logic algebraic programming, 51, 1, 1-41, (2002) · Zbl 1012.03041
[15] Diaconescu, R., Institution-independent ultraproducts, Fund. inform., 55, 3-4, 321-348, (2003) · Zbl 1036.03055
[16] Orejas, F.; Pino, E.; Ehrig, H., Institutions for logic programming, Theoret. comput. sci., 173, 485-511, (1997) · Zbl 0901.68027
[17] MacLane, S., Categories for the working Mathematician, (1998), Springer Berlin
[18] Andréka, H.; Németi, I., A general axiomatizability theorem formulated in terms of cone-injective subcategories, (), 13-35
[19] Tarlecki, A., Quasi-varieties in abstract algebraic institutions, J. comput. system sci., 33, 3, 333-360, (1986), original version: University of Edinburgh, Report CSR-173-84 · Zbl 0622.68033
[20] Shoenfield, J., Mathematical logic, (1967), Addison-Wesley Reading, MA · Zbl 0155.01102
[21] Hodges, W., Model theory, (1993), Cambridge Univ. Press Cambridge
[22] Tarlecki, A., On the existence of free models in abstract algebraic institutions, Theoret. comput. sci., 37, 269-304, (1986), preliminary version: University of Edinburgh, Computer Science Department, Report CSR-165-84, 1984 · Zbl 0608.68014
[23] Diaconescu, R., Category-based constraint logic, Math. struct. comput. sci., 10, 3, 373-407, (2000) · Zbl 0955.68022
[24] Diaconescu, R., Completeness of category-based equational deduction, Math. struct. comput. sci., 5, 1, 9-41, (1995) · Zbl 0835.18003
[25] R. Diaconescu, Category-based semantics for equational and constraint logic programming, Ph.D. thesis, University of Oxford (1994)
[26] Meseguer, J., Membership algebra as a logical framework for equational specification, (), 18-61 · Zbl 0903.08009
[27] Y. Lamo, The institution of multialgebras—a general framework for algebraic software development, Ph.D. thesis, University of Bergen, 2002
[28] Diaconescu, R.; Goguen, J.; Stefaneas, P., Logical support for modularisation, (), 83-130
[29] Goguen, J.; Roşu, G., Institution morphisms, Formal aspects comput., 13, 274-307, (2002) · Zbl 1001.68019
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.